OpenAI Astra Klaim Pecahkan 10 Soal Matematika Terbuka Cuma $2.000

Sepuluh soal matematika dan ilmu komputer teoretis yang sama-sama mandek minimal satu dekade, dipecahkan dalam satu pengumuman, dengan total biaya komputasi cuma sekitar $2.000. Itu klaim yang dilempar OpenAI pada 1 Agustus lalu lewat model riset internal bernama Astra—disebut sebagai cikal bakal keluarga model utama berikutnya perusahaan itu. Periset OpenAI Sébastien Bubeck yang mengumumkan hasilnya, sementara presiden OpenAI Greg Brockman menambahkan detail soal ongkos komputasinya, dan perusahaan merilis manuskrip setebal 249 halaman lengkap dengan sertifikat Lean 4 yang bisa diverifikasi mesin untuk tiap hasil di GitHub OpenAI.

Sepuluh soal yang "jatuh" dalam satu pengumuman

Hasil paling menonjol adalah konstruksi eksplisit pertama untuk grup non-sofik—menjawab pertanyaan yang menggantung sejak matematikawan Mikhail Gromov memperkenalkan konsep sofisitas pada 1999, hampir 27 tahun lalu. Selain itu, Astra diklaim mematahkan dugaan rigiditas Connes soal aljabar von Neumann grup, membuktikan dugaan volume Ehrhart, dan menyelesaikan tiga soal dari katalog Paul Erdős, termasuk soal nomor 183 tentang bilangan Ramsey multiwarna. Di ranah packing bola berdimensi tinggi, Astra juga diklaim menentukan secara eksak kekuatan asimtotik program linear Cohn–Elkies, memberi batas atas baru untuk kepadatan packing—perbaikan pertama pada eksponennya sejak 1978 Tech Times.

Setiap soal itu bukan sekadar sulit—sebagian memang sudah lama ditinggalkan komunitas matematika karena dianggap buntu, bukan cuma berat.

Cara verifikasinya: bukan kata OpenAI, tapi kata Lean

Yang membedakan klaim ini dari sekadar pengumuman marketing adalah mekanisme verifikasinya. Setiap hasil disertai sertifikat Lean 4—proof assistant yang mengecek validitas logis sebuah bukti secara mekanis, baris demi baris, tanpa perlu memercayai kata-kata OpenAI. Siapa pun bisa mengunduh sertifikat itu dari GitHub dan mengompilasinya sendiri untuk memastikan buktinya konsisten secara internal. Forbes mencatat Brockman menyebut seluruh proses menghasilkan sepuluh bukti itu memakan biaya komputasi API sekitar $2.000—angka yang jadi sorotan karena riset matematika tingkat ini biasanya makan waktu bertahun-tahun kerja manusia Forbes.

Sumber gambar: Domaintechnik di Unsplash

Kenapa sebagian matematikawan bilang klaimnya digembungkan

Kritik paling tajam datang dari peneliti AI Gary Marcus, yang menulis Astra memang mengesankan secara teknis tapi klaimnya "vastly oversold". Argumennya bertumpu pada satu celah penting: sertifikat Lean cuma memastikan pernyataan yang diformalkan itu benar secara logis—bukan memastikan pernyataan formal tersebut benar-benar menangkap soal terbuka aslinya persis seperti yang dipahami komunitas matematika selama ini. Menilai kesesuaian keduanya tetap butuh keahlian domain manusia, bukan sekadar kompilasi yang berhasil Gary Marcus.

Perbandingannya jadi lebih tajam kalau ditaruh di samping pengumuman serupa OpenAI pada Mei lalu, yang secara eksplisit menyebut hasilnya sudah diperiksa matematikawan independen di luar perusahaan. Pengumuman sepuluh bukti Astra kali ini tidak membuat klaim tinjauan eksternal seluas itu—metadata repositori dan proses kompilasi yang bisa direproduksi bukan pengganti tinjauan independen menyeluruh atas paket matematika secara utuh.

Sumber gambar: Glenn Carstens-Peters di Unsplash

Sinyal di balik nama "Astra"

Di luar soal matematika itu sendiri, pemilihan nama "Astra" untuk model yang disebut jadi basis keluarga model utama berikutnya juga jadi bahan pembacaan industri. OpenAI selama ini jarang membocorkan nama model depan jauh sebelum rilis publik—dan memilih melakukannya lewat pameran kemampuan riset murni, bukan lewat demo produk. Itu konsisten dengan pola OpenAI belakangan: mengukur kemajuan "penalaran jangka panjang" lewat soal-soal yang jawabannya bisa diverifikasi mesin secara objektif, entah itu kompetisi matematika atau—seperti kasus model riset lain OpenAI bulan lalu yang membuktikan konjektur jarak-satuan Erdős—soal geometri diskret.

Takeaway

Sepuluh sertifikat Lean yang bisa dikompilasi siapa pun adalah bukti nyata bahwa formalisasinya konsisten secara logis, dan itu sendiri sudah jadi pencapaian teknis yang jarang dipamerkan lewat cara sesahih ini. Tapi jarak antara "pernyataan formal ini valid" dan "ini benar-benar menjawab soal terbuka yang dipikirkan matematikawan selama puluhan tahun" masih perlu ditutup oleh manusia, bukan mesin. Sampai tinjauan independen yang lebih luas dari komunitas matematika muncul—seperti yang eksplisit terjadi pada pengumuman Mei lalu—klaim Astra pantas dibaca sebagai sinyal kemampuan yang genuinely maju, dikemas dengan tingkat kepastian yang lebih tinggi dari yang bisa dijamin buktinya sendiri.