Matematikçiler Fermat'ın Son Teoremini Formalize Etmek İçin Yapay Zekayı Kullanıyor
Matematikçiler, matematiğin en ünlü problemlerinden biri olan Fermat'ın Son Teoremini formalize etmek için yapay zekayı kullanmaya başladı. Sonuçlar, hız açısından beklentileri aştı.
Fermat'ın Son Teoremi, ilk olarak 1637'de Pierre de Fermat tarafından ortaya atıldı ve şöyle diyor: a, b ve c herhangi bir n > 2 tamsayısı için aⁿ + bⁿ = cⁿ denklemini sağlayan üç pozitif tamsayı yoktur. Teorem, 1995'te Andrew Wiles tarafından ünlü bir şekilde kanıtlandı, ancak matematikçiler şimdi bu kanıtın tamamen formal, makine tarafından doğrulanabilir bir versiyonunu yapay zeka araçlarını kullanarak oluşturmak için çalışıyorlar.
Bu ilerleme, Londra'da düzenlenen bir etkinlikte duyuruldu. Araştırmacılar, yapay zeka sistemlerinin matematiksel kanıtları bilgisayarların mantıksal doğruluğu kontrol edebileceği formatlara dönüştürme sürecinde yardımcı olabileceğini gösterdi. Bu formalizasyon süreci, emek yoğun olmakla birlikte, gizli boşluk veya varsayım olasılığını ortadan kaldırarak matematiksel akıl yürütmede mutlak kesinlik sağlıyor.
Beklenenden hızlı ilerleme, yapay zeka araçlarının karmaşık matematiksel akıl yürütmeyi ele alma konusunda giderek daha yetenekli hale geldiğini düşündürüyor. Bu durum, matematikte diğer ünlü çözülmemiş problemleri doğrulama ve keşfetme için yeni yollar açabilir.