AI Axiom Math Memverifikasi Teorema 246 Celah Prima dalam Lean

Axiom Math mengatakan sistem AxiomProver‑nya telah menghasilkan bukti Lean 4 yang diperiksa mesin untuk hasil paling kuat yang diketahui tentang celah antara bilangan prima: teorema bahwa tak terhingga banyak pasangan prima berbeda tidak lebih dari 246. Perusahaan menerbitkan hasil tersebut pada 17 Agustus 2026 sebagai cetak biru formalitas interaktif yang memberi kredit kepada 41 kontributor bernama di bidang matematika, teknik, dan peneliti utama, dengan IEEE Spectrum pertama kali melaporkan pencapaian ini.

Batas 246 merupakan tepi pengetahuan manusia saat ini dalam upaya panjang terhadap dugaan prima kembar, hipotesis abad ke-19 yang menyatakan bahwa prima yang terpisah tepat dua muncul selamanya. Halaman proyek Axiom Math menjelaskan pekerjaan ini sebagai formalitas terpadu dari makalah James Maynard 2013 “Small gaps between primes” bersama bagian lanjutan kolaborasi Polymath8b yang memperketat batas Maynard dari 600 menjadi 246. Bukti yang diperiksa mesin diatur dalam perpustakaan Lean publik, PrimeGapsLib, dengan teorema 246 sebagai hasil unggulannya.

“Teorema ini saat ini mewakili ambang pengetahuan manusia tentang bilangan prima,” kata Ken Ono, matematikawan pendiri Axiom Math.

Verifikasi formal berarti menerjemahkan sebuah bukti ke dalam bahasa yang dapat diperiksa baris demi baris oleh program kecil yang tepercaya disebut kernel. Hasilnya bukan jaminan mutlak — pernyataan itu sendiri harus diterjemahkan dengan benar, dan pemeriksa harus dapat dipercaya — namun hal ini menghilangkan kelemahan manusia dari rantai tersebut. Sampai kini, sistem AI yang bersaing dalam benchmark matematika kebanyakan diukur pada masalah kompetisi dengan bukti pendek yang berdiri sendiri; kesenjangan antara hasil tersebut dan formalitas tingkat riset sangat lebar, pola yang terlihat pada sistem sebelumnya yang unggul dalam geometri olimpiade sementara matematika riset tetap hampir tidak tersentuh.

From 70 Million to 246

Dugaan itu sendiri, yang dirumuskan secara tepat oleh Alphonse de Polignac pada abad ke-19, masih belum terbukti. Batas hingga pertama kali muncul pada 2013, ketika Yitang Zhang membuktikan bahwa tak terhingga banyak pasangan prima berada dalam jarak 70 juta satu sama lain. Beberapa bulan kemudian, Maynard memperkenalkan metode saringan yang disempurnakan dan memotong batas menjadi 600 — pekerjaan yang berkontribusi pada Medali Fields 2022 miliknya — dan kolaborasi Polymath8b, yang melibatkan Maynard dan Terence Tao, menurunkannya menjadi 246. Cetak biru Axiom Math menampilkan progresi tersebut sebagai proyek yang ingin diformalkan.

Formalitas mengikuti alur kerja yang dijelaskan perusahaan dalam tiga tahap. Peneliti pertama‑tama menulis bukti sebagai cetak biru — setiap definisi, lema, dan teorema diberi label, pernyataan yang tepat, serta daftar hasil yang menjadi dependensinya — menghasilkan grafik ketergantungan yang mengurutkan pekerjaan. AxiomProver, sistem multi‑agen perusahaan untuk riset matematika melalui bukti formal, kemudian menghasilkan bukti Lean 4 yang dapat diperiksa mesin dengan basis Mathlib, perpustakaan matematika komunitas, dan PrimeNumberTheoremAnd, proyek formalitas yang dipimpin Alex Kontorovich dan Tao. Tim Axiom kemudian meninjau kode yang dihasilkan dan menyusunnya ke dalam PrimeGapsLib.

