Claude memformalkan Teorema Fermat dalam 11 hari—bukan bukti baru

Melalui pengumuman riset bertanggal 4 September 2026, Anthropic menyatakan Claude bekerja sebagian besar secara otonom selama 11 hari untuk memformalkan Teorema Terakhir Fermat, menghasilkan sekitar 13 juta baris Lean dan pembuktian bagi 30.300 teorema, dengan sekitar 29.500 di antaranya digunakan dalam jalur akhir.

Yang dihasilkan bukan jawaban baru atas persoalan Fermat, melainkan realisasi formal dari argumen matematika yang telah dikenal. Kode tersebut tersedia sebagai artefak terbuka yang dapat diperiksa dengan Lean 4: nilai barunya terletak pada skala dan kecepatan autoformalisasi, bukan pada penemuan strategi pembuktian baru.

Apa yang sebenarnya dikerjakan Claude

Bukti matematika untuk pembaca manusia dapat melewati langkah yang dianggap jelas, memakai konvensi bidang tertentu, dan merujuk hasil dari banyak tulisan lain. Lean menuntut objek, asumsi, serta hubungan logis dinyatakan secara tepat agar setiap kesimpulan dapat diturunkan sesuai aturan sistem tipenya.

Karena itu, pekerjaan Claude bukan sekadar menyalin tulisan Andrew Wiles ke dalam bahasa pemrograman. Agen-agen Claude harus membangun definisi dan teorema pendukung, mengisi langkah implisit, lalu menghubungkan hasil tersebut sampai mencapai pernyataan akhir Teorema Terakhir Fermat.

Pekerjaan dibagi melalui Prove2Me, yang menyimpan graf ketergantungan antarteorema dan memisahkan pernyataan dari berkas pembuktiannya. Arahan manusia diberikan terutama pada tingkat prioritas matematika, sedangkan agen memilih serta mengerjakan banyak sasaran antara. Panjang kode yang dihasilkan mencerminkan rincian formal dan cakupan teori pendukung; itu bukan ukuran banyaknya matematika baru.

Mengapa hasil itu bukan bukti matematika baru

Teorema Terakhir Fermat menyatakan bahwa persamaan aⁿ + bⁿ = cⁿ tidak memiliki solusi bilangan bulat positif ketika n lebih besar dari dua. Isi matematis persoalan tersebut telah diselesaikan melalui karya Wiles dan Taylor–Wiles; formalisasi Claude mengikuti jalur Frey, Serre, Ribet, Wiles, serta Taylor–Wiles yang sudah terdapat dalam literatur.

Dalam pemeriksaan Kevin Buzzard pada 4 September 2026, matematikawan Imperial College London itu menulis bahwa ia telah mengompilasi basis kode dan menjalankan comparator, lalu menilai formalisasi tersebut mengikuti literatur awal dengan setia tanpa menambahkan hasil matematika baru.

Kata “bukti” di sini memiliki dua lapisan yang perlu dibedakan. Para matematikawan sebelumnya menemukan isi dan strategi argumennya; Claude menghasilkan artefak formal baru yang membuat rantai deduksi itu dapat diperiksa komputer. Menyebut Claude sebagai pemecah pertama teorema tersebut akan mencampuradukkan penemuan argumen dengan formalisasi argumen.

Apa yang dijamin kernel Lean—dan batasnya

Kernel Lean memeriksa apakah setiap deklarasi mengikuti aturan sistem tipe dan apakah kesimpulan akhir benar-benar dapat diturunkan dari definisi serta aksioma yang digunakan. Model menghasilkan kode pembuktian, tetapi pemeriksa yang lebih kecil menerapkan aturan formal secara deterministik; kelulusan bukan sekadar penilaian Claude terhadap keluarannya sendiri.

Pemeriksaan tambahan membandingkan sasaran proyek dengan pernyataan Teorema Terakhir Fermat di Mathlib dan memutar ulang lingkungan pembuktian. Kernel independen juga dapat digunakan untuk mengurangi ketergantungan pada satu implementasi pemeriksa. Lapisan-lapisan ini memperkuat keyakinan bahwa artefak formal yang dipublikasikan konsisten dengan sasaran formalnya.

Namun, kernel tidak memahami maksud bahasa manusia. Ia tidak menjamin bahwa nama sebuah teorema perantara tepat menggambarkan isinya, bahwa ringkasan berbahasa Inggris akurat, atau bahwa struktur kode memberikan penjelasan yang mudah dipahami matematikawan. Manusia tetap harus memastikan bahwa pernyataan formal mewakili teorema yang dimaksud dan menilai makna ribuan hasil perantara.

Artefaknya terbuka, tetapi pemeriksaan ulang membutuhkan komputer besar

Menurut catatan teknis repositori Fermat Anthropic, dokumentasi luring menyediakan halaman bagi 29.511 teorema, sedangkan pembangunan ulang memerlukan sekitar 67 GB ruang build ditambah berkas C yang dapat mencapai sekitar 220 GB; proses yang dicatat berlangsung 5 jam 32 menit dengan 96 pekerjaan paralel dan puncak memori 153 GB, sementara comparator berjalan 14 jam 46 menit dengan puncak 230 GB dan ekspor untuk kernel independen berukuran 37,8 GB.

Angka tersebut berarti artefak dapat diperiksa ulang secara independen, tetapi reproduksi lengkapnya belum ringan untuk komputer pribadi. Repositori juga memisahkan pernyataan, pembuktian, definisi, jalur menuju teorema akhir, dan perangkat verifikasi sehingga pembaca teknis dapat melihat tepat apa yang diperiksa.

Status pencapaian ini kini cukup jelas: rantai formal tersedia dan telah lolos beberapa lapisan pemeriksaan, tetapi keterbacaan, ketepatan label teorema perantara, dan kelayakannya untuk dipelihara dalam perpustakaan komunitas masih memerlukan penilaian manusia. Hasil tersebut mengubah perkiraan tentang skala pekerjaan yang dapat diautoformalisasi dalam waktu singkat, tanpa mengubah sejarah penemuan Teorema Terakhir Fermat.

Baca juga:

• Media kit kreator bukan sekadar pengikut—data ini yang dicari brand
• 86% perekrut memaklumi celah keterampilan—kepribadian bukan jawaban kosong
• Pajak kreator berubah pada 2026: tarif final 0,5% bukan jawaban otomatis