Fermat'ın Son Teoremi, 17. yüzyıldan bu yana matematikçilerin peşini bırakmayan bir problem olarak tarihe geçti. Pierre de Fermat'ın 1637'de kenar notuna düştüğü bu iddia — n ikiden büyük bir tam sayı olduğunda, xⁿ + yⁿ = zⁿ denkleminin pozitif tam sayı çözümü bulunmadığı — ancak 1995'te Andrew Wiles tarafından yaklaşık 150 sayfalık devasa bir matematiksel çalışmayla kanıtlanabildi.
Ancak bu ispatın doğrulanması, matematikçiler için bile zorlu bir süreçti. 'Biçimsel doğrulama' olarak adlandırılan alanda ise amaç, bu tür matematiksel ispatları bilgisayarların hata aramadan doğrulayabileceği yapılandırılmış bir dile çevirmek. Bu sürecin Wiles'ın ispatı için yıllarca süreceği tahmin ediliyordu.
Anthropic'in Claude yapay zeka modeline dayanan ajan sistemi, bu görevi yalnızca 11 günde tamamladı. Yapay zeka ajanları, ispatı Lean adlı biçimsel matematiksel ispat diline dönüştürdü. Lean, matematiksel adımların mantıksal tutarlılığını bilgisayarın otomatik olarak denetleyebildiği özel bir programlama ortamı sunuyor.
Bu başarının önemi birkaç açıdan değerlendirilebilir. Birincisi, yapay zekanın soyut ve ileri düzey matematiksel akıl yürütmeyi ne ölçüde kavrayabildiğini gözler önüne seriyor. İkincisi, biçimsel doğrulama alanını demokratikleştirme potansiyeli taşıyor: Daha önce yalnızca küçük bir uzman grubunun altından kalkabileceği bu tür projeler, yapay zeka desteğiyle çok daha hızlı ilerleyebilir hale gelebilir.
Öte yandan uzmanlar, bu sonuca temkinli bir coşkuyla yaklaşılması gerektiğini vurguluyor. Yapay zekanın ürettiği biçimsel kodun matematiksel açıdan tam ve eksiksiz olup olmadığı, bağımsız denetimlerle teyit edilmesi gereken bir husus. Bununla birlikte, 11 günlük bu performans; yapay zekanın yalnızca dil işleme değil, yapısal matematiksel düşünme alanında da ciddi bir potansiyel sergilediğini gösteriyor.
Gelecekte benzer yapay zeka sistemlerinin, henüz ispatlanamamış matematiksel problemlerin biçimsel çerçevesini oluşturmada ya da mevcut ispatların zayıf noktalarını bulmada kullanılabileceği öngörülüyor.