Saat sebuah perusahaan mengatakan modelnya memecahkan masalah matematika berat, pertanyaan pertama adalah verifikasi. Pada 1 Agustus, OpenAI memperkenalkan Astra lewat sepuluh hasil matematika dan ilmu komputer teoretis, makalah 249 halaman, repositori GitHub berisi sertifikat Lean, dan walkthrough penalaran.
Bidangnya mencakup geometri berdimensi tinggi, teori kode, teori grup, kompleksitas rangkaian aritmetika, kompleksitas kuantum, kriptografi lattice, dan kombinatorika ekstremal. OpenAI mengatakan hasil utama dalam masalah itu tidak maju selama setidaknya sepuluh tahun, sering kali lebih lama, dan biaya token untuk menemukan sepuluh solusi itu sekitar US$2.000 pada tarif Sol API.
Bukti ditempatkan di depan
Daftarnya mencakup batas sphere packing, peningkatan batas kode biner dan sferis, konstruksi grup non-sofic, contoh kontra untuk dugaan rigiditas Connes, batas bawah permanent, quantum parallel repetition, kekerasan closest vector problem, dugaan volume Ehrhart, dan masalah graf Erdős.
Klaim teknisnya konkret: makalah menyebut batas bawah formula n^4/log n untuk permanent, faktor kekerasan n^1/400 untuk Euclidean CVP, dan bentuk k^Theta(k) untuk bilangan Ramsey segitiga multiwarna. Repositori GitHub memakai Lean 4.32.0, mathlib, dan Lake, dengan berkas seperti NonSoficGroup.lean, ConnesRigidity.lean, dan GapCVP.lean.
“claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.”
Angka US$2.000 memberi tekanan baru
Biaya itu tidak mencakup pemilihan masalah, desain prompt, penyusunan naskah oleh manusia, formalization engineering, atau tinjauan eksternal. Jadi ini bukan sepuluh teorema seharga US$2.000. Namun angka tersebut tetap penting karena sebagian proses pencarian kini diberi harga.
Bagi laboratorium di Asia, pelajarannya praktis: klaim kemampuan matematika akan perlu disertai bukti, kode, dan jalur reproduksi. Sistem formal seperti Lean bisa menjadi infrastruktur untuk matematika berbantuan AI, teori komputer, dan bukti keamanan.
Pemeriksaan berikutnya datang dari luar
Astra masih merupakan model internal, sehingga pihak luar belum dapat mengulang proses pencarian OpenAI. Hal yang perlu diamati adalah apakah repositori Lean dapat dibangun oleh pihak ketiga, apakah pakar bidang menerima hasil dan atribusinya, serta apakah ada revisi pada syarat batas atau hubungan dengan literatur. Jika lolos, Astra menjadi preseden riset AI yang dapat diverifikasi.
Sumber: rilis riset OpenAI, makalah bukti OpenAI 249 halaman, repositori GitHub ten-proofs, CocoLoop, IT Home, dan Developers Digest; sumber memverifikasi cakupan Astra, daftar sepuluh hasil, estimasi biaya token sekitar US$2.000 pada Sol API, jalur build Lean 4.32.0, serta angka teknis n^4/log n dan n^1/400.