Anthropic merilis secara open source bukti lengkap Teorema Terakhir Fermat dalam Lean 4 yang telah diverifikasi mesin, di bawah lisensi Apache 2.0. Kode ini dibangun di atas pustaka matematika Mathlib. Pernyataan formal yang diberikan repositori ini adalah: untuk sembarang n ≥ 3 dan bilangan bulat positif a, b, c, berlaku a^n + b^n ≠ c^n. Dalam Lean, kalimat ini ditulis sebagai teorema yang dapat diverifikasi selangkah demi selangkah oleh kernel, tanpa menyisakan celah apa pun.
Skalanya adalah bagian paling langsung terlihat dari proyek ini. Repositori mencatat 60.475 modul, 29.511 teorema, dan 1.450 modul definisi, dengan pengecekan ekspor mencakup 1.052.234 deklarasi. Dokumentasi HTML yang dihasilkan berukuran sekitar 390 MB, sementara berkas ekspor lengkapnya mencapai 37,8 GB. Untuk menjalankan ulang secara lokal dibutuhkan ruang disk lebih dari 300 GB dan penggunaan memori puncak sekitar 153 GB.
Tiga lapis pengecekan, semuanya tercatat
Repositori ini tidak hanya menyatakan “berhasil dikompilasi” begitu saja. Pengecekan pertama adalah kompilasi kernel penuh oleh Lean 4.33.1 sendiri, yang memakan waktu 5 jam 32 menit di mesin 96-core. Pengecekan kedua menggunakan alat comparator resmi dari leanprover (v4.33.0) untuk verifikasi ulang, yang berjalan sekitar 14 jam 46 menit. Pengecekan ketiga beralih ke kernel independen yang ditulis dalam Rust, nanoda 0.4.13, yang selesai dalam sekitar 30 menit dengan 16 thread dan menampilkan output Your solution is okay!
Di luar tiga lapis pengecekan itu, ada satu batasan ketat lagi: seluruh modul tidak boleh mengandung axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def, maupun #eval. Kata kunci-kata kunci ini dikenal luas di komunitas Lean sebagai pintu belakang yang berpotensi jadi celah. sorry secara harfiah menandai bagian yang belum dibuktikan, sedangkan native_decide menyerahkan sebagian penilaian ke kode mesin yang tidak pernah dicek oleh kernel. Menyingkirkan semuanya sama saja dengan mengakui bahwa kredibilitas bukti ini sepenuhnya bertumpu pada kernel Lean dan alat pengecek — dan itu memang yang dinyatakan sendiri oleh README-nya.
Seberapa banyak yang ditulis AI, repositori ini tidak mengungkapkan
Menurut README, kode sumber Lean “dihasilkan oleh agen AI di atas kode Lean open source yang ditulis manusia, dengan Lean bertindak sebagai wasit.” Rasio pastinya tidak diungkapkan — modul mana yang ditulis manusia dan modul mana yang dihasilkan model lalu dikembalikan oleh kernel untuk ditulis ulang, rinciannya tidak dapat ditemukan dalam materi publik.
Sebaliknya, fondasi yang disumbangkan manusia dicantumkan cukup jelas. Sebanyak 106 berkas dependensi berasal dari proyek akademik yang sudah ada, terutama proyek formalisasi FLT yang dipimpin Kevin Buzzard dari Imperial College London serta flt-regular yang menangani kasus regular Kummer; selain itu ada 23 modul lain yang membuktikan ulang materi yang sudah ada di Mathlib.
Bila ditempatkan dalam sejarah matematika formal, lompatan skala kali ini cukup mencolok. Teorema Empat Warna diformalkan oleh Georges Gonthier dalam Coq pada 2005, sementara proyek Flyspeck untuk konjektur Kepler diumumkan rampung pada 2014 — keduanya diukur dalam satuan tahun-orang (person-year). Ketika tim Buzzard memulai proyek FLT, ekspektasi dari luar juga berupa rentang waktu bertahun-tahun. Seberapa jauh repositori ini memajukan garis akhir tersebut bergantung pada proporsi pembagian kerja manusia-AI yang sesungguhnya — dan itulah satu-satunya angka yang sampai sekarang belum terungkap.
Sumber: README dan catatan verifikasi repositori publik Anthropic, CocoLoop, proyek Mathlib, materi publik proyek FLT Imperial College London; jumlah modul, jumlah teorema, dan durasi tiga tahap pengecekan diverifikasi sesuai angka yang tercantum di repositori.