Proyek Stacks Resmi Diformalkan dalam Lean oleh Axiom

Axiom merilis formalisasi Lean dari keseluruhan Stacks Project, referensi sumber terbuka yang memuat fondasi geometri aljabar modern. Terdiri dari sekitar 16 juta baris kode, karya ini menjadi perpustakaan matematika terformalisasi yang paling besar dan dapat digunakan kembali yang pernah dibangun.

Perpustakaan untuk Penelitian dan AI

Seluruh pengembangan matematika dari Stacks Project kini dapat diakses sebagai satu perpustakaan tunggal yang diperiksa oleh mesin. Para peneliti maupun agen kecerdasan buatan dapat mengimpor definisi dan teorema secara langsung ke dalam bukti formal baru, sementara tag permanen menghubungkan setiap deklarasi Lean kembali ke teks kanonikal.

Inisiatif ini berakar dari Stacks Project yang digagas oleh matematikawan Universitas Columbia, Johan de Jong, pada tahun 2005. Proyek tersebut telah berkembang melalui kontribusi ratusan matematikawan selama dua dekade, serta didukung oleh fondasi komunitas Lean dan Mathlib yang telah membangun perpustakaan matematika kaya dan abstraksi pendukung jauh sebelumnya.

Pentingnya verifikasi formal semakin mendesak seiring kemampuan sistem kecerdasan buatan dalam menghasilkan argumen matematika melampaui kecepatan pemeriksaan manual manusia. Di bidang geometri aljabar, sebuah bukti tunggal kerap melibatkan rangkaian teorema panjang sebelum argumen utamanya dimulai, sebuah celah infrastruktur Lean yang berhasil ditutup oleh Axiom melalui pengerahan kawanan agen kecerdasan buatan terkoordinasi.

Sejarah dan Evolusi Geometri Aljabar

Geometri aljabar mempelajari hubungan antara persamaan aljabar dan bentuk geometris, mulai dari lingkaran hingga kurva eliptik yang mengamankan kriptografi digital modern. Perkembangan bidang ini melibatkan kontribusi besar dari Emmy Noether yang mengalihkan fokus ke struktur abstrak seperti ring, modul, dan ideal, serta Alexander Grothendieck dan kolaboratornya yang memperkenalkan teori skema melalui risalah monumental.

Seiring ekspansi subjek tersebut, literatur dasarnya tersebar dalam ribuan halaman monograf berbahasa Prancis dan pengetahuan lisan dari pembimbing ke mahasiswa. De Jong kemudian mengorganisasi fondasi tersebut menyerupai pengelolaan proyek perangkat lunak sumber terbuka dengan prinsip editorial yang ketat, di mana setiap teorema memiliki bukti dan asumsi yang dinyatakan secara eksplisit.

Sebelumnya, pada 27 Oktober 2026, Axiom telah merilis formalisasi Lean untuk Klasifikasi Grup Sederhana Hingga atau CFSG. Berbeda dengan CFSG yang berpusat pada satu teorema mercusuar, Stacks Project berfungsi sebagai perpustakaan fondasi yang terdiri dari ribuan definisi, konstruksi, dan lemma yang saling mengunci untuk digunakan kembali dalam berbagai bukti mendatang.

Sistem Rekayasa dan Temuan Sistem

Untuk membangun perpustakaan yang koheren, Axiom merancang sistem hierarkis agen kecerdasan buatan dengan tanggung jawab khusus guna menerjemahkan pernyataan, mencari abstraksi di Mathlib, dan menyusun bukti secara paralel. Keandalan pernyataan ditegakkan melalui audit multingen, pengecekan silang semantik, serta keharusan setiap definisi dan lemma untuk terhubung dengan teorema hilir.

Selama proyek berlangsung, sistem tersebut menemukan puluhan pernyataan dalam Stacks Project yang memerlukan penyempurnaan lokal, termasuk hipotesis yang hilang dan kasus batas. Alih-alih mengabaikannya, agen kecerdasan buatan mendiagnosis hambatan matematika tersebut dan menyusun contoh tandingan eksplisit untuk memperbaiki literatur matematika terkait.

Dalam pengumuman tanggal 21 Oktober 2026, de Jong meminta agar komentar dan permintaan tarik yang dihasilkan oleh kecerdasan buatan tidak diserahkan langsung ke repositori hulu Stacks Project untuk saat ini. Stacks Project tetap menjadi teks hidup di bawah pengelolaan Johan de Jong dan komunitasnya, sementara formalisasi Lean ini berjalan sebagai proyek sumber terbuka independen yang dikelola oleh Axiom.

Masyarakat dapat mengeksplorasi teks berdampingan, memeriksa contoh tandingan, serta melacak grafik dependensi lengkap melalui situs stacks.axiommath.ai.