费马大定理完整机器证明开源，含29511条定理
60475 个模块，29511 条定理。最终依赖的公理只有三条：propext、Classical.choice、Quot.sound。96 核机器完整编译一遍 5 小时 32 分，官方检查工具再跑 14 小时 46 分，第三方独立内核另跑
形式化验证 资讯与深度分析
收录 形式化验证 相关 AI 新闻、产品动态和产业观察。 本页收录 4 篇已发布文章。
伯克利Vero基准：43个项目最好只做完27个
Vero 让智能体在 Lean 4 仓库里既写实现又写证明，2705 条规范的单条通过率最高摸到 87.3%，整仓完全做对的却只有 43 个里的 27 个。单点能力和工程完成度之间那道缝，第一次被量出了具体宽度。
面壁开源8B形式化模型压过32B对手
MathForm 8B 在最难的 FATE X 上拿到 37% 一致性通过率，压过多款 32B 专用形式化模型。把数学题翻成 Lean 4 这件事上，检索 Mathlib 加编译器反馈迭代，比继续堆参数划算。
OpenAI让Astra写出十个证明
Astra 这组证明的看点不止“AI 会做数学”。OpenAI 同时交出论文、Lean 证书和推理记录，等于把数学成果从口头战报推到可复查工程件。