Anthropic menyatakan bahawa Claude telah menyelesaikan bukti formal pertama bagi Teorem Terakhir Fermat. Ini bukanlah penemuan semula teorem tersebut, tetapi pengalihan bukti yang sudah ada menjadi kod logik yang boleh disemak langkah demi langkah oleh komputer. Syarikat tersebut mengatakan bahawa kerja ini mengambil masa 11 hari dan menghasilkan sebanyak 13 juta baris akhir.
Maksud bukti formal ialah menulis hujah matematik dalam bahasa yang boleh diperiksa oleh mesin. Bukti dalam kertas tradisional sering memerlukan semakan rakan sebaya yang panjang; sekiranya terdapat kelemahan di mana-mana langkah, proses pembaikannya mungkin berterusan selama berbulan-bulan atau bahkan bertahun-tahun. Teorem Terakhir Fermat dibuktikan oleh ahli matematik British Andrew Wiles pada tahun 1995, tetapi menukar seluruh bukti ini kepada versi yang boleh diperiksa oleh mesin masih dianggap sebagai projek kejuruteraan yang sangat intensif.
11 hari menyelesaikan matlamat projek jangka panjang
Ahli matematik Imperial College London, Kevin Buzzard, telah mendorong projek berkaitan sejak 2024, dengan matlamat yang sama iaitu menukar bukti Wiles ke dalam pembantu bukti Lean. Menurut pelan asal, kerja ini memerlukan kerjasama jangka panjang, dan pendanaan telah diatur hingga tahun 2029.
Anthropic menyatakan bahawa Claude telah menyelesaikan sasaran serupa lebih awal. Selepas ditinjau oleh Buzzard, bukti ini boleh berdiri tanpa bergantung kepada andaian tambahan, iaitu hanya berdasarkan sistem aksiom paling asas matematik.
Diselesaikan secara selari oleh pelbagai agen
Menurut Anthropic, pasukan penyelidik Universiti Columbia yang dipimpin oleh Tianyi Peng membolehkan beberapa agen Claude beroperasi secara selari, masing-masing bertanggungjawab menulis definisi dan membuktikan kesimpulan kecil, kemudian menyusunnya secara bertahap menjadi struktur bukti yang lebih besar. Intervensi manusia adalah minimum, terutama hanya memberikan urutan keutamaan peringkat.
Perkembangan awal tidak berjalan lancar. Anthropic menyatakan bahawa sebahagian agen sementara tidak dapat berkongsi kandungan yang telah selesai, dan juga mengulangi kerja yang sama. Selepas itu, pasukan menggunakan alat bernama Prove2Me untuk memberikan senarai tugas dan cara pengurusan fail yang seragam kepada setiap agen, serta menyimpan catatan bahasa semula jadi untuk membantu mereka memanfaatkan hasil satu sama lain.
- Lebih daripada 30,000 teorem sokongan
- Jumlah penggunaan mencapai berbilion token
- Akhirnya dibuktikan sebanyak 13 juta baris
Fokus pada yang boleh diverifikasi, bukan teorem baru
Fokus kejayaan ini bukan pada penemuan teorem matematik baharu, tetapi pada penukaran bukti-bukti penting yang sudah ada menjadi versi yang boleh disemak langkah demi langkah oleh komputer. Seiring dengan peningkatan jumlah kertas matematik dan kandungan yang dihasilkan oleh AI, kos semakan manual terhadap bukti-bukti juga meningkat, menjadikan alat formalisasi semakin diperhatikan.
Anthropic juga menyatakan bahawa bukti ini lebih besar daripada 5 kali ganda perpustakaan bersama yang biasa digunakan dalam kalangan komuniti matematik, Mathlib. Dokumen penuh telah diunggah ke GitHub, membolehkan penyelidik meneruskan pemeriksaan berperingkat-peringkat terhadap struktur dan kebenarannya.