Hasil utama yang dinyatakan perpustakaan sedikit melampaui teorema utama. Selain batas 246, perpustakaan memformalkan batas 600 Maynard, dan menyertakan tantangan verifikasi mandiri — dibangun hanya pada Mathlib, dengan slot bukti dibiarkan kosong — yang memungkinkan siapa pun yang memiliki alat perbandingan Lean untuk secara independen mengonfirmasi bahwa bukti perpustakaan cocok dengan teorema yang dinyatakan. Perusahaan memperingatkan bahwa pemeriksaan lengkap dapat memakan waktu berjam‑jam; versi tereduksi yang mencakup dua hasil lainnya selesai dalam hitungan menit.

Where This Sits Among AI Formalization Claims

Hasil ini muncul pada tahun klaim‑klaim yang semakin meningkat tentang sistem AI yang melakukan matematika tingkat riset, kebanyakan berlandaskan skor kompetisi atau bukti pendek. Axiom Math menjadi salah satu pengklaim paling agresif: AxiomProver dikreditkan telah memecahkan masalah yang sebelumnya terbuka, termasuk pekerjaan yang dipublikasikan perusahaan dalam jurnal peer‑review, dan sistem AI kini telah memecahkan beberapa masalah Erdős yang telah lama ada. Formalisasi 246 merupakan jenis hasil yang berbeda — bukan teorema baru, melainkan rekonstruksi yang diperiksa mesin dari salah satu bukti paling menuntut secara teknis dalam teori bilangan modern.

Perbandingan terdekat terjadi awal tahun ini, ketika Math, Inc. menggunakan agen Gauss‑nya untuk menyelesaikan bukti formal hasil pemadatan bola Maryna Viazovska yang memenangkan Medali Fields pada dimensi 8 dan 24. Sidharth Hariharan, mahasiswa Ph.D. Carnegie Mellon yang memimpin upaya cetak biru manusia pada formalitas tersebut dan kini menjadi intern di Axiom Math serta kontributor matematika bernama pada proyek 246, berargumen bahwa hasil baru ini merupakan pencapaian yang lebih komprehensif. Alasannya, seperti yang ia jelaskan, adalah Axiom dibangun untuk dapat dipakai kembali: bukan formalitas satu‑kali pada satu bukti, PrimeGapsLib adalah perpustakaan yang dipelihara berisi hasil‑hasil celah prima yang dimaksudkan mendukung pekerjaan formalitas dan riset di masa depan.

Perbedaan itu penting bagi cara membaca hasil tersebut. Verifikasi satu‑kali menunjukkan bahwa sebuah sistem dapat bertahan menghadapi satu bukti yang sulit. Sebuah perpustakaan menunjukkan sesuatu yang lebih mendekati infrastruktur — mesin formal yang dapat dipakai kembali oleh hasil‑hasil lain — yang merupakan arah sistem pembuktian formal telah bergerak saat mereka beralih dari menyelesaikan latihan ke memeriksa matematika nyata. Klaim kapabilitas di sini berlandaskan artefak yang bersifat publik dan dapat dijalankan kembali, bukan pada skor benchmark: cetak biru, kode Lean, dan tantangan perbandingan yang dirancang agar peneliti luar dapat memverifikasi bukti secara mandiri.

Ono memandang matematika sebagai tempat uji coba untuk ambisi yang lebih besar. Jika sifat‑sifat perangkat lunak — apakah sebuah program berakhir, apakah outputnya benar untuk setiap masukan — dapat diekspresikan sebagai pernyataan matematika yang tepat, maka sistem yang diturunkan dari AxiomProver dapat membuktikannya secara formal, ia berargumen, mengarah pada verifikasi kode AI yang mulai menjalankan infrastruktur, keuangan, dan sistem keamanan.

“Dunia akan beroperasi dengan kode komputer yang belum pernah dibaca siapa‑pun,” kata Ono. “AI sudah hadir dan kita tidak dapat lagi menutup mata — formalitas bukti adalah tempat uji coba untuk menyelesaikan apa yang saya rasa adalah tantangan terpenting yang akan kita hadapi dari AI.”

Untuk saat ini, yang dapat diserahkan lebih sempit dan dapat diperiksa: sebuah cetak biru berkontribusi 41 penulis, sebuah perpustakaan Lean publik, dan sebuah bukti yang diverifikasi mesin bahwa prima yang berada dalam jarak 246 satu sama lain tidak pernah habis — tetangga terdekat yang terverifikasi dari dugaan prima kembar, serta bagian terdalam dari matematika riset yang belum pernah diperiksa secara menyeluruh oleh sistem AI.