Model internal OpenAI klaim pecahkan sepuluh soal matematika yang lama buntu

OpenAI menyebut mereka mengarahkan versi internal dari model besar berikutnya, bernama Astra, ke sepuluh soal matematika yang hasil utamanya tidak bergerak selama setidaknya satu dekade, dan model itu menemukan solusi untuk semuanya. Biaya komputasi tiap soal di bawah 2.000 dolar. Untuk mendukung klaim ini, OpenAI merilis formalisasi Lean 4 beserta makalah pendukung di repositori GitHub publik, supaya matematikawan lain bisa memeriksa buktinya, bukan sekadar percaya pada hasil akhirnya.

Simon Willison, yang menyorot pengumuman ini, belum sepenuhnya yakin dengan cara penyajiannya. Ia mencatat OpenAI tidak membuka prompt yang dipakai untuk mencapai solusi tersebut, sehingga pekerjaan ini sulit direproduksi dan menyisakan pertanyaan seberapa besar arahan manusia di tiap penyelesaian. Ia juga menyandingkan dua reaksi dari kalangan matematikawan. Satu pihak menggambarkan krisis batin yang dalam bagi bidang yang bertumpu pada intuisi manusia, sementara Terence Tao menawarkan pandangan yang lebih tenang yang ia sebut "big mathematics", ketika manusia menyediakan pertanyaan dan arah kreatif dan mesin mengerjakan bagian teknis yang berat.

Yang perlu dicatat adalah soal biaya. Jika model frontier bisa menuntaskan persoalan yang buntu selama sepuluh tahun hanya dengan beberapa ribu dolar per soal, titik sempit di sebagian matematika murni bergeser dari tingkat kesulitan mentah ke soal mana yang layak diarahkan ke model, dan siapa yang memeriksa hasilnya.

Kenapa ini penting

Bagi yang bekerja di matematika atau bidang apa pun yang padat pembuktian, pertanyaannya bukan lagi apakah model bisa ikut berkontribusi, melainkan bagaimana kita memverifikasi hasilnya. Formalisasi Lean adalah bagian yang perlu dibaca sebelum mempercayai satu hasil pun, dan tidak adanya prompt yang dibuka jadi alasan wajar untuk tetap skeptis untuk sekarang.