Claude Memformalkan Teorem Terakhir Fermat dalam Lean

Anthropic baru-baru ini telah menyelesaikan satu tugasan penyelidikan yang besar. Sebuah model dalaman telah bekerja selama 11 hari untuk memformalkan Teorem Terakhir Fermat menggunakan bahasa pembuktian Lean 4.

Ini bukanlah satu penemuan matematik yang baharu. Andrew Wiles telah membuktikan teorem ini pada tahun 1995. Apa yang dilakukan oleh Anthropic adalah menterjemah bukti sedia ada tersebut ke dalam kod. Ini membolehkan komputer menyemak setiap langkah logik dengan kepastian mutlak.

Skala projek ini sangat besar: • Model tersebut menghasilkan 13 juta baris kod Lean. • Ia membuktikan 30,300 teorem perantara. • Ia menggunakan hampir 6 bilion token output.

Model tersebut bekerja sebahagian besarnya secara sendirian. Manusia hanya memberikan arahan peringkat tinggi sekali-sekala. Proses tersebut selesai pada tengah malam ketika tiada sesiapa yang memerhati. Sistem tersebut merekodkan kejayaan itu secara automatik.

Dua perkara penting untuk diperhatikan:

  1. Model ini adalah alat penyelidikan dalaman. Anda belum boleh mengaksesnya melalui API. Ia tidak sama dengan model Claude yang anda gunakan hari ini.
  2. Nilai sebenar bagi pembangun terletak pada lapisan penyelarasan yang dipanggil Prove2Me.

Prove2Me ialah alat sumber terbuka. Ia menggunakan graf kebergantungan untuk mengurus tugasan. Berbanding senarai semak yang ringkas, ia mencipta peta tentang bagaimana bukti-bukti tersebut saling berhubung antara satu sama lain.

Struktur ini menyelesaikan dua masalah utama bagi aliran kerja ejen:

  • Ia menghalang beberapa ejen daripada melakukan kerja yang sama.
  • Ia memberikan ejen memori kongsi supaya mereka tidak melupakan matlamat utama.

Kebanyakan aliran kerja ejen gagal kerana mereka hilang jejak konteks dari semasa ke semasa. Penggunaan graf luaran yang dikongsi, berbanding tetingkap sembang yang panjang, dapat memastikan tugasan kekal di landasan yang betul.

Anda patut mengkaji seni bina Prove2Me jika anda membina aliran kerja ejen. Walaupun anda tidak menggunakan model penyelidikan Anthropic, cara mereka menyelaraskan tugasan adalah satu pelan tindakan untuk kerja berjangka panjang.

Source: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36

Optional learning community: https://t.me/GyaanSetuAi