2026-11-05 16:19:48
AxiomMath 於週三將 Stacks Project 形式化,並把 7,654 頁內容轉換為 1600 萬行經過驗證的程式碼
根據 TechCrunch 報導,AxiomMath 週三宣布,已完成對 Stacks Project 的形式化驗證。Stacks Project 是有史以來彙編出的最大型數學資料集之一。該公司使用 Lean 將這個專案約 7,654 頁的內容轉換為約 1,600 萬行經電腦驗證的程式碼;Lean 是一種專為形式化證明驗證而設計的程式語言。Stacks Project 由哥倫比亞大學數學家 Johan de Jong 於 2005 年創立,是一個開放原始碼的參考資料庫,涵蓋從大學程度的代數到進階代數幾何、數論與幾何等數學領域。數學形式化可讓證明助理逐行驗證程式碼,確保邏輯嚴謹,為開發軟體及進行科學研究的 AI Agent 奠定可靠基礎。