Sebuah startup yang didirikan oleh seorang dropout Stanford kurang dari 15 bulan lalu mengklaim telah melakukan sesuatu yang biasanya memakan waktu puluhan tahun bagi matematikawan manusia: menyelesaikan beberapa masalah matematika yang belum terpecahkan menggunakan sistem AI, lalu mendapatkan karya tersebut diterima oleh kalangan akademis.
Axiom Math, perusahaan berbasis Palo Alto yang dipimpin pendirinya Carina Hong, menyatakan bahwa sistem AxiomProver-nya telah menyelesaikan setidaknya empat masalah matematis yang sebelumnya belum terpecahkan. Bukti-bukti tersebut diposting di arXiv pada Februari 2026, tetapi hingga akhir Mei 2026, belum ada publikasi di jurnal yang ditinjau sejawat yang dikonfirmasi—perbedaan ini disembunyikan oleh kerangka artikel tersebut.
Apa yang sebenarnya diselesaikan oleh Axiom
Masalah yang dipecahkan oleh AxiomProver bukanlah latihan sepele. Di antara hasilnya adalah solusi untuk dugaan-dugaan signifikan dalam geometri aljabar dan Dugaan Fel, sebuah masalah yang terkait dengan karya Srinivasa Ramanujan. Salah satu masalah yang terpecahkan melibatkan dugaan teori bilangan berusia 20 tahun.
Setidaknya salah satu bukti dihasilkan dari kolaborasi dengan matematikawan terkemuka, bukan hasil murni mesin.
Perusahaan menggunakan verifikasi formal melalui asisten bukti Lean. Alih-alih menghasilkan teks yang tampak seperti bukti dan berharap itu benar, AxiomProver menghasilkan bukti yang diperiksa secara mekanis untuk validitas logis pada setiap langkah. Lapisan verifikasi formal inilah yang memberikan kredibilitas pada karya tersebut, yang tidak dimiliki oleh output model bahasa besar biasa.
Uang dan tim di baliknya
Axiom Math mengumpulkan dana Seri A sebesar $200 juta yang dipimpin oleh Menlo Ventures, mendorong valuasi pasca-investasi menjadi $1,6 miliar. Hal ini ditambah dengan $64 juta dalam investasi seed sebelumnya, sehingga total pendanaan yang diketahui mencapai $264 juta. Hong meninggalkan program joint J.D./Ph.D. di Stanford untuk memulai usaha ini pada Maret 2025.
Ken Ono, seorang teori bilangan terkemuka yang dikenal karena karyanya tentang warisan Ramanujan dan bentuk modular, bergabung dengan Axiom Math sebagai matematikawan pendiri.
Gambaran lebih besar mengenai AI dan matematika
Axiom Math tidak beroperasi dalam ruang hampa. Google's DeepMind telah mendorong kemajuan dalam penalaran matematis, paling terlihat dengan sistem AlphaProof-nya.
Praktik standar bagi para matematikawan adalah memposting preprint di arXiv sementara makalah sedang menjalani tinjauan sejawat, sebuah proses yang dapat memakan waktu berbulan-bulan atau bahkan bertahun-tahun. Postingan arXiv Februari 2026 saat ini sedang menjalani pemeriksaan oleh para ahli, dan belum ada publikasi yang ditinjau sejawat yang dikonfirmasi hingga akhir Mei 2026.