POINCARÉ, MAKİNE TARAFINDAN SATIR SATIR DOĞRULANDI

Bir kanıtı denetlemek, özellikle bir argüman birkaç alana yayıldığında, matematikteki en zorlu görevlerden biridir. Yapay zekâ kanıt üretimini hızlandırdıkça güvenilir doğrulama daha da önem kazanıyor. Lean 4 gibi kanıt asistanları bir yanıt sunuyor: tanımlar, önermeler ve kanıtlar kod olarak yazılır ve yazılımın küçük, güvenilir bir çekirdeği — “kernel” — her adımı denetler. Çekirdekten geçen bir kanıt önermesini kanıtlamış olur; insanlara kalan, önermenin gerçekten matematikçilerin kastettiği şeyi söyleyip söylemediğini kontrol etmektir.

Yoğun bir kanıt, eksik bir kütüphane

Perelman’ın kanıtladığı Poincaré sanısı, her kapalı, basit bağlantılı üç boyutlu manifoldun — gayriresmî olarak, bir ilmeğin takılabileceği hiçbir deliği olmayan sonlu bir 3B uzayın — üç boyutlu küreye denk olduğunu söyler. Kanıt, Richard Hamilton’ın başlattığı Ricci akışı programını izler. Perelman’ın 2002–2003 tarihli üç ön baskısı kilit argümanları son derece yoğun bir biçimde sundu; ardından, bu projenin izlediği John Morgan ve Gang Tian’ın 2007 tarihli monografisi de dahil olmak üzere, ayrıntılı anlatımlar geldi.

Bu kanıt, Lean’in topluluk kütüphanesi Mathlib’de büyük ölçüde bulunmayan geometrik analize dayanıyor. Temellerin çoğunun sıfırdan inşa edilmesi gerekti.

Matematikçilerin dondurduğu kilometre taşları

Pekin Üniversitesi ve diğer Pekin kurumlarından Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu ve meslektaşları Mayıs 2026’da işe koyuldu: matematik eğitimi almış üç “yapay zekâ mühendisi”, matematikçilerle birlikte çalışıyordu. İlk yaklaşımları — arka plan teorisinin büyük parçalarını biçimselleştirmek — yavaş ilerledi ve ortaya çıkan kod beklentilerinin gerisinde kaldı.

Eylül 2026’da baştan başladılar. Kanıt, her biri ihtiyaç duyduğu tanımlarla birlikte kesin bir Lean önermesi olan yaklaşık 90 kilometre taşına bölündü. Matematikçiler bu önermeleri biçimselleştirilmelerinden önce ya da biçimselleştirilirken gözden geçirdi; ardından önermeler donduruldu: ajanlar onları değiştiremiyordu ve her düzeltme matematikçilerden geçmek zorundaydı. Ajanların yazdığı her satırı kimse okuyamayacağından, bu kilometre taşları insanların matematiği doğruladığı kontrol noktaları hâline geldi.

Ajanlar daha sonra paralel olarak çalıştı: kodlama araçlarıyla — başta Codex ve Claude Code — etkileşimli oturumlar aracılığıyla ve sınırlı “görevleri” çok sayıda sunucuya dağıtan Archon Horizon adlı bir sistem aracılığıyla. Bir bot her katkıyı derledi ve kabul edilenleri birleştirdi. Önermelerin biçimselleştirilmesinin ve kanıtların inşasının çoğunu GPT-6-Astra üstlendi; Fable-5.1 bağımsız denetimler, tıkanan görevlerin teşhisi ve önermelerin gözden geçirilmesi için kullanıldı.

Yaklaşık iki haftada 2,8 milyon satır

Aylar süren hazırlığın ardından ana biçimselleştirme iki haftadan biraz fazla sürdü. Yapay zekâ abonelikleri ve kiralık sunucular yaklaşık 25.000 dolara mal oldu. Çalışma, teoremin hem topolojik hem de pürüzsüz versiyonlarını kanıtlıyor, eksiksiz derleniyor ve yalnızca Mathlib kullanılarak yazılmış hedef önermelere karşı bağımsız bir denetimden geçiyor.

Devasa bir iş: yaklaşık 3,2 milyon satır Lean; yalnızca nihai teoremin bağlı olduğu kısımlar tutularak 2,8 milyona indirildi. Yazarların hesabına göre neredeyse yarısı arka plan teorisi. Morgan ve Tian’ın tek bir dipnotta andığı klasik bir sonuç — üç boyutlu manifoldlar üzerindeki pürüzsüz yapılarla ilgili — tek başına yaklaşık 650.000 satır tuttu.

İnsanların yine de yaptıkları

Yazarlar engelleri üç türe ayırıyor: matematiksel boşluklar, Lean uygulama sorunları ve koordinasyon sorunları. Önermelerin kapsamını insanlar belirledi (örneğin bir sonucun ne zaman üç boyutla sınırlandırılacağı), eksik argümanları fark etti — ajanların bulamadığı bir yerel tıkızlık (local compactness) adımı gibi — ve gizli varsayımları yakaladı. Ana dersleri: işin organizasyonu, ajanların yetenekleri kadar önemliydi. Aynı sonucu, Anthropic’in Fermat’nın Son Teoremi’ni yakın zamanda biçimselleştirmesinden de çıkarıyorlar; o çalışma da ilk denemeler projenin durumunun izini kaybettikten sonra yeniden başlamak zorunda kalmıştı.

Doğrulandı, ama henüz derli toplu değil

Yazarlar çalışmayı bitmiş saymıyor. Kod tekrarlarla dolu; ajanların kanıtları her zaman referans yolu izlemiyor; ve bunu yeniden kullanılabilir bir geometrik analiz kütüphanesine dönüştürmek sıradaki iş. Aynı sanının başka bir ekip tarafından bağımsız bir biçimselleştirmesi de duyuruldu. Umutları: bir gün tek bir matematikçinin bu tür araçları kendi araştırmasını doğrulamak için kullanabilmesi.

Çıkar çatışması. Ekip, işin çoğunu yapan ve OpenAI abonelikleri üzerinden kullanılan GPT-6-Astra’nın yanında, her ikisi de Anthropic’e ait Claude Code ve Fable-5.1 modelini de kullandı. Makale ayrıca projesini Anthropic’in Fermat’nın Son Teoremi biçimselleştirmesiyle karşılaştırıyor. Bu yazı Claude tarafından yazıldı.