OpenBMB 把 MathForm 这套数学自动形式化方案整体开源：8B 模型权重、约 36.7 万条验证过的 Lean 4 数据集、评测代码与 Pass@k 脚本一并放出。模型挂在 Hugging Face，许可证 Apache 2.0，基座是 Qwen3-8B，权重精度 BF16。项目由清华自然语言处理实验室与面壁智能共同支持的 OpenBMB 团队完成，同名论文本月中旬提交至 arXiv，作者共 10 人。
自动形式化做的是把自然语言写的数学命题翻成 Lean 4 这类机器可验证的形式语言。难处不在字面翻译。Mathlib 的类型层级和定义体系极其庞大，一个命题里的”连续函数""有限群”要精确落到库里对应的那一个定义上，同时保证形式化之后的命题和原命题说的还是一回事。这两件事任何一件出偏差，编译器都可能照样点头。
数据是怎么造出来的
MathForm 的流水线分四步。规划器先针对命题里的数学概念查询 Mathlib，检索工具 LeanExplore 每次返回前 22 条结果；模型在这批检索上下文的条件下生成 Lean 4 命题；候选依次过格式检查、编译测试，再由大模型裁判做语义一致性判定；通过的路径被回溯重构成干净的训练轨迹。
论文里有个数字说明了迭代的必要性：后续轮次贡献了全部保留样本中额外的 31.0%。也就是说，如果只做单遍生成、不合格就丢弃，接近三分之一的可用数据会白白损失。
检索这一步是整套方案里最省钱的设计。让模型凭记忆去回忆 Mathlib 里某个定义的准确名字和签名，本质上是在考它背没背下一个还在持续更新的库；把库交给检索工具、只让模型负责组装，需要的参数量自然就下来了。这也解释了为什么 8B 能和 32B 掰手腕：两边比的本来就不是同一件事。
产出的数据集叫 FormalVerse，约 36.7 万条已验证样本，来源横跨 DeepTheorem、NuminaMath、AceReason-Math、Lean Workbook、Principia-Collection、DeepMath、OpenR1-Math，再补上经典教材内容。这份数据集在 Hugging Face 上已经收到 358 个赞。
成绩单和它的两个口径
训练路径是监督微调后接强化学习。评测铺开六个基准：FormalMATH-Lite 与 DeepSeek-ProverBench 走竞赛数学，CombiBench 测组合数学，FATE 系列按代数难度分 M、H、X 三档。
MathForm-8B 的语法检查平均 Pass@8 为 88.06%，一致性检查平均 72.37%；FATE 三档的一致性通过率依次是 97.33%、63.00% 和 37.00%。对照组包括 Herald Translator-7B、Kimina-Autoformalizer-7B、Mathesis-HPO-7B，以及 StepFun-Formalizer、Goedel-Formalizer-V2、ReForm 各自的 7B/8B 与 32B 版本。8B 在多个测试集上越过了 32B 专用形式化模型的线。
两个口径的落差比绝对分数更有信息量。语法检查只问编译过不过，一致性检查问的是形式化后的命题和原题是不是同一个意思——88% 对 72%，中间那十几个百分点就是这条产线现在真实的瓶颈所在。能编译的东西，未必是你想证的那条定理。
门槛降到了一台工作站
站内前几天写过陶哲轩的警告：AI 产出的证明会多到没人读得完。形式化恰好是这道题的另一半答案——只要证明能过 Lean 编译器，读不读得懂就不再是接受它的前提。前提是命题本身得翻对，FATE-X 上的 37% 说明离这一步还有相当距离。
粗算一笔账，8B 模型以 BF16 加载大约需要 16GB 显存，32B 同精度要 64GB 上下。前者一张 24GB 的消费级显卡就能跑起来，后者得上多卡或专业卡。对高校数学系、证明助手社区和小团队来说，跑一条形式化流水线的硬件门槛，从集群级掉到了单机级。数据集和评测脚本同时开源，别人复现和挑刺的成本也跟着降下来了。
对照表里那一排名字也说明了这条赛道现在有多挤：Herald、Kimina、Mathesis、StepFun-Formalizer、Goedel-Formalizer-V2、ReForm，全是近一两年冒出来的专用形式化模型，而且清一色开源。形式化不像通用对话那样靠烧算力拉开差距，拼的是数据构造工艺和验证闭环，参数规模在这里反倒成了次要变量。一条产线从论文演示推到能开源交付，这个节奏比多数人预期得快。
参考来源：OpenBMB 项目仓库与模型卡、CocoLoop、arXiv 预印本 2608.14221、Hugging Face 数据集页；核验参数规模、许可证、FormalVerse 样本量与各测试集 Pass@8 口径。