Pada 1 Agustus 2026, OpenAI mengumumkan pencapaian luar biasa di bidang matematika teoretis. Model AI internal mereka yang belum dirilis ke publik bernama Astra berhasil menghasilkan solusi untuk 10 masalah matematika terbuka yang masing-masing telah tidak terpecahkan selama setidaknya satu dekade.
Yang membuat pencapaian ini istimewa adalah biayanya yang sangat terjangkau. Seluruh proses pembuktian membutuhkan biaya komputasi hanya sekitar 2.000 dollar AS (sekitar Rp32 miliar). Setiap bukti telah diverifikasi secara otomatis menggunakan Lean 4, sistem pembuktian formal yang memastikan kebenaran matematis tanpa celah.
Apa Saja yang Berhasil Dipecahkan?
OpenAI mempublikasikan manuskrip setebal 249 halaman yang mencakup berbagai jenis hasil: bukti formal, kontra-eksampel, dan batas yang lebih baik dari sebelumnya. Masalah-masalah ini berasal dari enam bidang matematika dan ilmu komputer teoretis, termasuk:
- Geometri — hasil baru tentang struktur ruang dan bentuk
- Kriptografi — implikasi untuk keamanan sistem enkripsi
- Teori Kompleksitas — batas baru tentang seberapa sulit masalah komputasi tertentu
Hasil paling menonjol adalah konstruksi eksplisit dari grup non-sofik, masalah yang telah terbuka sejak 1999 atau selama 27 tahun. Grup sofik adalah konsep fundamental dalam matematika abstrak, dan keberadaan grup non-sofik selama ini hanya diperkirakan tanpa bukti konstruksi yang eksplisit.
Bagaimana Astra Bekerja?
Astra bukan sekadar chatbot matematika biasa. Model ini dirancang khusus untuk penalaran matematis tingkat tinggi, mampu merumuskan strategi pembuktian, mencari kontra-eksampel, dan membangun argumen formal yang kompleks. Setelah Astra menghasilkan draf bukti, tim manusia di OpenAI menyiapkan manuskrip dan memformalkannya dalam Lean 4.
Seluruh file Lean, rantai alat (toolchain), daftar aksioma, dan metadata dipublikasikan secara terbuka di repositori GitHub OpenAI. Ini memungkinkan siapa saja untuk memverifikasi kebenaran hasil secara independen.
Apakah Ini Berarti AI Sudah Menggantikan Matematikawan?
OpenAI menekankan bahwa Astra belum menggantikan peran matematikawan profesional. Hasil-hasil ini masih memerlukan tinjauan independen oleh spesialis sebelum diterima secara luas oleh komunitas matematika. Kemampuan Astra adalah menghasilkan draf bukti yang kemudian disempurnakan oleh manusia.
Namun, pencapaian ini menunjukkan bahwa AI kini mampu berkontribusi pada penemuan matematis asli, bukan sekadar menyelesaikan soal-soal yang sudah diketahui jawabannya. Biaya 2.000 dollar AS untuk 10 pembuktian yang masing-masing telah terbuka selama bertahun-tahun menunjukkan efisiensi luar biasa yang sebelumnya tidak terbayangkan.
Dampak bagi Masa Depan Riset Matematika
Pencapaian Astra membuka kemungkinan baru untuk kolaborasi manusia-mesin dalam penelitian matematika. Para peneliti kini dapat menggunakan AI untuk mengeksplorasi ruang masalah yang terlalu luas untuk diteliti secara manual, sambil tetap mempertahankan standar ketat pembuktian formal.
OpenAI belum mengumumkan kapan Astra akan tersedia untuk publik atau berapa harga aksesnya. Namun, publikasi terbuka ini menetapkan preseden penting: hasil matematika yang dihasilkan AI dapat diverifikasi secara independen dan transparan.
