Axiom 用 24 天把有限单群分类写进 Lean
奇数阶定理当年在 Coq 里做机器验证用了约六年，它只是分类证明里的一块；Axiom 这次报出的是 24 天、4310 万行 Lean 代码、205 万个声明，对应约 1.5 万页原始证明。
形式化验证 资讯与深度分析
收录 形式化验证 相关 AI 新闻、产品动态和产业观察。 本页收录 6 篇已发布文章。
Claude 给 123 个开源库写出汇编级证明
证明代码累计约 1.8 亿行 Rocq，被证明的二进制中位长度只有 1.8 万条 RISC V 指令。在 36 个小型验证任务上，Opus 5.5 完成一半任务所用的 token 比 Opus 5 少约四成。
费马大定理完整机器证明开源，含29511条定理
60475 个模块，29511 条定理。最终依赖的公理只有三条：propext、Classical.choice、Quot.sound。96 核机器完整编译一遍 5 小时 32 分，官方检查工具再跑 14 小时 46 分，第三方独立内核另跑
伯克利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 证书和推理记录，等于把数学成果从口头战报推到可复查工程件。