Axiom, 43,1 milyon satırlık Lean kanıtıyla “muazzam teoremi” biçimselleştirdi

Neler değişiyor?

Axiom Math, 26 Ekim tarihli açıklamasında sonlu basit grupların sınıflandırmasının ilk eksiksiz bilgisayar denetimli kanıtını yayımladığını bildirdi. Şirkete göre mühendis ve matematikçilerin yönettiği onlarca yapay zekâ ajanı, 24 günde Lean kanıt asistanında yaklaşık 43,1 milyon satır kod üretti. “İlk” ve “eksiksiz” nitelemeleri Axiom’un beyanı; bağımsız akademik doğrulama yerine yayımlanan kanıt ve bağımlılık grafiği incelenebilir durumda.

Çalışma, yaklaşık 15 bin sayfa ve 500’den fazla makaleye yayılan sonlu basit grupların sınıflandırmasını biçimsel bağımlılıklara çevirdi. Axiom, süreçte yayımlanmış kayıttan 34 önemli sapma belirlediğini; en büyük sorunun Unbalanced Group Theorem çevresinde olduğunu ve bu bölüm için yeni bir grup kuramı sonucu geliştirdiğini söylüyor.

Projenin önemi yalnız kanıtın boyutu değil, ajanların ortak bir kanıt haritasındaki görevleri bölüşmesi. İnsan uzmanlar şüpheli adımları incelerken Lean her çıkarımı denetliyor; bu yapı, bilimsel ajanlarda sonuç sayısından çok izlenebilir bağımlılık ve doğrulanabilir teslimatın önemini gösteriyor.