OpenAI Klaim Model AI Rahasia Pecahkan Ratusan Soal Matematika, Ilmuwan Minta Bukti
Baca dalam 60 detik
- OpenAI mengunggah 722 manuskrip matematika ke GitHub yang dihasilkan model AI internal yang belum dirilis ke publik.
- Hanya 162 dari 722 manuskrip yang memiliki verifikasi komputer melalui Lean, memicu keraguan tentang validitas klaim.
- Para matematikawan menuntut transparansi model, prompt, dan bukti replikasi sebelum mengakui terobosan ini.

OpenAI kembali membuat geger dunia akademik. Perusahaan riset kecerdasan buatan itu mengunggah 722 manuskrip matematika ke repositori GitHub pada Selasa lalu, semuanya dihasilkan oleh model AI internal yang belum dilepas ke publik. Klaimnya mengejutkan: hampir seluruh manuskrip tersebut dihasilkan dari satu perintah tunggal yang diberikan kepada satu agen AI, meskipun sebagian mungkin memerlukan beberapa kali percobaan.
Jika benar, ini bisa menjadi lompatan besar dalam bidang matematika. Namun, tidak semua ilmuwan menyambut klaim tersebut dengan antusias. Sejumlah matematikawan terkemuka justru mempertanyakan validitas dan transparansi di balik pencapaian itu. Mereka menuntut bukti konkret sebelum menerima narasi besar yang disampaikan OpenAI.
"Sampai mereka merilis modelnya dan orang bisa mereplikasi hasilnya, saya pikir klaim tentang penyelesaian masalah dengan satu agen tunggal harus dianggap belum terverifikasi," ujar Andrew Sutherland, matematikawan dari Massachusetts Institute of Technology (MIT), kepada Scientific American. "Kita harus meminta bukti," tegasnya.
Manuskrip-manuskrip tersebut dikelompokkan ke dalam 372 "keluarga" hasil terkait, di mana satu keluarga bisa memuat teorema utama beserta argumen pendamping, konsekuensi, atau bukti alternatif. Artinya, angka 722 merujuk pada jumlah manuskrip, bukan jumlah soal yang terpecahkan. OpenAI sendiri mengakui bahwa tidak semua manuskrip memiliki formalisasi Lean dan "beberapa hasil yang tidak diformalkan mungkin bermasalah." Dengan kata lain, sebagian besar dari apa yang mereka publikasikan bisa saja salah.
Verifikasi Lean hanya memastikan bahwa bukti mengikuti pernyataan sebagaimana tertulis dalam Lean. Alat itu tidak membuktikan bahwa pernyataan tersebut cocok dengan soal asli, atau bahwa hasilnya baru dan penting. Aspek terakhir inilah yang kini harus dinilai oleh para matematikawan—dan di sinilah keraguan muncul.
"Adalah fakta bahwa AI kini dapat menghasilkan argumen matematika dalam situasi di mana manusia yang memicunya tidak mampu memahami, memverifikasi, atau bertanggung jawab atas argumen tersebut," demikian pernyataan Institute for Advanced Study di Princeton, New Jersey. "Kami percaya pemahaman manusia atas matematika tetap yang terpenting. Bagaimana, di era baru ini, kita bisa menuju paradigma yang memasukkan pemahaman manusia sebagai bagian dari output akademik yang bertanggung jawab?"
Kritik juga datang dari aspek teknis. Repositori openai/math dikelola dengan fitur Issues dimatikan dan tidak pernah menerima pull request. "Itu mengecewakan. Jika Anda mempublikasikan 722 manuskrip dan meminta formalisasi Lean, Anda perlu tempat bagi orang untuk mengirimkannya," tulis Keith Adler, seorang peneliti, di platform X. Dmitry Rybin, matematikawan lain, mengaku kesulitan memahami bukti yang diajukan OpenAI untuk masalah bilangan kromatik bidang, menyebutnya sebagai "matematika alien yang sulit dipercaya."
Meski begitu, ada pula yang melihat sisi positif. Profesor Abhishek Saha menyebut hari itu sebagai "hari yang sangat besar bagi matematika," tetapi mencatat bahwa sebagian besar soal termasuk dalam kategori "kemajuan luar biasa dalam program yang sudah ada" atau "terobosan mengejutkan." Artinya, mayoritas soal menarik, tetapi tidak mustahil atau mengubah permainan seperti masalah Millennium. Hanya satu dari 722 manuskrip yang masuk kategori terobosan besar: Quasi-Riemann Hypothesis.
OpenAI juga dinilai belum memenuhi rekomendasi kelompok penasihat Institute for Advanced Study yang dirilis 29 September lalu. Rekomendasi itu mencakup pengungkapan nama model, prompt, ringkasan alur pemikiran, waktu yang dibutuhkan, dan biaya komputasi untuk setiap hasil. OpenAI hanya mempublikasikan angka komputasi rata-rata dan 10 ringkasan penalaran, tanpa prompt, dengan alasan masih berupaya merilis model secara bertanggung jawab.
Sebagai perbandingan, Anthropic mengambil jalur berbeda dengan mempublikasikan seluruh 13 juta baris bukti Fermat's Last Theorem yang telah diverifikasi Lean di GitHub bulan lalu. Bukti tersebut memformalkan teorema yang dipublikasikan Andrew Wiles pada 1995, bukan mengklaim hasil baru. OpenAI berjanji akan menambahkan formalisasi Lean seiring diperolehnya; untuk saat ini, baru 162 dari 722 manuskrip yang memilikinya.
Bagi Indonesia, perkembangan ini menjadi cermin penting. Riset AI di Tanah Air masih didominasi oleh adopsi teknologi, bukan penciptaan model dasar. Ketika dunia bergerak ke arah verifikasi formal dan transparansi riset AI, Indonesia perlu memperkuat ekosistem riset matematika dan ilmu komputer agar tidak sekadar menjadi konsumen. Pertanyaannya, apakah lembaga riset dan kampus di Indonesia siap terlibat dalam gelombang baru ini—bukan hanya sebagai pengguna, tetapi juga sebagai kontributor yang mampu memverifikasi dan mengembangkan?



