Axiom 以 24 天將有限單純群分類寫進 Lean
數學 AI 公司 Axiom 宣布，旗下 AxiomProver 智慧體集群在 24 天內完成有限單純群分類定理的 Lean 形式化，稱為首份完整的電腦檢查證明，過程中並挑出 34 處數學偏差。
形式化驗證 資訊與深度分析
收錄 形式化驗證 相關產品動態與產業觀察，共 6 篇文章。
Claude為123個開源函式庫寫出組合語言層證明
Anthropic前沿紅隊用Claude為123個開源函式庫的239個進入點寫出形式化證明：輸入小於64 MB時不會當機，證明直接落在編譯後的RISC-V執行檔上。
費馬最後定理完整機器驗證證明開源
Anthropic以Apache 2.0授權開源費馬最後定理在Lean 4中的完整機器驗證證明，建立在Mathlib之上，經三套核心交叉驗證。
柏克萊Vero基準：43個專案僅27個全解
柏克萊RDI實驗室推出Vero基準，要求AI代理人在整個Lean 4儲存庫規模上同時寫實作、寫證明。就算是表現最好的模型，43個專案裡也只有27個被完整解出。
面壁開源8B形式化模型完勝32B對手
OpenBMB全面開源數學自動形式化方案MathForm：8B模型、約36.7萬筆已驗證Lean 4資料集與評測程式碼一併釋出，多項測試贏過32B專用形式化模型。
OpenAI讓Astra寫出十個證明
OpenAI以Astra的內部版本公開十項數學與理論計算機科學成果，並同步發布249頁論文、Lean證書與推理記錄。