費馬最後定理完整機器驗證證明開源
Anthropic以Apache 2.0授權開源費馬最後定理在Lean 4中的完整機器驗證證明，建立在Mathlib之上，經三套核心交叉驗證。
形式化驗證 資訊與深度分析
收錄 形式化驗證 相關產品動態與產業觀察，共 4 篇文章。
收錄 形式化驗證 相關產品動態與產業觀察，共 4 篇文章。
Anthropic以Apache 2.0授權開源費馬最後定理在Lean 4中的完整機器驗證證明，建立在Mathlib之上，經三套核心交叉驗證。
柏克萊RDI實驗室推出Vero基準，要求AI代理人在整個Lean 4儲存庫規模上同時寫實作、寫證明。就算是表現最好的模型，43個專案裡也只有27個被完整解出。
OpenBMB全面開源數學自動形式化方案MathForm：8B模型、約36.7萬筆已驗證Lean 4資料集與評測程式碼一併釋出，多項測試贏過32B專用形式化模型。
OpenAI以Astra的內部版本公開十項數學與理論計算機科學成果，並同步發布249頁論文、Lean證書與推理記錄。