面壁智能 MathForm 开源：让 AI 自动把数学题翻译成 Lean 4 形式化代码

面壁智能 OpenBMB 最近正式开源了 MathForm，这是一套围绕 Lean 4 数学形式化语言设计的训练框架、数据集和模型组合。形式化数学长期被视为 AI 的高难度任务之一，因为模型不仅要“算对”，还要把推理过程写成可被 Lean 编译器验证的代码。

本次更新的核心是 FormalVerse 数据集，规模达到 367K 以上已验证示例。研究者把每道题对应的形式化证明都跑过 Lean 4 校验，确保数据本身可信，而不是只靠“看起来对”的文本对。

面壁团队公布了一组受限预算下的对比：在 100K 训练数据预算下，基于 FormalVerse 训练的模型 Consistency Check 指标达到 60.32%，高于 FineLeanCorpus 的

46.53% 和 NuminaMath-LEAN 的

41.49%。

这意味着在同等数据规模下，MathForm 路径产出的模型“形式化正确率”更稳。

为什么 Lean 4 自动形式化值得专门做一套

Lean 4 是当前数学形式化领域最活跃的开源证明助手之一，Mathlib 社区沉淀了大量形式化定理。但让大语言模型直接生成 Lean 4 代码，一直存在两个痛点：一是公开数据稀疏，二是模型常常写出“看起来合理、编译却报错”的证明。

MathForm 的思路是把这条链路拆成三段：先用主流大模型把自然语言题目改写成 Lean 4，再用 Lean 编译器反复验证，最后只保留编译通过的部分入库。这种“编译器当裁判”的做法，和过去靠人工标注相比，扩展性明显更好。

对中文开发者和研究者的实际价值

对国内做数学 AI、AI for Science 的团队来说，MathForm 的最大意义是降低起步门槛。框架、数据集、模型权重同时开源，意味着小团队不必从零攒 Lean 4 训练数据，可以直接复现基线，再结合自己的教材或竞赛题库做增量训练。

在课程和竞赛场景下，中学高年级到本科阶段的数论、代数题比较适合作为切入点。形式化证明可以帮学生检验推理链是否完整，也方便老师在批改时定位“哪一步出现跳步”。

对企业和大模型团队的影响

对正在做代码生成、数学解题或 AI 助教的大模型团队，MathForm 提供了一种可借鉴的范式：用确定性工具当奖励信号。相比纯文本 RLHF，这种基于编译器的反馈更稳定，也更容易追溯失败原因。

短期看，更现实的应用是把 MathForm 类能力嵌进 RAG 或 Agent 流程：当用户问一个复杂数学问题时，系统先尝试自动形式化，再调用 Lean 4 验证，把“是否严格成立”明确告诉用户，而不是只给一句看似自信的自然语言解释。

后续值得关注的几个观察点

首先，60.32% 这个数字是在 100K 预算下得出的，扩展到更大数据规模时能否继续领先，还需要等社区复现和独立评测。其次，FormalVerse 是否会持续更新、是否覆盖中文数学题和国内竞赛题源，决定了中文用户的实际收益。

另外，Lean 4 自动形式化对算力并不友好，单次编译验证耗时明显。后续如果出现更高效的轻量验证策略或专用推理加速方案，这套路线才更容易被普通开发者用起来。

对关注 AI for Math 的读者，MathForm 更像是一份开源基础设施，而不是一个面向终端用户的产品。把它接入自己的研究、教学或产品链路，才是这次开源真正的落点。