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

> Yaklaşık 15 bin sayfalık ispat, 24 günde yaklaşık 43,1 milyon satırlık Lean koduna dönüştü. Ajanlar yayımlanmış ispatlarda 34 sapma buldu.

- Yayın: JARRUS (@jarrus.ai), thejarrus.com
- Haber tarihi: 27 Ekim 2026 (2026-10-27)
- Sitede: 2026-10-29
- Etiketler: Araştırma, Ajanlar
- Adres: https://thejarrus.com/tr/haber/axiom-cfsg/

### 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.

![Sonlu basit grupların periyodik tablosu: devirli ve alterne gruplar, on altı Lie tipi aile ve 26 sporadik grup](https://thejarrus.com/gorsel/c59-sonlu-basit-gruplar-tablosu.webp)
*Görsel: [Axiom, Formalizing the Enormous Theorem](https://axiommath.ai/research/the-enormous-theorem-formalized/) (26 Ekim 2026). Kaynakları S. D. Smith ve ATLAS of Finite Group Representations.*

https://x.com/axiommathai/status/2115089794867040584

### 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ı.

![Galois'dan Lean'e sonlu basit grupların sınıflandırmasındaki kilometre taşları, 1832-2026](https://thejarrus.com/gorsel/c59-galoisten-leane.webp)
*Görsel: [Axiom](https://axiommath.ai/research/the-enormous-theorem-formalized/) (26 Ekim 2026). 1950 öncesi eksen sıkıştırılmış.*

### 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ı.

![Axiom'un 2-25 Ekim 2026 arasında tamamlanan kilometre taşı sayısı, 108'de 108'e ulaşan çizgi](https://thejarrus.com/gorsel/c59-24-gunluk-ilerleme.webp)
*Grafik: [Axiom](https://axiommath.ai/research/the-enormous-theorem-formalized/) (26 Ekim 2026). Ana daldaki gün sonu sayıları; gri alanlar duraklamalar.*

### 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ı.

## Kaynaklar

1. [Axiom: Formalizing the Enormous Theorem, 26 Ekim 2026](https://axiommath.ai/research/the-enormous-theorem-formalized/)
2. [Axiom (X): Duyuru gönderisi ve ekiple röportaj videosu, 27 Ekim 2026](https://x.com/axiommathai/status/2115089794867040584)
3. [GitHub: AxiomMath/CFSG, 27 Ekim 2026](https://github.com/AxiomMath/CFSG)

Hata bildirimi: hata@thejarrus.com