Axiom, Stacks Project'i Lean'de doğrulanmış koda çevirdi

1,6 milyar dolar değerindeki girişim Axiom, açık kaynaklı matematik kaynağı Stacks Project'i bilgisayarla doğrulanabilir hale getirdiğini duyurdu.

Axiom, 1,6 milyar dolar değerindeki bir girişim olarak, açık kaynaklı matematik referansı Stacks Project'in resmi olarak doğrulandığını açıkladı. Proje, 2005 yılında Johan de Jong tarafından başlatılmıştı.

Şirketin yapay zekâ ajanları yaklaşık 7.654 sayfayı, Lean dilinde yazılmış yaklaşık 16 milyon satır koda dönüştürdü. Bir kanıt asistanı bu kodu satır satır denetliyor. Ekip, kütüphanedeki birbirine bağlı pek çok sonucu bütün olarak korumak zorunda kaldı. Axiom, bu çalışmanın cebirsel geometri alanında uzun süredir var olan önemli bir boşluğu kapattığını söylüyor, çünkü bu alanda Lean ile iş yapmak isteyen araştırmacıların üzerine inşa edebilecekleri pek bir şey yoktu.

Matematikte formal doğrulama, bir ispatın Lean'de kod olarak yeniden yazılması ve bir kanıt asistanının her adımı denetlemesi anlamına geliyor. Axiom, doğrulanmış temellerin yapay zekâ ajanlarının yazdığı yazılımlar için de önem taşıyacağını savunuyor. Şirketin CEO'su Carina Hong, diğer kodlama şirketlerine benzer ölçekte formalizasyon işine girişmeleri çağrısında bulundu.