Axiom tüm Stacks Project külliyatını Lean dilinde resmileştirdi

Yapay zeka araştırma şirketi Axiom, modern cebirsel geometrinin temel referans kaynağı kabul edilen yaklaşık 7 bin 500 sayfalık Stacks Project külliyatının Lean ortamındaki tam resmi doğrulamasını yayımladı. Yaklaşık 16 milyon satır kod içeren çalışma, bugüne kadar inşa edilmiş en büyük bütünleşik ve yeniden kullanılabilir resmi matematik kütüphanesi olma niteliğini taşıyor. Columbia Üniversitesi matematikçisi Johan de Jong tarafından 2005 yılında başlatılan açık kaynaklı proje, bu adımla birlikte bilgisayar tarafından adım adım denetlenebilen tek bir kod tabanına dönüştü.

Söz konusu ölçekte bir kütüphanenin oluşturulması için Axiom mühendisleri, paralel çalışan koordineli yapay zeka ajanlarından oluşan hiyerarşik bir sistem kullandı. Bu ajanlar bağımlılık grafiği boyunca matematiksel önermeleri resmi dile çevirdi, Mathlib kütüphanesindeki mevcut soyutlamalarla eşleştirdi ve ispatları tamamladı. Süreç boyunca ajanlar, özgün metinde yer alan onlarca eksik hipotezi ve pozitif karakteristik gibi özel durumlara bağlı uç hataları tespit ederek açık karşı örneklerle birlikte metni düzeltti.

Elde edilen resmi kütüphane, araştırmacıların ve yapay zeka sistemlerinin cebirsel geometri ispatlarını sıfırdan kurmadan doğrudan temel tanımları içe aktarmasına olanak tanıyor. Axiom, özgün projedeki dört karakterlik kalıcı etiket yapısını koruyarak Lean bildirimlerini kaynak metinle eşleştiren etkileşimli bir web arayüzü de sundu. Johan de Jong'un talebi doğrultusunda, resmi doğrulama sürecinde elde edilen düzeltmeler ve karşı örnekler ana depoya gönderilmek yerine Axiom'un bağımsız açık kaynak deposunda tutuluyor.