Fermat'nın Son Teoremi — n 2'den büyük üsler için xⁿ + yⁿ = zⁿ denkleminin tamsayı çözümü olmadığı ifadesi — Pierre de Fermat'ın 1640 civarında ünlü "marj çok dar" notunu düşmesinden sonra matematikçilere 350 yıldan uzun süre direndi. Andrew Wiles nihayet 1990'ların ortasında kanıtladı. Şimdi Anthropic, Claude ajanlarından oluşan bir sürünün hiçbir insan ekibinin tamamlayamadığı bir işi yaptığını söylüyor: o ispatı, bir bilgisayarın adım adım denetleyebileceği bir biçime çevirmek.
Şirkete göre, büyük ölçüde özerk çalışan düzinelerce Claude ajanı, Fermat'nın Son Teoremi'nin Lean ispat asistanındaki ilk eksiksiz, makineyle doğrulanmış biçimselleştirmesini üretti — yaklaşık 29.500 ara teorem içeren kabaca 13 milyon satır Lean kodu. Çalışma 11 gün sürdü. Columbia Üniversitesi'nde yapay zekâ destekli biçimselleştirme araçları geliştiren Tianyi Peng'in grubu, ara sıra yüksek düzeyli talimatlar vererek çabayı yönetti; gerisini ajanlar halletti.
Lean hem bir programlama dili hem de bir doğrulama sistemidir. Matematiksel bir iddia ve türetimi kod olarak yazılır; Lean bunu sabit bir mantıksal kurallar kümesine karşı denetler. Zincirdeki tek bir halka eksikse ispat derlenmez. Amaç da budur: güven, insan denetçilerin titizliğinden küçük ve denetlenmiş bir mantık çekirdeğine kayar.
Şirket, ilk denemelerin birçoğunun başarısız olduğunu söylüyor: ilk ajan ekipleri kısmi ilerleme kaydetti ancak projenin genel durumunu gözden kaçırdı ve etkin biçimde işbirliği yapmayı bıraktı. Atılım ancak Peng ve Columbia'daki meslektaşlarının geliştirdiği açık bir biçimselleştirme platformu olan Prove2Me'ye geçişten sonra geldi. Platform, teorem ifadelerinin yönlü asiklik bir grafiğini tutuyor; ajanlar sıradaki ispatlara karar verirken bunu kullanıyor — bellek yitimine karşı koymak ve paralel çalışmayı mümkün kılmak için tasarlanmış bir düzenek.
Çabanın ölçeği çarpıcı. Anthropic, ajan ekibinin yaklaşık altı milyar çıktı token'ı tükettiğini söylüyor; dışarıdan gözlemciler bunun 100.000 ila 300.000 dolar arası hesaplama maliyeti anlamına geldiğini tahmin ediyor. Bir yan deney çok daha küçük bütçelerin işe yarayabileceğini gösteriyor: yalnızca üç özel Claude Max aboneliğiyle ajanlar, Vinogradov'un üç asal sayı teoremini üç günde biçimselleştirdi.
Biçimselleştirme, Wiles'ın ispatının Darmon, Diamond ve Taylor'a göre sadeleştirilmiş bir sürümünü izliyor ve kod, yazılı bir açıklamayla birlikte Anthropic'in GitHub deposunda kamuya açık. Londra Imperial College'da Fermat'nın Son Teoremi'ni biçimselleştirmek için 2024'ten beri süren ve Eylül 2029'a kadar finanse edilen bir topluluk projesine liderlik eden Kevin Buzzard çalışmayı inceledi. Kodu kendisi derledi ve karşılaştırma aracını çalıştırdı; doğrulama geçiyor. Buzzard, Xena Project blogunda bunu modern matematik literatürünün otomatik biçimselleştirilmesine doğru büyük bir adım olarak nitelendiriyor — ancak ispatın erken literatürünü izlediği için matematiksel olarak yeni bir şey eklemediğini de vurguluyor.
Bu başarı, yapay zekânın matematikteki son dönemdeki karışık siciline oturuyor. 2024'te DeepMind'ın AlphaProof ve AlphaGeometry 2 modelleri Uluslararası Matematik Olimpiyatı'nda gümüş madalya seviyesine ulaştı. Nisan 2026'da 23 yaşında bir kişi, GPT-5.4 Pro'ya tek bir komutla 60 yıllık bir Erdős problemini çözdü; ispat daha sonra Lean'de doğrulandı. Kısa süre sonra OpenAI'nin dahili bir akıl yürütme modeli, düzlemsel birim mesafe problemiyle ilgili 80 yıllık bir varsayımı çürüttü — ancak inceleyen matematikçiler, argümanın geriye dönük bakıldığında başka yazarlara atfedilebilecek fikirlere dayandığını belirtti.
Biçimsel matematik için mesaj, altyapının ham model yeteneği kadar önemli olabileceği: Fermat biçimselleştirmesindeki belirleyici unsur, daha akıllı bir model değil, Prove2Me'nin planlama grafiği gibi görünüyor. Daha geniş alan içinse, ünlü bir teoremin ispatının iki haftadan kısa sürede, küçük bir araştırma bursuna denk bir maliyetle yapay zekâ ajanlarınca makineyle denetlenebilmesi, bir ispatı "doğrulamanın" ne anlama geldiğini ve matematik literatürünün ne kadarının bilgisayarla denetlenen bir zemine oturtulabileceğini yeniden çerçeveliyor.
