Seorang programer memakai agen AI untuk membuktikan konjektur matematika terbuka

Dan Abramov, seorang programer tanpa latar riset di matematika, menghabiskan sekitar satu bulan memakai AI untuk menghasilkan bukti sebuah konjektur terbuka, lalu memformalkannya di Lean supaya bisa diperiksa komputer. Konjektur ini berasal dari John Conway dan berbicara soal omnific integer, bagian bilangan bulat dari surreal number. Secara sederhana, ia menanyakan apakah sifat pemfaktoran yang berlaku pada bilangan bulat biasa juga berlaku di sistem bilangan yang lebih aneh ini. Abramov tidak menyelesaikannya dengan tangan. Ia membangun alur kerja tempat tiap model memegang peran berbeda: ChatGPT untuk eksplorasi matematis yang terstruktur dan menurutnya lebih skeptis, Claude untuk menulis formalisasi Lean, dengan Codex menjalankan pengaturan multi-agent secara lokal untuk mengelola tiap tahap.

Angkanya mencolok. Proyek ini menghabiskan sekitar 40 miliar token, sebagian besar berupa cached read, dengan perkiraan biaya $40.000 untuk API. Kemajuan datang bukan dari satu prompt jitu, melainkan dari menemukan hasil antara yang nyata, yang ia sebut finite-degree primality, dan itu menjadi pijakan sisa pekerjaannya. Untuk pemeriksaan akhir ia menjalankan dua agen Lean paralel, satu memverifikasi prasyarat yang sudah dikenal dan satu lagi membuktikan bagian baru secara mandiri.

Buktinya belum dikonfirmasi kalangan matematikawan. Ia lolos pemeriksaan mekanis di registry Palomar, dan beberapa orang yang paham Lean serta bidang ini menilai pernyataannya tampak benar, tapi Abramov berhati-hati soal ini dan terbuka mengundang siapa pun mencari celahnya. Seperti katanya, dengan asumsi buktinya tidak bergantung pada bug di kernel Lean, kemungkinan besar bukti itu sahih.

Kenapa ini penting

Ini titik data konkret soal posisi matematika berbantuan AI: orang non-ahli kini bisa mendorong konjektur nyata sampai ke bukti yang bisa diperiksa mesin, tapi biayanya besar dan verifikasi manusia tetap yang menentukan apakah itu dihitung sah. Kalau kamu bekerja di formal methods atau riset, yang layak dipelajari adalah alur kerjanya, bukan judulnya.