Startup kecerdasan buatan Axiom Math mengumumkan telah memformalkan seluruh Stacks Project, salah satu karya rujukan matematika terbesar yang pernah ditulis manusia, menjadi sekitar 16 juta baris kode Lean yang dicek secara mekanis. Langkah ini dihadirkan sebagai benteng terhadap gelombang "AI slop" yang mengancam fondasi ilmu pengetahuan. 🔗 TechCrunch
Gelombang Manuskrip AI dalam Matematika
Kecerdasan buatan semakin sering mengklaim telah memecahkan masalah matematika yang sulit. Sebulan lalu, OpenAI merilis 719 manuskrip yang mengaku menyelesaikan sebagian masalah terberat di bidang matematika, namun pemeriksaan komputer yang dimaksudkan untuk mengonfirmasi hasil tersebut pun masih bisa lolos dari kesalahan. 🔗 TechCrunch
Axiom Math menjawab pertanyaan ini bukan dengan memperlambat, melainkan dengan membangun fondasi yang lebih kuat. Startup bernilai 1,6 miliar dolar AS ini ingin menciptakan infrastruktur terverifikasi yang dapat diandalkan agen AI untuk menulis perangkat lunak dan, pada akhirnya, melakukan penelitian ilmiah. 🔗 TechCrunch
Stacks Project: Dari 7.654 Halaman ke 16 Juta Baris Kode
Stacks Project dimulai pada 2005 oleh Johan de Jong, matematikawan Columbia, sebagai referensi sumber terbuka. Sejak itu, para matematikawan di seluruh dunia berkontribusi, membangun hasil dari aljabar tingkat perguruan tinggi hingga ide paling canggih di bidang aljabar, geometri, dan teori bilangan. 🔗 TechCrunch
Matematikawan Columbia, Peter Woit, pernah menyatakan bahwa tidak ada yang benar-benar sebanding dengan Stacks Project, dan membandingkannya dengan "buku-buku Bourbaki yang terkenal", seri yang membangun ulang matematika dari fondasinya pada abad ke-20. 🔗 TechCrunch
Axiom menggunakan armada agen AI-nya untuk menerjemahkan sekitar 7.654 halaman Stacks Project menjadi sekitar 16 juta baris kode yang dicek oleh komputer. Axiom sendiri menyebut angka sekitar 7.500 halaman dalam pengumuman resminya. 🔗 TechCrunch 🔗 Axiom Math
Formalisasi matematika dilakukan dengan menulis ulang bukti sebagai kode dalam bahasa pemrograman Lean, lalu sebuah program yang disebut proof assistant memeriksa kode baris per baris. Jika bukti lolos, matematikawan dapat mempercayai bahwa bukti tersebut secara logis sah. 🔗 TechCrunch
Insinyur menggunakan ide yang sama, disebut verifikasi formal, untuk memastikan desain chip berfungsi, sementara peneliti di Prancis menggunakannya untuk menemukan bug dalam perangkat lunak yang menghitung tunjangan keluarga. 🔗 TechCrunch
Tantangan: Menjaga Konsistensi 16 Juta Baris Kode
Formalisasi Stacks Project bukan sekadar memeriksa setiap teorema secara terpisah. Teorema dan definisi dalam Stacks saling terhubung, dan setiap hasil dibangun dari hasil sebelumnya. Seperti pohon keluarga, banyak hasil dalam Stacks dapat ditelusuri kembali ke hasil-hasil sebelumnya. 🔗 TechCrunch
Keterhubungan ini membuat Axiom awalnya tidak yakin proyek ini akan berhasil, karena tim harus menjaga setiap koneksi tetap utuh di sepanjang sekitar 16 juta baris kode Lean. "Hal-hal yang besar dan hal-hal yang halus dalam hidup biasanya tidak berjalan bersama," kata CEO Axiom, Carina Hong, kepada TechCrunch. 🔗 TechCrunch
Cara Kerja: Agen AI yang Belajar "Selera" Matematika
Untuk menyelesaikan proyek ini, tim memberikan struktur longgar kepada agen-agen mereka dan membiarkan mereka berjalan secara paralel. "Agen-agen menemukan tugas untuk diri mereka sendiri dan mengidentifikasi hal-hal yang dapat dikerjakan secara paralel," kata Ashvin Swaminathan, anggota staf teknis Axiom. 🔗 TechCrunch
Axiom juga melatih modelnya sendiri untuk mahir dalam matematika, sebuah pendekatan yang menurut Hong belum banyak diambil startup verifikasi lainnya. Awalnya, tim mengandalkan salah satu ahli Lean internal untuk mengajari agen-agen rasa manusia, dan seiring waktu agen-agen itu mengembangkan selera mereka sendiri. 🔗 TechCrunch
Hasilnya mengisi salah satu celah terbesar dalam matematika formal. "Ketika Anda melihat apa yang telah diformalisasi dalam matematika, ada lubang hitam besar. Dan lubang hitam itu mencakup geometri aljabar," kata Swaminathan. 🔗 TechCrunch
Dampak dan Kritik
Axiom berpendapat bahwa setiap hasil terverifikasi menjadi blok bangunan, sehingga bukti di masa depan dapat bersandar pada matematika yang telah dicek alih-alih memulai dari awal. Terence Tao, matematikawan UCLA dan peraih Fields Medal, menyatakan secara sederhana: "Semakin banyak bukti formal yang Anda miliki, semakin banyak bukti formal yang dapat Anda buat." 🔗 TechCrunch
Namun, klaim ini belum lepas dari catatan kritis. Analisis metadata oleh AI Proved What? menunjukkan sekitar 97 persen tag formalisasi berada dalam tier "StacksFrontier" yang ditulis AI dan belum mendapat peninjauan manusia. Analisis yang sama mencatat belum ada verifikasi build independen atas pustaka tersebut per 4 November 2026. 🔗 TechTimes
Mathlib maintainer Kim Morrison menyambut rilis ini, tetapi mengidentifikasi duplikasi pekerjaan formalisasi, kesenjangan antara beberapa pernyataan Stacks dan pasangan formalnya, serta masalah yang dapat memengaruhi penggunaan ulang. Penilaian Morrison ini menimbulkan pertanyaan soal kelengkapan, tetapi tidak membuktikan pustaka tersebut secara keseluruhan tidak sah. 🔗 TechTimes
Implikasi Lebih Luas
Axiom yakin perangkat lunak di masa depan akan membutuhkan fondasi terverifikasi, seperti yang kini disediakan Stacks Project. "Kami percaya bahwa matematika adalah domain di mana Anda mulai membangun hal-hal ini dan bahwa itu adalah keterampilan yang dapat ditransfer," kata Swaminathan. "Agen dapat membaca kode kami, memahaminya, dan membangun infrastruktur baru di atasnya." 🔗 TechCrunch
Cara agen-agen Axiom membangun Stacks, bekerja secara paralel dan memilih tugas mereka sendiri, adalah bagaimana Hong memperkirakan sebagian besar pekerjaan AI di masa depan akan dilakukan. "Anda ingin agen memiliki perpustakaan yang dapat digunakan ulang untuk mereka bangun dan terus mendorong batas," kata Hong. 🔗 TechCrunch
Fakta Kunci
- Axiom Math bernilai 1,6 miliar dolar AS dan menggalang pendanaan Seri A senilai 200 juta dolar AS yang dipimpin Menlo Ventures pada Maret 2026.
- Stacks Project berisi sekitar 7.654 halaman matematika tingkat lanjut, diterjemahkan menjadi sekitar 16 juta baris kode Lean.
- Stacks Project dimulai pada 2005 oleh Johan de Jong dari Columbia University dan dikembangkan ratusan matematikawan selama dua dekade.
- Formalisasi menggunakan proof assistant Lean untuk memeriksa bukti baris per baris secara mekanis.
- Sekitar 97 persen tag formalisasi berada dalam tier StacksFrontier yang ditulis AI dan belum ditinjau manusia.
- CEO Axiom, Carina Hong, berusia 25 tahun, keluar dari program PhD matematika Stanford, dan mendirikan perusahaan pada Maret 2025.
Sumber
- TechCrunch — "Axiom Math wants to keep AI slop out of mathematics" (5 November 2026) — https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/
- TechTimes — "A $1.6B AI Company Wants To Stop Chatbots From Flooding Mathematics With Made-up Answers" (6 November 2026) — https://www.techtimes.co.uk/axiom-math-stacks-project-lean-library-review-1809778
- Axiom Math — "The Stacks Project, formalized in Lean" — https://axiommath.ai/research/the-stacks-project-formalized/
- Axiom Math (@axiommathai) via X — pengumuman formalisasi Stacks Project (4 November 2026)
