Axiom Math’ın AI’ı Lean’de 246 Asal Boşluk Teoremini Doğruluyor

Axiom Math, AxiomProver sisteminin asal sayılar arasındaki boşluklarla ilgili bilinen en güçlü sonucu, yani asal çiftlerinin sonsuz sayıda 246’dan daha fazla fark göstermediği teoremini, makine tarafından denetlenmiş bir Lean 4 kanıtı ürettiğini söylüyor. Şirket, bu sonucu 17 Ağustos 2026’da 41 isimli matematik, mühendislik ve ana araştırmacı katkıda bulunanı içeren etkileşimli bir formalizasyon planı olarak yayımladı; IEEE Spectrum ilk rapor etti.

246 sınırı, ikiz asal varsayımı üzerine uzun süren saldırıda insan bilgisinin şu anki sınırıdır; bu, 19. yüzyılda ortaya atılan, iki asal sayının tam iki farkla sonsuza kadar tekrar ettiği hipotezidir. Axiom Math’ın proje sayfası, çalışmayı James Maynard’ın 2013 tarihli “Small gaps between primes” (Asallar Arasındaki Küçük Boşluklar) makalesinin birleşik formalizasyonu ve Polymath8b iş birliğinin, Maynard’ın 600 sınırını 246’ya düşüren kısmı olarak tanımlıyor. Makine tarafından denetlenmiş kanıtlar, PrimeGapsLib adlı halka açık bir Lean kütüphanesinde düzenlenmiş olup, 246 teoremi bu kütüphanenin önde gelen sonucu olarak yer alıyor.

“Bu teorem şu anda asal sayılar hakkında insan bilgisinin eşiğini temsil ediyor,” dedi Axiom Math’ın kurucu matematikçisi Ken Ono.

Formal doğrulama, bir kanıtı küçük, güvenilir bir çekirdek programının satır satır kontrol edebileceği bir dile çevirmek anlamına gelir. Sonuç mutlak bir garanti değildir — ifadenin kendisinin doğru çevrilmesi ve denetleyicinin sağlam olması gerekir — ancak insan hakeminin hatasını zincirden çıkarır. Şimdiye kadar, matematik benchmark’larında yarışan AI sistemleri çoğunlukla kısa, bağımsız kanıtlarla ölçülmüştür; bu sonuçlarla araştırma düzeyindeki formalizasyon arasındaki boşluk geniş olmuştur; bu durum daha önce olimpiyat geometrisinde üstün performans gösteren sistemlerde görülmüştür, ancak araştırma matematiği büyük ölçüde dokunulmamıştır.

70 Milyondan 246’ya

Varsayım kendisi, 19. yüzyılda Alphonse de Polignac tarafından kesin olarak formüle edilmiş olup, hâlâ kanıtlanmamıştır. İlk sınırlı sınır 2013’te Yitang Zhang, sonsuz sayıda asal çiftinin birbirinden 70 milyon içinde olduğunu kanıtladığında ortaya çıktı. Aylar sonra, Maynard rafine bir süzme yöntemi tanıttı ve sınırı 600’e indirdi — bu çalışma 2022 Fields Madalyası’na katkı sağladı — ve Maynard ile Terence Tao’nun da içinde olduğu Polymath8b iş birliği bunu 246’ya taşıdı. Axiom Math’ın planı, bu ilerlemeyi formalize etmeyi amaçlayan proje olarak sunuluyor.

Formalizasyon, şirketin üç aşamada tanımladığı bir akış izler. Araştırmacılar önce kanıtı bir plan olarak yazdı — her tanım, lema ve teorem bir etiket, kesin bir ifade ve bağlı olduğu sonuçların bir listesi ile verildi — böylece bir bağımlılık grafiği oluşturuldu. AxiomProver, şirketin çok‑ajanlı matematik araştırma sistemi, Mathlib topluluk matematik kütüphanesi ve Alex Kontorovich ile Tao’nun yönettiği mevcut formalizasyon projesi PrimeNumberTheoremAnd üzerine inşa edilmiş makine‑denetlenebilir Lean 4 kanıtları üretti. Axiom ekibi daha sonra oluşturulan kodu gözden geçirip PrimeGapsLib’e düzenledi.

