Axiom Math, Grup Sınıflandırmasının Lean’deki 43,1 Milyon Satırlık Kanıtını Yayımladı

Axiom Math, 27 Ekim 2026’da, Sonlu Basit Grupların Sınıflandırması’nın bilgisayar tarafından denetlenmiş ilk eksiksiz kanıtı olarak nitelendirdiği çalışmayı yayımladığını duyurdu. Mühendisler ve matematikçiler, düzinelerce yapay zekâ ajanından oluşan sürüleri yönlendirerek bu çalışmayı 24 günde ortaya çıkardı; ajanlar Lean kanıt asistanında yaklaşık 43,1 milyon satır kod yazdı.

Şirket, duyurusunda şöyle yazdı: “Bugün, Sonlu Basit Grupların Sınıflandırması’nın (CFSG) bilgisayar tarafından denetlenmiş ilk eksiksiz kanıtını yayımlıyoruz.” Bu sınıflandırma, sonlu grupların temel yapı taşlarını tanımlar. Özgün kanıt, yaklaşık 100 matematikçinin 500’den fazla makalesinde toplam yaklaşık 15.000 sayfaya yayılır; bu kapsamı nedeniyle devasa teorem lakabını kazanmıştır.

Axiom’ın Yayımladığı Kanıt

CFSG, her sonlu basit grubun asal dereceli çevrimsel bir grup, en az beş sembol üzerinde tanımlı bir alternatif grup, sonlu cisimler üzerinde kurulan Lie tipi grupların on altı sonsuz ailesinden birine ait bir grup ya da birbirinden ayrı tam 26 sporadik gruptan biri olduğunu ortaya koyar. Duyuruda, bazı yazarların Tits grubunu 27. grup olarak saydığı da belirtiliyor. En büyük sporadik grup olan Canavar, Robert Griess tarafından 1980’de 196.884 boyutlu bir cebir kullanılarak kuruldu.

İnsanların yürüttüğü kanıtlama çalışmaları onlarca yıla yayıldı. Walter Feit ve John Thompson, 1963’te, Pacific Journal of Mathematics dergisinin bir sayısını bütünüyle dolduran 255 sayfalık bir makalede her değişmeli olmayan sonlu basit grubun mertebesinin çift olduğunu kanıtladı. Daniel Gorenstein, sınıflandırmayı tamamlamak için 1972’de on altı aşamalı bir program ortaya koydu ve 1983’te çalışmanın tamamlandığını duyurdu. Ancak kuasitin durumu, Michael Aschbacher ve Stephen Smith’in 2004’te 1.221 sayfalık bir inceleme yayımlamasına kadar Geoffrey Mason’ın tamamlanmamış bir el yazısına dayanıyordu; bu yayın, sonradan birinci nesil kanıt olarak anılacak çalışmayı tamamladı. Gorenstein ve Richard Lyons’ın başlattığı, daha sonra Ronald Solomon ve Inna Capdeboscq’un da katıldığı daha sistematik ikinci nesil kanıt ise hâlâ tamamlanmadı. Bu nedenle Axiom, birinci nesil kanıtı biçimselleştirdi.

Proje sayfası, biçimselleştirmenin birinci nesil kanıtı izlediğini ve her mantıksal adımın Lean çekirdeği tarafından denetlendiğini belirtiyor; ayrıca 43,1 milyon Lean satırı, 2,05 milyon bildirim ve kaynakçada yer alan 715 makale ile kitap listeleniyor. Axiom, kanıt haritasının ikinci nesil ciltlerden yararlandığını ve biçimselleştirmenin daha önceki Qiuzhen-CFSG projesinden yaklaşık 1,2 milyon satır kod içerdiğini söylüyor. Çalışma ayrıca, yüzlerce katkı sunana atfettiği Mathlib üzerine kurulu. Projenin temel katkı sunanları Dean Cureton, Vasily Ilin, Bhavik Mehta ve Niels Voss; baş araştırmacısı ise Letong Hong.

