Axiom, matematik tarihinin en uzun ispatı olan sonlu basit grupların sınıflandırmasını yapay zekâ ajanlarıyla Lean’de doğruladı

Simetrinin periyodik tablosu

Yapay zekâ girişimi Axiom, 26 Ekim’de yayımladığı yazıda ve ertesi gün X’teki duyurusunda, Sonlu Basit Grupların Sınıflandırması’nı (CFSG) Lean ispat dilinde bilgisayarla doğruladığını açıkladı. Şirket bunu, bu teoremin ilk eksiksiz bilgisayar denetimli ispatı olarak tanımlıyor.

Teorem, sonlu grupların “atomları” sayılan sonlu basit grupların tam listesini veriyor: asal mertebeli devirli gruplar, en az beş sembol üzerindeki alterne gruplar, sonlu cisimler üzerindeki on altı Lie tipi grup ailesi ve 26 sporadik grup. Sporadik grupların en büyüğü, yaklaşık 8,08 × 10⁵³ elemanlı Canavar (Monster) grubu.

Axiom@axiommathai

İnsanlık tarihinin en büyük matematik ispatı artık bilgisayarla doğrulandı.

Axiom bugün, "simetrinin periyodik tablosu" olan Sonlu Basit Grupların Sınıflandırması'nın Lean'de eksiksiz otomatik biçimselleştirmesini duyuruyor.

Yaklaşık 15.000 sayfa; kuşaklar boyunca 100'den fazla matematikçi tarafından kuruldu.

İngilizceden çevrildi·Orijinalini göster

Yarım asırlık bir ispat

Axiom’a göre özgün ispat yaklaşık 100 matematikçinin 500’den fazla makalesine yayılıyor ve yaklaşık 15 bin sayfa tutuyor. Yol haritası 1954’te Brauer’in involüsyonların merkezleyicileri üzerine konuşmasıyla başladı. 1963’te 255 sayfalık Feit-Thompson teoremi geldi, Gorenstein 1972’de on altı adımlık programını açıkladı ve 1983’te sınıflandırmanın tamamlandığını duyurdu. Ancak “quasithin” durumdaki bir boşluk ancak 2004’te, Aschbacher ve Smith’in 1.221 sayfalık çalışmasıyla kapandı. İkinci nesil, daha düzenli bir ispat 1990’lardan beri yazılıyor; 2023’te onuncu cildi çıktı.

Feit-Thompson teoremi 2012’de Inria’dan Georges Gonthier ve arkadaşlarınca Coq (bugün Rocq) ispat yardımcısında doğrulanmıştı. Teoremin tamamı ise şimdiye kadar bilgisayarda doğrulanmamıştı.

Yapay zekâ ajanlarıyla 24 gün

Çalışma 1 Ekim’de başladı, ilk ajan sürüsü 2 Ekim’de devreye girdi ve 108 kilometre taşının hepsi 25 Ekim’de tamamlandı. Axiom’un AxiomProver sistemi üzerinde onlarca yapay zekâ ajanından oluşan sürüler çalıştı. İş 108 kilometre taşına ve yaklaşık 380 göreve bölündü. Öncü ajanlar argümanları parçalara ayırıp ifadeleri gözden geçirdi; diğerleri var olan sonuçları aradı ya da Lean ispatları yazdı. İnsan matematikçiler takılma noktalarını inceledi, mühendisler sistemi ayakta tuttu.

Sonuçta yaklaşık 43,1 milyon satırlık Lean kodu ortaya çıktı; bunun yaklaşık 1,2 milyon satırı daha önceki Qiuzhen-CFSG projesinden alındı. 10 Ekim’de Canavar grubunun basit olduğu ispatlandı. Süreç pürüzsüz değildi: ajanlar bazı ön koşulları ispatlamadan varsaydığı için on binlerce satır silindi ve 13 Ekim’de yalnızca bir kilometre taşı kapanınca plan yeniden yapıldı.

Yayımlanmış ispatlarda 34 sapma

Ajanlar yayımlanmış literatürde 34 kayda değer sapma buldu. Çoğu yazım hatası, tablo hatası ya da düşürülmüş bir hipotez gibi küçük sorunlardı. En önemlisi Walter’ın Dengesiz Grup Teoremi (UGT) ispatındaydı: ajanlar bir kapanma iddiasına karşı örnekler buldu, örneğin PSL₂(49) grubu. Bu karşı örnekler teoremi çürütmedi, ancak kilit bir çıkarımı gerekçesiz bıraktı. AxiomProver alternatif bir argüman ve “basit tepelerin korunması” adlı yeni bir grup teorisi sonucu üretti; Axiom matematikçileri daha sonra bu sonuca gerek duymayan daha kısa bir yol da buldu.

Aschbacher ve Smith’in quasithin çalışmasındaki bir lemmada iddia edilen eşitliğin SL₂(5) grubu için yanlış olduğu görüldü ve eşitlik bir eşitsizlikle değiştirildi. Bulunan hatalar, Richard Lyons ve Ronald Solomon’dan oluşan bir danışma kuruluyla düzeltilecek.

Çekinceler

Çalışma, ikinci nesil ispat tamamlanmadığı için ilk nesil ispatı izliyor. Lean her adımı denetliyor, ancak biçimsel ifadenin teoremi tam karşılayıp karşılamadığı insan incelemesine bağlı; Axiom da ilerlemenin abartılmaması gerektiği konusunda uyarıyor. Kod GitHub’da Apache 2.0 lisansıyla açık ve henüz bağımsız bir doğrulama yapılmadı.