Matematikçi Thomas Hales, Lean'in güvenilirliğini ve yapay zekâ destekli otoformalizasyonun yükselişini değerlendiriyor

Hacker News'te de öne çıkan, Terence Tao'nun blogunda yayımlanan matematikçi Thomas Hales'in konuk yazısı, yapay zekânın hiçbir insan ekibinin ulaşamayacağı bir hızda biçimsel kanıtlar ürettiği bir dönemde, çalışan matematikçilerin Lean teorem kanıtlayıcısı hakkında neleri bilmesi gerektiğini ortaya koyuyor. Hales yazının başında konunun özünü çerçeveliyor: matemattete değer verdiği şey, onun tutarlılığı ile bilim ve uygarlığa sağladığı destekteki güvenilirliğidir. Tao da yazına düştüğü editör notunda, yazının kendisinin yapay zekâ kullanılarak başka bir dosya biçiminden dönüştürüldüğünü belirtiyor.

Otoformalizasyon dönüm noktalarıyla dolu bir yıl

Hales bu değişimin başlangıcını, araştırmacıların otoformalizasyonun — yapay zekânın bir makaleyi okuyup Lean ya da başka bir kanıt asistanında biçimsel bir kanıt üretmesinin — pratik hale geldiğine giderek daha çok inandığı 2025 ilkbahar sonu ve yazına tarihliyor. Yazıda sıralanan zaman çizelgesi şöyle:

• Eylül 2025: Math Inc., asal sayı teoreminin yarı-otoformalizasyonunu gerçekleştiriyor; yapay zekâ takıldığında insanlar devreye giriyor.
• Ocak 2026: J. Urban, iki haftada üretilen ve Munkres'in topoloji ders kitabının büyük bölümünü küme teorisine dayalı bir kanıt asistanında kapsayan 130.000 satırlık biçimsel topolojiyi anlatan bir arXiv ön baskısı yayımlıyor.
• Mart 2026: Math Inc., Viazovska ve iş birlikçilerinin 24 boyutlu küre paketleme sonucunu otoformalize ediyor; 8 boyutlu durumu duyurduktan yaklaşık bir hafta sonra, sonra yaklaşık 200.000 satıra indirilen kabaca 500.000 satır kod üretiliyor.
• Mayıs 2026: Meta'daki bir grup, ATLAS adlı projede 26 matematik ders kitabının büyük bölümlerini biçimlendiriyor.
• 4 Eylül: Anthropic, Fermat'nın Son Teoremi'nin otoformalizasyonunu duyuruyor; 11 günde üretilen 13 milyon satırlık Lean kodu.
• 8 Eylül: OpenAI, Navier-Stokes için bir zorla patlama (forced blowup) sonucunu Lean biçimlendirmesiyle birlikte duyuruyor ve Jared Lichtman, "bilinen tüm matematiği biçimsel koda çevirmeyi" amaçlayan MAP'yi (Mathematics Autoformalization Project) başlatıyor.

Yapay zekâ öncesi dönemle karşıtlık çarpıcı: Kepler sanısının elle inşa edilen biçimsel kanıtı kabaca 20 insan-iş-yılı ve yaklaşık 500.000 satır kanıt betiği tüketmişti. Hales ayrıca Urban'ın Ocak ayındaki, biçimlendirmenin "2026'da oldukça kolay ve yaygın hale gelebileceği" yönündeki öngörüsüne ve IEEE Spectrum aracılığıyla aktarılan Jesse Han'ın, yaygın ölçekli biçimlendirmenin matematiğin devrimci bir dönüşümü olduğunu belirten görüşüne değiniyor. 8 ve 24 boyutlu küre paketleme, Navier-Stokes ve Fermat'nın Son Teoremi biçimlendirmelerinin tümü bu yıl tamamlandı ve dört renk teoremi, Feit-Thompson tek derece teoremi, küre içe çevirme ve Kepler sanısı gibi önceki dönüm noktalarına katıldı.

Lean ve mathlib

Yazıya göre matematikçiler arasında Lean; Isabelle, HOL Light, Coq (yeni adıyla Rocq), Metamath ve Mizar gibi sistemlerin önünde en popüler kanıt asistanı. Lean, 2013'te Leo de Moura tarafından Microsoft'ta tanıtıldı ve topluluğun yararına açık kaynaklı hale getirildi. Kevin Hartnett'ın proje tarihini anlatan "The Proof in the Code" adlı yazısı, Jeremy Avigad'ı Lean'in ilk kullanıcısı olarak anıyor; 2017'de Avigad'ın yüksek lisans öğrencisi Mario Carneiro, Johannes Hölzl ile çalışarak matematik kütüphanesi mathlib'i çekirdek kütüphaneden ayırdı. Mathlib bugün 2,5 milyon satır kodun içinde yaklaşık 300.000 teorem ve 100.000'den fazla tanım içeriyor; 700'den fazla katkıcısı var ve bir kanıtın, Cauchy-Schwarz eşitsizliği gibi mevcut bir sonucu yeniden türetmek yerine ona atıf yapmasına olanak tanıyor.

Lean güvenilir mi?

Yazının merkezindeki soru, Lean'in matematiğin talep ettiği güvenilirliği taşıyıp taşıyamayacağı. Lean, indüktif yapılar hesabı (calculus of inductive constructions) adlı bir tip teorisi lehçesi üzerine inşa edilmiş. Hales, Russell'ın 1901 paradoksuyla tetiklenen temel krizin iki yoldan yanıtlandığını anlatıyor: güvenli olmayan kümeleri yasaklayan Zermelo'nun küme-teorik aksiyomları ve paradoksal yapıları sözdizimi hatalarına dönüştüren Russell'ın tip teorisi. Küme teorisiyle yetişen matematikçiler için Hales, ZFC'nin CIC içine kodlanabileceğini ve CIC'in bir lehçesinin erişilemez kardinaller hiyerarşisiyle güçlendirilmiş ZFC içine geri kodlanabileceğini gösteren B. Werner'ın 1997 tarihli "Sets in Types, Types in Sets" makalesine işaret ediyor. Basitleştirilmiş tabiriyle tipler ayrık kümeler gibi davranır: doğal sayı 2 ile gerçel sayı 2.0 farklı tiplerde yaşar ve açık bir zorlama (coercion) aracılığıyla bağlanır. Ayrıca Hales, Lean'in aynı zamanda sıradan programlarının derlenip çalıştığı genel amaçlı bir programlama dili olduğunu ve programlama ile matematik dillerinin birbirinden bağımsız varlıklar olmadığını vurguluyor.

Neden önemli

Hales'in savı şudur: Matematik otoritesini tutarlılık ve güvenilirlikten alır ve yapay zekâ, alanı tek hakeminin bir kanıt asistanı olduğu makine üretimi kanıtlarla doldurmaya hazırlanıyor. Bu, Lean'e ilişkin temel soruları yeniden acil hale getiriyor: otoformalizasyon kolay ve yaygın hale gelirse, bir teoremin doğruluk sertifikası giderek kanıtlayıcının onu kabul etmiş olmasına denk düşecek ve matematikçilerin bu garantisin tam olarak neye dayandığını bilmesi gerekecek. MAP gibi girişimler trilyon satırlık biçimsel koddan söz ettiğine göre, topluluğun doğrulayıcının kendisini anlaması, her sonucun arkasındaki güven zincirinin bir parçası haline geliyor.