Herkese açık GitHub deposu, sonucu sürümü 4.35.0-rc3’e sabitlenmiş, Mathlib ve TauCeti projesi üzerine kurulu, yalnızca Classical.choice, propext ve Quot.sound standart aksiyomlarını kullanan ve native_decide içermeyen, sorry kullanılmamış bir Lean4 kanıtı olarak tanımlıyor. TauCeti’den alınan sınıflandırmanın biçimsel ifadesi şöyle: “Her sonlu basit grup, sınıflandırma listesindeki açıkça kurulmuş gruplardan biriyle izomorftur.” README’de, lake build komutunun geliştirmenin tamamını denetlediği belirtiliyor. Ekip, Lake derleme aracında yaptığı ve ana projeye aktarmayı planladığı açık değişiklikler ile optimizasyonlar sayesinde derleme süresini 24 saatin altına indirdi. Kod, Apache-2.0 lisansını taşıyor.

24 Günlük Ajan Sürüsü Çalışması

Axiom, projeyi koordine etmek için 1 Ekim 2026’da bir Slack kanalı açtı. Önceden yapılmış Lean çalışmaları ve yayımlanmış literatürden derlenen şirket içi bir kanıt haritası, çalışmayı 108 kilometre taşına ve yaklaşık 380 daha küçük göreve böldü. İlk ajan sürüsü 2 Ekim 2026’da faaliyete geçti; ajanlar kilometre taşlarını GitHub sorunları üzerinden üstlendi ve tamamladıkları işleri Slack’te bildirdi. Baş ajanlar zorlayıcı argümanları parçalara ayırıp ifadeleri gözden geçirirken diğer ajanlar mevcut sonuçları aradı veya Lean kanıtları yazdı. Bir ajan, eksik ön koşulları başka ajanlara devredebiliyor; bu ajanların sonuçları da ortak bir depoya ekleniyordu.

İlk ilerleme, zayıf noktaları ortaya çıkardı. İlk bakışta yönetilebilir görünen bazı kilometre taşlarının ardında, ajanların kanıtlamak yerine varsaydığı çok kapsamlı ön koşullar vardı. Ekip, bu varsayımlara dayanan on binlerce satır kodu silerek daha sağlam bir planla işe yeniden başladı. İlk kilometre taşlarından biri, aday kanıtı henüz gerekçelendirilmesi gereken yapısal varsayımlara dayanan sinyalizatör funktörü teoremiyle ilgiliydi. Ajanların Lean’in yeniden denetleyebileceğinden daha hızlı kanıt üretmesiyle derleme süreleri de darboğaza dönüştü. Axiom, mühendislerinin önbelleğe alınmış derleme sonuçlarını çalışanlara dağıttığını, bağımsız denetimleri paralel yürüttüğünü ve maliyetli sonlu hesaplamaları ayrı ayrı denetlenebilir sertifikalara dönüştürdüğünü söylüyor. Şirket, bu değişikliklerin doğrulamayı birkaç mertebe hızlandırdığını belirtiyor.

Şirketin aktardığına göre, kanaldaki bir mesaj 10 Ekim 2026’da ajanların Canavar grubunun basit olduğunu kanıtladığını duyurdu. Ajanlar ayrıca Griess cebiri aracılığıyla Canavar’ın varlığını biçimselleştirdi ve Canavar tipi grupları Canavar grubuyla özdeşleştiren bir teorem oluşturdu. 13 Ekim 2026’da yalnızca bir kilometre taşı tamamlandı. Bunun üzerine mühendisler yeniden planlama çalışması başlatarak tamamlanmamış kilometre taşlarını, açık ve kesin biçimde ifade edilmiş daha küçük teoremlere böldü. Her bir ayrıştırmada, parçaların kısa bir Lean kanıtıyla özgün kilometre taşını nasıl ortaya koyacağı gösterilmeliydi.

Yayımlanmış Kanıttaki Açıklar

Axiom’ın bildirdiğine göre, kanıtın Lean’e aktarılması yayımlanmış argümanlardaki sorunları ortaya çıkardı. Bunların çoğu yazım hataları, tablolardaki yanlışlar veya atlanmış varsayımlar gibi küçük sorunlardı; ancak şirket, yayımlanmış metinden kayda değer 34 sapma tespit ettiğini ve bunların en önemlisinin Dengesiz Grup Teoremi’yle (Unbalanced Group Theorem, UGT) ilgili olduğunu belirtiyor.

