Rasanya kecerdasan buatan hampir setiap minggu menyelesaikan masalah matematika baru. Bulan lalu, hanya OpenAI saja yang merilis 719 naskah yang mengklaim menyelesaikan beberapa masalah paling sulit di bidang ini. Bahkan pemeriksaan oleh komputer pun bisa salah. Setelah bertahun-tahun menghadapi konten sampah AI, orang tidak bisa tidak bertanya, apakah matematika akan menjadi bidang berikutnya yang terdampak.
AxiomMath dapat menghindari nasib ini bukan dengan memperlambat, tetapi dengan membangun fondasi yang lebih kuat. Startup bernilai 1,6 miliar dolar AS ini berharap menciptakan lapisan dasar yang telah diverifikasi, yang memungkinkan agen AI mengandalkannya untuk menulis perangkat lunak, dan pada akhirnya melakukan penelitian ilmiah.
Pada hari Rabu, perusahaan tersebut mengumumkan telah secara resmi memverifikasi Stacks Project, salah satu pencapaian matematika terbesar yang pernah ditulis manusia. Para matematikawan biasanya memberikan penilaian sangat tinggi terhadap Stacks. Matematikawan dari Universitas Columbia, Peter Woit, pernah menyebutnya "hampir tidak ada hal lain yang bisa dibandingkan dengannya," dan membandingkan proyek ini dengan "seri Bourbaki yang terkenal"—seri karya yang merekonstruksi matematika dari dasar pada abad ke-20.
Colleague Woit dari Kolombia, Johan de Jong, meluncurkan Stacks Project pada tahun 2005 sebagai referensi open source. Sejak itu, para matematikawan terus berkontribusi, memperluas konten dari aljabar tingkat universitas hingga ke ide-ide terdepan di bidang aljabar, geometri, dan teori bilangan.
Kelompok agen AI perusahaan menerjemahkan basis data sekitar 7.654 halaman ini menjadi sekitar 16 juta baris kode yang dapat diperiksa oleh komputer.
Tujuan matematika formal adalah memastikan bahwa struktur dasarnya dapat diandalkan. Matematikawan akan menulis ulang bukti menjadi kode menggunakan bahasa pemrograman bernama Lean, lalu program yang disebut proof assistant memeriksa kode tersebut baris demi baris. Jika bukti lulus, matematikawan dapat percaya bahwa bukti tersebut secara logis valid.
Insinyur juga menggunakan pendekatan yang sama, yaitu verifikasi formal, untuk memastikan apakah desain chip layak; peneliti Prancis menggunakannya untuk menemukan kerentanan perangkat lunak dalam perhitungan tunjangan keluarga.
Untuk repositori seperti Stacks Project, memeriksa teorema satu per satu hanyalah sebagian dari pekerjaan. Teorema dan definisi dalam Stacks saling terkait, dan masing-masing dibangun di atas konten sebelumnya. Seperti silsilah, banyak hasil dalam Stacks dapat ditelusuri kembali ke hasil yang lebih awal.
Keterkaitan ini membuat Axiom awalnya tidak yakin apakah proyek ini layak dilanjutkan. Tim harus memastikan setiap koneksi tetap utuh di dalam sekitar 16 juta baris kode Lean.
CEO Axiom, Carina Hong, mengatakan kepada TechCrunch: "Skala besar dan kehalusan biasanya tidak kompatibel dalam kenyataan. [Stacks] adalah sekumpulan hasil matematis yang membentuk dasar matematis. Anda ingin [teorema] saling konsisten, bukan seperti yang berparadoks. Anda juga ingin definisi-definisi ini tidak saling bertentangan."
CEO berusia 25 tahun ini pernah drop out dari program doktor matematika di Stanford dan mendirikan perusahaan ini pada Maret 2025. Pada Maret tahun ini, Axiom menyelesaikan pembiayaan Seri A senilai $200 juta yang dipimpin oleh Menlo Ventures.
Hong mengatakan: "Kami tidak yakin apakah vibe coding dapat mempertahankan keindahan Stacks."
Untuk menyelesaikan proyek ini, tim memberikan struktur yang fleksibel kepada agen dan menjalankannya secara paralel. Ashvin Swaminathan, anggota tim teknologi Axiom, mengatakan, "Untuk Stacks, kami menetapkan sebuah hierarki... tetapi bukan hierarki yang secara ketat menentukan apa yang harus dilakukan setiap agen. Agen akan mencari tugas sendiri dan mengidentifikasi hal-hal yang dapat diproses secara paralel."
Axiom juga melatih model mereka sendiri agar unggul dalam matematika. Hong mengatakan, pendekatan ini tidak diambil oleh sebagian besar startup verifikasi lainnya. Awalnya, tim mengandalkan seorang ahli Lean internal untuk mengajarkan agen-agen tersebut membentuk standar penilaian seperti manusia. Seiring berjalannya waktu, Hong mengatakan, agen-agen tersebut telah belajar sendiri kemampuan penilaian tersebut.
Hasil ini mengisi salah satu kekosongan terbesar dalam matematika formal. Swaminathan mengatakan, "Ketika Anda melihat konten matematika yang telah diformalkan, Anda akan melihat ada lubang hitam besar. Dan lubang hitam itu mencakup geometri aljabar."
Swaminathan mengatakan bahwa hingga kini, peneliti yang ingin menggunakan Lean untuk memeriksa pekerjaan baru dalam geometri aljabar hampir tidak memiliki dasar yang siap pakai. "Sekarang mereka memilikinya."
Axiom percaya bahwa setiap hasil yang diverifikasi menjadi blok bangunan, di mana bukti masa depan dapat dibangun di atas matematika yang telah diperiksa, tanpa harus memulai dari awal. Matematikawan UCLA dan penerima Penghargaan Fields, Terence Tao, merangkumnya dengan lebih ringkas: "Semakin banyak bukti formal yang Anda miliki, semakin banyak bukti formal yang dapat Anda hasilkan."
Target audiens Axiom tidak hanya matematikawan. Para pengembang telah lama berusaha memastikan kode mereka bebas dari kerentanan dan risiko keamanan. Seiring dengan semakin banyaknya perangkat lunak yang ditulis oleh agen AI, masalah ini hanya akan menjadi lebih besar.
Axiom betting, perangkat lunak masa depan perlu dibangun di atas fondasi yang telah terbukti, seperti Stacks saat ini.
Swaminathan mengatakan: “Kami percaya bahwa matematika adalah bidang di mana Anda memulai membangun hal-hal ini, dan ini adalah keterampilan yang dapat dipindahkan. Agen dapat membaca kode kami, memahaminya, dan membangun infrastruktur baru di atasnya. Formalisasi yang kami buat dengan Lean sekarang menjadi fondasi dasar di mana agen dapat membangunnya.”
Cara Axiom membangun Stacks—bekerja secara paralel dan memilih tugas sendiri—adalah cara yang diharapkan Hong akan menjadi standar banyak pekerjaan AI di masa depan. Ia percaya bahwa agen AI memerlukan basis pengetahuan yang terstruktur dan dapat digunakan kembali untuk menghindari menghasilkan konten sampah.
Hong mengatakan: "Anda ingin [agen] memiliki repositori yang dapat digunakan kembali, di mana mereka dapat terus membangun dan mendorong batas-batasnya. Jika Anda memulai dengan pilihan teknis yang buruk dan memenuhinya dengan sampah, maka akan sangat sulit bagi mereka untuk memperluas batas tersebut."
Hong sangat percaya diri dengan metode ini, bahkan secara terbuka mengeluarkan tantangan. Dia berkata, "Saya secara terbuka menantang semua perusahaan pemrograman untuk melakukan pekerjaan formalisasi sebesar ini."