Axiom, 7.500 sayfalık Stacks Project'in tamamını Lean ile formelleştirdi

TechCrunch'a göre 1,6 milyar dolar değerlemeye sahip girişim Axiom, temel cebirsel geometri referansı olan Stacks Project'in tamamını resmi olarak doğruladı ve onu yaklaşık 16 milyon satır makine denetimli Lean koduna dönüştürdü. Axiom, sonucu şimdiye kadar kurulmuş en büyük bütünleşik ve yeniden kullanılabilir formelleştirilmiş matematik kütüphanesi olarak tanımlıyor.

Bir referans metnin çevirisi

Stacks Project, 2005'te Columbia Üniversitesi matematikçisi Johan de Jong tarafından başlatılan ve iki on yıl boyunca yüzlerce katkıcı tarafından genişletilen açık kaynak bir cebirsel geometri referansıdır. Axiom uzunluğunu yaklaşık 7.500 sayfa olarak veriyor; TechCrunch ise yaklaşık 7.654 sayfa sayıyor. TechCrunch'a alıntılanan Columbia'dan Peter Woit, "benzeri gerçekten hiçbir şey yok" diyerek projeyi 20. yüzyılda matematiği temellerinden yeniden inşa eden Bourbaki kitaplarına benzetti.

Yayın, projenin kalıcı dört karakterlik tag'lerini koruyor; böylece her Lean bildirimi kanonik metindeki ilgili pasaja bağlanıyor. Axiom ayrıca orijinal sayfaları Lean koduyla yan yana gösteren bir çevrimiçi görüntüleyici ve etkileşimli bir bağımlılık grafiği yayımladı. Tek bir tag birkaç resmi tanıma genişleyebildiği için — bazıları yeni yazılmış, bazıları mevcut Mathlib kütüphanesine köprülenmiş — arayüz bu eşlemeleri açıkça kaydediyor. Axiom'a göre Lean'in çekirdeği (kernel), atıf yapılan bir sonucun yalnızca kesin hipotezleri sağlandığında uygulanabileceğini garanti ediyor.

Formelleştirme ne kazandırıyor

Bir ispatı formelleştirmek, onu Lean'de kod olarak yeniden yazmak ve proof assistant adı verilen bir programla satır satır denetlemek anlamına geliyor. İspat geçerse matematikçiler onun mantıksal olarak sağlam olduğuna güvenebiliyor. TechCrunch'ın belirttiği gibi mühendisler aynı tekniği, yani resmi doğrulamayı çip tasarımlarını onaylamak için kullanıyor; Fransa'daki araştırmacılar ise aile yardımlarını hesaplayan yazılımdaki hataları yakalamak için kullandı.

Stacks Project için tek tek teoremleri denetlemek işin yalnızca bir parçasıydı. Sonuçları, her şeyin öncesindeki üzerine inşa edildiği yoğun bir bağımlılık ağacı oluşturuyor ve bütün külliyat tutarlı kalmak zorunda. "Hayatta büyük olan şeylerle hassas olan şeyler pek bir araya gelmez" diyen Axiom CEO'su Carina Hong, TechCrunch'a tanımların birbiriyle "çatışmaması" gerektiğini ekledi.

Paralel çalışan ajanlar

Axiom, binlerce teoremi paralel olarak çeviren, ispatlayan ve bütünleştiren büyük ve eşgüdümlü yapay zeka ajanı ekipleri çalıştırdığını söylüyor. TechCrunch, ekibin her görevi dayatmak yerine gevşek bir hiyerarşi kurduğunu ve ajanların eşzamanlı yapabilecekleri işleri kendilerinin belirlemesine izin verdiğini aktarıyor. Şirket ayrıca matematikte iyi olmak için kendi modellerini eğitti; Hong, diğer doğrulama girişimlerinin genelde bu yaklaşımı benimsemediğini söyledi.

TechCrunch'ın 25 yaşında olarak tanımladığı Hong, şirketi kurmak için Stanford'daki matematik doktora programından ayrıldı; şirketi Mart 2025'te kurdu. Mart ayında Axiom, Menlo Ventures liderliğinde 200 milyon dolarlık bir Series A yatırım turu aldı.

Bu, Axiom'un bu sezonki ikinci büyük yayını. 27 Ekim 2026'da şirket, Sonlu Basit Grupların Sınıflandırması'nın Lean formelleştirmesini yayımladı. Ama Axiom'un belirttiğine göre ikisi farklı mühendislik zorlukları temsil ediyor: o proje tek bir dönüm noktası niteliğindeki teoreme odaklanırken, Stacks Project değeri binlerce birbirine kenetlenmiş, yeniden kullanılabilir tanıma ve lemmada yatan temel bir kütüphane.

Cebirsel geometri boşluğunun doldurulması

Yayın, Axiom'un teknik kadrosundan Ashvin Swaminathan'ın formelleştirilmiş matematikteki bir kara delik dediği sorunu ele alıyor. Modern cebirsel geometriye Lean'de yaklaşmak zordu; çünkü çağdaş bir ispat, çekirdek argümanına henüz başlamadan önce değişmeli cebir, şemalar, kılıflar (sheaf), kohomoloji ve cebirsel stack'ler boyunca uzun sonuç zincirlerine atıfta bulunabiliyor. Alandaki yeni çalışmaları denetlemek isteyen araştırmacıların daha önce üzerine inşa edecek çok az Lean altyapısı vardı — ve şimdi, Swaminathan'ın TechCrunch'a söylediğine göre, var.

Neden önemli

Arka planda insanların kolayca inceleyemediği, makine tarafından üretilmiş matematikteki artan hacim var. TechCrunch, yalnızca OpenAI'nin geçen ay zor problemlere çözüm iddiasında bulunan 719 bildiri yayımladığını ve bilgisayar denetimlerinin bile hata yapabileceğini belirtiyor. Resmi doğrulama, o sel ile birlikte ölçeklenen yanıtlardan biri: proof assistant yorulmuyor ve doğrulanmış her teorem bir sonraki için yapı taşı haline geliyor. TechCrunch'a alıntılanan UCLA matematikçisi ve Fields Madalyası sahibi Terence Tao, bu bileşik etkiyi şöyle özetledi: "Ne kadar çok formelleştirilmiş ispatınız varsa, o kadar çok formelleştirilmiş ispat yapabilirsiniz."

Axiom'un daha büyük iddiası saf matematikten öteye uzanıyor. Yapay zeka ajanları dünyanın kodunun giderek daha fazlasını yazdıkça, şirket bunların Hong'un slop dediği şeyden kaçınmak için doğrulanmış temellere ihtiyaç duyacağını savunuyor; Lean kütüphanesi de ajanların üzerine inşa edeceği alt tabaka olarak konumlanıyor. Hong, "tüm kodlama şirketlerini bu ölçekte formelleştirme üzerinde çalışmaya" meydan okumaya kadar gitti.