Buna bir örnek, Aschbacher ve Smith’in kuazi-ince ciltlerindeki bir lemmaydı; lemma, iki sayısal niceliğin eşit olduğunu ileri sürüyordu. Ajanlar, SL₂(5) grubunu içeren bir karşı örnek buldu: ileri sürülen eşitlik bir niceliğin 2 olmasını gerektirirken bu nicelik 1’di. Eşitliği eşitsizlikle değiştirmek lemmayı düzeltti; ancak sonraki argümanlarda bazı durumları elemek için eşitlikten yararlanılmıştı. Bu nedenle ekip, söz konusu durumları da kapsayacak şekilde daha önceki bir argümanı genişletti.

UGT, alt grupları hakkındaki bilgilerden hareketle bir grubun tamamının belirlenmesine yardımcı olur: makalenin özetine göre, sınıflandırmanın tümevarımsal varsayımları altında, bir involüsyonun merkezleyeni içinde normal olan ve önemsiz olmayan tek mertebeli bir alt grup, içinde bulunduğu basit grubun tek karakteristikli Lie tipi bir grup ya da belirli derecelerde bir alternating grup olmasını gerektirir. Axiom, UGT’yi John Walter’ın 1986 tarihli incelemesinden yola çıkarak ele aldı. Ajanları bu argümanı biçimselleştirirken, argümanda kullanılan bir kapanış önermesine açık karşı örnekler buldu: ilişkili basit grupları belirli bir aile içinde tutacağı varsayılan bir işlem, bu aileden açıkça dışlanan bir grup üretebiliyordu.

Şirketin açıklamasına göre, PSL₂(49)’dan başlanınca, cisim involüsyonunun merkezleyeni PGL₂(7) olduğundan, işlem PSL₂(7) basit bileşenini veriyor. 7 bir Mersenne asalı olduğu için bu bileşen aileden dışlanıyor. Axiom, bu karşı örneklerin ne UGT’nin kendisini ne de Walter’ın II.5.9(ii) önermesinin sonucunu çürüttüğünü belirtiyor.

Düzeltme, Axiom’ın açıklamasına göre AxiomProver sisteminin üretip biçimselleştirdiği alternatif argümanın temel fikirlerini sağlayan Solomon’ın 1976 tarihli maksimal 2-bileşenler kuramından yararlandı. Makalede Teorem 2.3 (basit tepelerin korunması) olarak belirtilen kilit adım, Axiom tarafından AxiomProver’ın kanıtladığı, grup kuramında yeni bir sonuç olarak tanımlanıyor. Gilman ve Solomon’ın indirgemeleri ile Foote ve Harris’in tanıma teoremleriyle birlikte bu sonuç, sınıflandırma için gereken UGT’nin basit grup biçimini sağlıyor. Biçimselleştirme tamamlandıktan sonra Axiom matematikçileri, 9.5. Not olarak kaydedilen ve Teorem 2.3’e başvurmadan aynı sonuca ulaşan, ilk nesil yöntemler çerçevesinde daha kısa bir çıkarım buldu.

Colin Defant ve Ken Ono’nun katkıda bulunduğu The Unbalanced Group Theorem adlı bu makale, 27 Ekim 2026’da CC BY 4.0 lisansı altında Hexagon ön baskı sunucusunda 1. sürüm olarak yayımlandı; proje sayfasında 35 sayfa olarak listeleniyor. Axiom, literatürde bulunan düzeltmeleri derlemek için grup kuramcılarıyla birlikte çalıştığını ve bunları projenin düzeltmeler sayfasında yayımlayacağını belirtiyor. Sınıflandırmanın temelini oluşturan çalışmaları yürüten Lyons ve Solomon’a UGT’nin düzeltilmesi konusunda danışıldı. Şirket, onların da yer aldığı bir danışma kuruluyla birlikte düzeltmeleri derlemeyi ve çözüme kavuşturmayı sürdüreceğini; kurulda ayrıca dış danışman Dan Nakano’nun da bulunduğunu söylüyor. Axiom, katkısını kanıtı makinelerce denetlenebilir hâle getirmek, karşılaşılan engelleri belgelemek ve bu engelleri çözen biçimselleştirilmiş argümanlar sunmak olarak tanımlarken, sınıflandırmanın grupları keşfeden ve argümanları geliştiren matematikçilerin başarısı olmaya devam ettiğini belirtiyor.