Anthropic, Fermat'nın Son Teoremi'nin makine denetimli Lean 4 ispatını yayımladı

Tam ve makine denetimli bir ispat

Anthropic, Fermat'nın Son Teoremi'nin Lean 4'te tam ve makine denetimli bir ispatını sunan bir GitHub deposu yayımladı ve depo Hacker News'in ön sayfasında yer buldu. Deponun README'sine göre argüman, sabitlenmiş toolchain sürümleriyle (Lean 4.33.1 — README, bu sürümün 2026 kernel sağlamlık düzeltmelerini içerdiğini belirtiyor) Mathlib üzerine inşa edilmiş klasik Frey, Serre, Ribet, Wiles ve Taylor–Wiles zinciridir. Çalışma Apache License 2.0 altında yayımlandı ve bakımı yapılmayan, katkı kabul etmeyen bir araştırma eseri olarak çerçevelendi.\n Theorems/Thm_fermat_last_theorem.lean dosyasında bildirilen biçimselleştirilmiş ifadeye göre, 3 ≤ n olan her doğal sayı n ve tüm pozitif doğal a, b ve c sayıları için a^n + b^n ≠ c^n. README, ifadenin Lean'ın yerleşik doğal sayılarını ve aritmetiğini kullandığına dikkat çekiyor — tek Mathlib bileşeni ℕ üzerindeki kuvvet alma işlemi, ki Mathlib bunu zaten Lean'ın kendi tanımı olarak tanımlıyor — ve varsayılan build hedefi ayrıca Mathlib'in FermatLastTheorem ifadesini bu sonuçtan türetiyor.

Üç katmanlı denetim

README, bağımsız olarak tekrarlanabilir olacak şekilde tasarlanmış bir doğrulama zincirini anlatıyor. Sıfırdan yapılan bir lake build 60.475 modülün tamamını derledi ve her bildirim Lean kernel tarafından denetlendi. Varsayılan hedef, kanıtın yalnızca Lean'ın üç standart aksiyomuna — propext, Classical.choice ve Quot.sound — dayanması gerektiğini #guard_msgs ile zorunlu kılıyor ve bir tarama, paketlenmiş hiçbir modülde sorry, eklenmiş aksiyom, native_decide ya da başka bir kaçış yolu bulamadı.

İkinci bir araç olan leanprover'un karşılaştırıcısı, kanıtlanan ifadeyi yalnızca Mathlib kullanılarak yazılmış bir challenge dosyasıyla karşılaştırdı; ifadenin ve andığı her sabitin challenge ile eşleştiğini ve tüm ispatın (Mathlib dahil) kernel üzerinden yeniden oynatıldığını doğruladı. README'de alıntılanan hükmü şu: "Your solution is okay!"

Üçüncü olarak, Rust ile yazılmış bağımsız bir Lean kernel olan nanoda, ortamın tamamının bir export'unu kabul etti ve 1.052.234 bildirimi hatasız biçimde denetledi. Yazarlar, nanoda'ya ilerleme çıktısı ve daha hızlı tanımsal-eşitlik araması için dört küçük yama uyguladı ve hiçbirinin bir typing kuralı eklemediğini, çıkarmadığını ya da zayıflatmadığını belirtiyor.

README neyin denetlenmediği konusunda açık sözlü: sonuç, kernel'e (ya da nanoda'ya) ve denetim araçlarına duyulan güvene bağlı olarak geçerli ve hiçbir araç, her ara teoremin adının ima ettiği şeyi gerçekten kanıtlayıp kanıtlamadığını doğrulayamaz. PROOF-PATH.md, her klasik adımı onu taşıyan Lean teoremine eşliyor. Yeniden üretim hafif sayılmaz — referans build 96 paralel iş ve 153 GB bellek zirvesiyle 5 saat 32 dakika sürdü ve karşılaştırıcı çalışması yaklaşık 15 saat aldı.

Topluluk temelleri üzerinde yapay zeka ajanları

README'ye göre Lean kaynakları, insanlar tarafından yazılmış açık kaynak Lean üzerine inşa eden ve "hakem olarak Lean'ı" kullanan yapay zeka ajanları tarafından üretildi ve okunmakrather than denetlenmek için yazıldı: adlar makine tarafından üretiliyor ve matematiksel anlam değil pipeline etiketleri taşıyor. Proje, Kevin Buzzard öncülüğündeki Imperial College London FLT projesinden malzeme içeriyor — Frey paketi, Galois temsilleri, deformasyon teorisi ve patching — ayrıca Kummer teoreminin flt-regular ispatı ve Mathlib; ATTRIBUTION.md, ödünç alınmış malzeme içeren 106 dosyayı listeliyor. Yaklaşık 390 MB'lık bir html/ klasörü her şeyi çevrimdışı web sayfaları olarak sunuyor; 29.511 teoremin her biri için genişletilebilir bağımlılık grafikleri içeren bir sayfa dahil.

Çelişkili bir anlatı

İki kaynak ayrılıyor. Depo ortaya çıkmadan dakikalar önce yayımlanan bir dev.to yazısı, FLT'nin Lean'da biçimselleştirilmesinin Buzzard öncülüğünde süren bir topluluk çabası olduğunu, Best ve çalışma arkadaşlarının 2025 tarihli makalesinin yalnızca regüler asal sayılar özel durumunu kapsadığını ve Claude'nun belgelenmiş Lean çalışmalarının Riemann zeta fonksiyonuyla ilgili bir sonuçla sınırlı olduğunu savunuyor — dolayısıyla tamamlanmış bir FLT biçimselleştirmesi Claude'ya atfedilmemeli. Anthropic hesabı altında yayımlanan ve Imperial College projesine açıkça dayanan depo, bu değerlendirmeden sonra ortaya çıktı ve belirli bir model adı vermiyor. Tam da bir kuşkucunun isteyeceği çözümü davet ediyor: build'leri ve denetleyicileri yeniden çalıştırın ve makinelerin neyi kabul ettiğine bakın.

Neden önemli

Denetimler bağımsız yeniden üretimden sağlam çıkarsa, matematiğin en ünlü teoremlerinden biri tamamen makine denetimli bir ispata sahip küçük gruba katılıyor ve güven tabanı, ikinci bir kernel ile çapraz denetlenen Lean kernel, üç standart aksiyom ve kısa bir araç listesine daralıyor. Bu, saf matematiğin ötesinde önemli: kod insanlar ya da yapay zeka ajanları tarafından yazılmış olsun, ölçekte doğruluğun okunabilirlik veya itibar yoluyla değil, doğrulama yoluyla nasıl tesis edilebildiğini gösteriyor. Kanıt asistanları açısından, bu boyutta bir proje kernel'leri, karşılaştırıcıları ve export araçlarını pratikte sınıyor. Ve yapay zeka destekli matematik için faydalı bir emsal oluşturuyor: teslim edilen şey makul görünen bir metin değil, makinenin kabul ettiği bir ispat ve kalan varsayımlar açıkça beyan edilmiş durumda.