Anthropic: Claude, Fermat'ın Son Teoremi'nin bilgisayarla doğrulanan kanıtını 11 günde yazdı
Anthropic, Fermat'ın Son Teoremi'nin bilgisayarla doğrulanan ilk tam kanıtını yayımladı: Claude, Lean dilinde 11 gün boyunca büyük ölçüde otonom çalıştı.
Ne oldu
Anthropic, Fermat'ın Son Teoremi'nin ilk eksiksiz ve bilgisayarla doğrulanmış kanıtını yayımladı. Şirkete göre Claude, resmî doğrulama için geliştirilen Lean dilinde kanıtı yazmak için 11 gün boyunca büyük ölçüde otonom çalıştı; ortaya 13 milyon satır kod ve 29.500 ara teorem çıktı.
Çalışmayı, Columbia Üniversitesi'ndeki grubu yapay zekâ ile formalizasyon araçları geliştiren Anthropic araştırmacısı Tianyi Peng yönetti. Kanıt GitHub'da açık olarak yayımlandı.
Neden önemli
Fermat'ın, n > 2 için aⁿ + bⁿ = cⁿ eşitliğini sağlayan pozitif a, b, c tam sayıları bulunmadığı iddiası 1637 civarında yazıldı ve Andrew Wiles bunu ancak 1995'te kanıtladı: doğrulanması aylar süren 129 sayfalık bir çalışma. Yapay zekânın Riemann hipotezi üzerine yeni matematik üreten son çalışmasından farklı olarak buradaki yenilik doğrulama: formalize edilmiş bir kanıtı makine kontrol ediyor.
Uzmanlar ne diyor
Teoremin formalizasyonu için yıllardır süren topluluk çalışmasını yöneten Imperial College London'dan Kevin Buzzard, bunu "olağanüstü bir otoformalizasyon başarısı" olarak nitelendirdi: teorem, matematiğin aksiyomlarından başka varsayım olmadan kanıtlandı. Anthropic'e göre sonuç, matematiksel bilginin kontrol edilmesinin ve ona güvenilmesinin daha kolay olacağı bir geleceğe işaret ediyor.