面壁智能 OpenBMB 今天拿出了 MathForm——一个面向 Lean 4 数学自动形式化的开源框架、数据集与模型。数学形式化这个领域，最让人头疼的不是写不出证明，而是编译通过了，语义却悄悄跑偏。MathForm 的野心，就是把这种“假成功”按在地上摩擦。在 AI 辅助证明的浪潮里，这是少有的从数据到模型全链路开源的动作。
Lean 4 社区不缺证明器，缺的是高质量的训练信号。MathForm 的底气来自 FormalVerse 数据集，367K+ 个已验证示例，规模不算小。在匹配 100K 预算的条件下，基于 MathForm 训练的模型 Consistency Check 指标达到 60.32%，明显压过 FineLeanCorpus 的 46.53% 和 NuminaMath-LEAN 的 41.49%。注意，这不是靠堆算力堆出来的，是在同样预算下的横向对比。换句话说，数据质量和训练策略才是关键变量。大语言模型在数学推理上的能力，终于可以更可靠地迁移到形式化证明中。
MathForm 怎么做到的？它用检索规划来组织证明线索，再用语义一致性反馈去迭代修正，专门针对“编译通过但语义漂移”的难题。更难得的是，面壁智能把数据集和 8B 模型一并开源，整套方案对小模型尤其友好——8B 参数，在消费级显卡上也能跑起来。这意味着，那些没有顶级算力的小团队，也能在这条路径上继续做文章。在形式化这个越来越重要的方向，MathForm 给出的不是一句口号，而是一套能拿起来就用的工具链。这条路要是走通了，数学家和算法工程师的协作方式都可能被改写。
