Axiom, yapay zekâ ajanlarının Sonlu Basit Grupların Sınıflandırması’nı Lean’de biçimselleştirdiğini söylüyor

Yapay zekâ matematiği şirketi Axiom, X’te Sonlu Basit Grupların Sınıflandırması’nın Lean ile tamamen otomatik biçimselleştirildiğini duyurdu. Şirket bu sonucu “simetrinin periyodik tablosu” olarak nitelendiriyor. Axiom, özgün kanıtın nesiller boyunca 100’den fazla matematikçi tarafından yazılmış yaklaşık 15.000 sayfadan oluştuğunu belirtiyor ve bunun bilgisayar tarafından doğrulanan tarihin en büyük matematik kanıtı olduğunu söylüyor.

Axiom’un açık kaynak deposuna göre, yapay zekâ ajanlarından oluşan sürüler 24 günde yaklaşık 43,1 milyon satır Lean üreterek 715 makale ve kitabı kapsadı ve yayımlanmış kayıttan 34 sapma tespit etti. Yapay zekâ haber hesabı TestingCatalog’un bir paylaşımında, ajanların işi yazılım ekipleri gibi bölüştüğü ve Lean’in denetleyebileceğinden daha hızlı kod yazdığı da belirtiliyor.

Bu rakamlar Axiom’un kendi açıklamasına dayanıyor; duyuru kapsamında biçimselleştirmenin bağımsız bir incelemesi yapılmış değil. Paylaşım, 28 Ekim itibarıyla X’te yaklaşık 6.200 beğeni almıştı.