Kütüphanenin belirtilen ana sonuçları başlık teoreminden biraz daha öteye gidiyor. 246 sınırının yanı sıra, Maynard’ın 600 sınırını da formalize ediyor ve sadece Mathlib üzerine kurulu, kanıt yuvası boş bırakılmış bir kendi içinde bağımsız doğrulama meydan okuması içeriyor — bu, kütüphane kanıtlarının belirtilen teoremlere uygun olduğunu herkesin Lean karşılaştırma aracıyla bağımsız olarak onaylamasını sağlıyor. Şirket, tam denetimin saatler sürebileceği konusunda uyarıyor; diğer iki sonucu kapsayan azaltılmış bir sürüm ise dakikalar içinde çalışıyor.

Bu, AI Formalizasyon İddiaları Arasında Nerede Duruyor

Sonuç, AI sistemlerinin araştırma düzeyinde matematik yapabildiğine dair artan iddiaların bir yılına denk geliyor; çoğu iddia yarışma puanları veya kısa kanıtlara dayanıyor. Axiom Math, daha agresif iddia sahiplerinden biri: AxiomProver, şirketin hakemli dergilerde yayınladığı çalışmalar da dahil olmak üzere, daha önce açık olmayan problemleri çözdüğü için övgü alıyor ve AI sistemleri artık birkaç uzun süredir devam eden Erdős problemini çözdü. 246 formalizasyonu farklı bir sonuç türü — yeni bir teorem değil, modern sayı teorisinin en teknik olarak zor kanıtlarından birinin makine‑denetlenmiş yeniden inşası.

En yakın karşılaştırma, bu yılın başlarında Math, Inc.‘nin Gauss ajanını kullanarak Maryna Viazovska’nın 8 ve 24 boyutlardaki Fields Madalyalı küre paketleme sonuçlarının formal kanıtını tamamlamasıdır. Carnegie Mellon doktora öğrencisi Sidharth Hariharan, bu formalizasyonun insan planlama çabasını yönetti ve şu anda Axiom Math’ta stajyer ve 246 projesinde isimli matematik katkıcısı olarak çalışıyor; yeni sonucun daha kapsamlı bir başarı olduğunu savunuyor. Onun gerekçesi, Axiom’un yeniden kullanılabilirlik için inşa edildiği: tek bir kanıtın tek seferlik formalizasyonu yerine, PrimeGapsLib gelecekteki formalizasyon çalışmaları ve araştırmalar için destek sağlayacak bakım yapılan bir asal‑boşluk sonuçları kütüphanesidir.

Bu ayrım, sonucun nasıl okunması gerektiği açısından önemlidir. Tek seferlik bir doğrulama, bir sistemin tek bir zor kanıtla başa çıkabildiğini gösterir. Bir kütüphane ise altyapıya daha yakın bir şey gösterir — diğer sonuçların üzerine inşa edebileceği yeniden kullanılabilir formal makine, formal kanıt sistemlerinin alıştırma çözmekten gerçek matematiği denetlemeye geçişte hareket ettiği yönü gösterir. Buradaki yetenek iddiası, kamuya açık ve yeniden çalıştırılabilir varlıklara dayanır; bir plan, Lean kodu ve dış araştırmacıların kanıtları kendileri doğrulayabileceği bir karşılaştırma meydan okuması.

Ono, matematiği daha büyük bir hedef için bir test ortamı olarak çerçeveliyor. Yazılımın özellikleri — bir programın sonlanıp sonlanmadığı, çıktısının her girdi için doğru olup olmadığı — kesin matematiksel ifadelerle tanımlanabiliyorsa, AxiomProver’dan türetilen sistemlerin bunları formal olarak kanıtlayabileceğini, AI‑tarafından üretilen kodun altyapı, finans ve güvenlik sistemlerini çalıştırmaya başlamasıyla birlikte doğrulama sağlayabileceğini savunuyor.

“Dünya, kimsenin okumadığı bir bilgisayar kodu üzerinde çalışmak üzere,” dedi Ono. “AI burada ve artık göz yumamayız — kanıt formalizasyonu, AI’dan kaynaklanan en önemli zorluğu çözmek için bir test ortamı.”

Şimdilik teslim edilebilir daha dar ve denetlenebilir: 41 yazarın planı, halka açık bir Lean kütüphanesi ve asal sayıların 246 içinde birbirine yakın olduğu sürece tükenmeyeceğini gösteren, ikiz asal varsayımının en yakın doğrulanmış komşusu ve bir AI sisteminin şimdiye kadar uçtan uca kontrol ettiği en derin araştırma matematiği.