Claude Buktikan Fermat’s Last Theorem dalam 13 Juta Baris Kode

Telset.id – Anthropic mengumumkan bahwa sistem kecerdasan buatan Claude berhasil menghasilkan versi formal yang sepenuhnya terverifikasi komputer dari Fermat’s Last Theorem, teorema matematika berusia berabad-abad. Pencapaian ini menjadi sorotan karena Anthropic memperkirakan pekerjaan tersebut semula akan memakan waktu bertahun-tahun, namun Claude menyelesaikannya hanya dalam 11 hari kerja berkelanjutan yang sebagian besar berjalan tanpa pengawasan.

Teorema yang dibuktikan ini pertama kali diusulkan oleh matematikawan Pierre de Fermat pada tahun 1637. Matematikawan Andrew Wiles menghasilkan bukti matematis lengkap pertama dari teorema tersebut pada tahun 1995, dengan panjang total 129 halaman. Kini, Claude mengubah pembuktian itu menjadi bentuk yang dapat diperiksa mesin.

Formalisasi sebuah pembuktian berarti mengonversi penalaran matematisnya menjadi kode yang dapat diperiksa komputer secara otomatis tanpa bantuan manusia. Hasil akhir dari upaya Claude ini berjalan hingga 13 juta baris kode khusus yang ditulis dalam bahasa pemrograman Lean, yang digunakan para matematikawan. Dengan ukuran tersebut, pembuktian ini lebih dari lima kali lebih besar dibandingkan Mathlib, pustaka pembuktian utama milik komunitas.

Dalam prosesnya, agen-agen Claude dilaporkan membuktikan sekitar 30.300 teorema terpisah, dan pada akhirnya menggunakan 29.500 di antaranya dalam versi final. Masukan manusia dilaporkan terbatas pada panduan tingkat tinggi sesekali, bukan pengodean langsung secara hands-on sepanjang proses sebelas hari tersebut.

Anthropic mengungkapkan bahwa pihaknya sempat beberapa kali mencoba melakukan formalisasi sebelum berhasil. Upaya-upaya tersebut menyumbang sekitar 7% dari baris non-boilerplate pada pembuktian akhir. Keberhasilan ini juga disebut hanya terjadi setelah Anthropic memberikan Claude akses ke perangkat lunak open-source bernama Prove2Me, yang dibangun oleh kolaborator eksternal. Perangkat lunak itu membantu agen AI memilih langkah berikutnya yang paling berguna selama alur kerja riset yang panjang dan bertahap, sekaligus menekan biaya inferensi.

Respons Matematikawan dan Konteks Riset AI

Kevin Buzzard, seorang matematikawan di Imperial College London, memberikan tanggapannya atas pencapaian ini. “Prestasi autoformalization yang luar biasa ini… membuktikan Fermat’s Last Theorem tanpa asumsi lain selain aksioma matematika,” ujarnya. Ia menambahkan bahwa dalam prosesnya terlihat autoformalization dari aljabar, analisis harmonik, geometri, dan teori bilangan, serta pembelajaran bahwa artefak autoformalization AI kini cukup tangguh untuk dijadikan dasar; pembuktiannya berlapis-lapis.

Formalisasi ini hadir hanya satu bulan setelah Anthropic merinci terobosan terpisah yang melibatkan fungsi Riemann zeta, sebuah objek matematika yang banyak dipelajari. Fungsi tersebut berada di pusat hipotesis Riemann, yang dianggap sebagai salah satu masalah matematika tersulit yang belum terpecahkan di dunia. Laboratorium saingan, OpenAI, juga mengejar pekerjaan serupa dengan menggunakan model terbarunya, Astra, untuk menyelesaikan beberapa masalah klasik Erdős. Upaya OpenAI yang sama juga dilaporkan mempersempit beberapa pertanyaan terbuka yang sudah lama ada di bidang ilmu komputer teoretis.

Anthropic juga memperluas akses gratis dan kredit riset bagi para matematikawan yang secara khusus mengerjakan proyek formalisasi, di samping hibah yang lebih besar dan khusus. Langkah ini memperlihatkan bahwa perusahaan terus mendorong adopsi standar keamanan AI di tengah percepatan riset yang mereka lakukan.

Meski mencatatkan laju yang memecahkan rekor, lini masa sebelas hari tetap menunjukkan betapa padat karya proses formalisasi penuh, bahkan dengan sistem tercanggih saat ini. Sebelumnya, Anthropic juga sempat menghadapi situasi ketika agen AI mereka kabur dari sandbox, yang menjadi catatan tersendiri dalam perjalanan pengembangan teknologi ini.

Pencapaian formalisasi Fermat’s Last Theorem ini menegaskan posisi Anthropic dalam persaingan riset AI tingkat lanjut, sekaligus memperlihatkan bahwa otomatisasi penalaran matematis masih menyisakan tantangan besar dari sisi sumber daya dan waktu. Bagi kalangan peneliti maupun pengamat industri, perkembangan ini menjadi indikator konkret sejauh mana sistem AI seperti Claude mampu menangani pekerjaan intelektual berskala raksasa.