Anthropic menyatakan bahwa Claude telah menyelesaikan bukti formal pertama untuk Teorema Terakhir Fermat. Ini bukan penemuan ulang teorema tersebut, melainkan mentranskripsi bukti yang sudah ada menjadi kode logika yang dapat diverifikasi baris demi baris oleh komputer. Perusahaan menyebut pekerjaan ini memakan waktu 11 hari dan menghasilkan sekitar 13 juta baris konten.
Arti dari bukti formal adalah menuliskan argumen matematis dalam bahasa yang dapat diperiksa oleh mesin. Bukti dalam paper tradisional sering memerlukan tinjauan sejawat yang berkepanjangan; jika terdapat kelemahan di salah satu langkahnya, proses perbaikan bisa berlangsung selama berbulan-bulan bahkan bertahun-tahun. Teorema Terakhir Fermat dibuktikan oleh matematikawan Inggris Andrew Wiles pada tahun 1995, tetapi mengonversi seluruh bukti ini menjadi versi yang dapat diperiksa oleh mesin selalu dianggap sebagai proyek teknis yang sangat intensif.
Selesaikan tujuan proyek jangka panjang dalam 11 hari
Matematikawan Imperial College London, Kevin Buzzard, telah mendorong proyek terkait sejak 2024, dengan tujuan yang sama yaitu mentranskripsikan bukti Wiles ke dalam asisten bukti Lean. Sesuai rencana awal, pekerjaan ini memerlukan kolaborasi jangka panjang, dan pendanaan telah diatur hingga tahun 2029.
Anthropic menyatakan bahwa Claude telah menyelesaikan tugas ini lebih awal daripada tujuan sejenisnya. Setelah ditinjau oleh Buzzard, bukti ini dinyatakan dapat berdiri sendiri tanpa bergantung pada asumsi tambahan, yaitu hanya berdasarkan sistem aksioma paling dasar matematika.
Diselesaikan secara paralel oleh banyak agen
Menurut Anthropic, tim peneliti dari Universitas Columbia, yang dipimpin oleh Tianyi Peng, membiarkan beberapa agen Claude bekerja secara paralel, masing-masing bertanggung jawab untuk menulis definisi dan membuktikan kesimpulan kecil, kemudian menyusunnya secara bertahap menjadi struktur bukti yang lebih besar. Intervensi manusia sangat sedikit, terutama hanya memberikan urutan prioritas tahapan.
Progress awal tidak berjalan lancar. Anthropic menyatakan bahwa sebagian agen sementara tidak dapat berbagi konten yang telah selesai dan seringkali melakukan pekerjaan yang sama berulang-ulang. Kemudian, tim menggunakan alat bernama Prove2Me untuk memberikan daftar tugas dan cara pengorganisasian file yang seragam kepada masing-masing agen, serta menyertakan catatan dalam bahasa alami untuk membantu mereka memanfaatkan hasil satu sama lain.
- Lebih dari 30.000 teorema pendukung
- Total konsumsi mencapai miliaran token
- Akhirnya terbukti sekitar 13 juta baris
Fokus pada yang dapat diverifikasi, bukan teorema baru
Fokus pencapaian ini bukan pada penemuan teorema matematis baru, tetapi pada mengubah bukti-bukti besar yang sudah ada menjadi versi yang dapat diverifikasi secara bertahap oleh komputer. Seiring dengan meningkatnya jumlah makalah matematika dan konten yang dihasilkan AI, biaya pemeriksaan manual terhadap setiap bukti juga meningkat, sehingga alat formalisasi semakin mendapat perhatian.
Anthropic juga menyatakan bahwa bukti ini berukuran lebih dari lima kali lipat dari perpustakaan bersama yang umum digunakan di bidang matematika, Mathlib. Dokumen lengkap telah diunggah ke GitHub, memungkinkan para peneliti untuk terus memeriksa struktur dan kebenarannya baris demi baris.