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

面壁智能（OpenBMB）正式上线了一个新的开源项目 MathForm，定位是面向 Lean 4 的数学自动形式化框架。整套内容包含训练框架、配套数据集和模型权重，目前已经在 GitHub 和 Hugging Face 同步开源，开发者可以直接下载使用。

所谓自动形式化，就是让模型把人类写在纸上的数学命题和推理过程，翻译成 Lean 4 这类形式化证明系统能

的代码。它是数学 AI 从

走向

的关键中间步骤，也是这几年 AI for Math 的主战场之一。

填补自动形式化的开源空白

过去两年，DeepMind 的 AlphaProof、Lean Copilot 等项目都把 Lean 4 当作验证底座。但

这一步，长期缺乏高质量数据集和可复现流程，论文里的数字很难拿来横向比较。MathForm 想补的就是这块短板。

MathForm 同步放出了名为 FormalVerse 的数据集，包含超过 36.7 万条已经过 Lean 4 验证的

配对样本，话题覆盖代数、几何、数论等基础分支，难度跨度从教材习题到竞赛题都有。

在 10 万条训练预算的对照设置下，基于 FormalVerse 训练的模型在一致性检查（Consistency Check）指标上达到 60.32%，明显高于 FineLeanCorpus 的 46.53% 和 NuminaMath-LEAN 的 41.49%，差距都在十几个百分点。

对研究者和中文用户的意义

对做数学 AI 的研究者来说，更大的意义是开源了一整套可复现的流水线：数据筛选、训练配方、评测脚本都齐了。小型团队不需要从零搭环境，可以直接在 MathForm 基础上做二次实验和消融研究，这是过去几个月里少见的

放出来。

对普通开发者而言，这条线更像是

。短期看不会直接变成消费品，但当自动形式化模型足够稳定，就能嵌进数学教育工具、论文校对、教材自动出题等场景，逐步改变数学写作的工作流。

对国内 AI 工具使用者来说，面壁智能选择把模型、数据、代码全部开源，意味着本地部署和二次训练的门槛很低。对中文数学场景的微调也会更友好，不必依赖闭源 API，这一点和之前开源小模型的路子一脉相承。

还值得继续观察的几件事

需要注意的是，Consistency Check 不是端到端的证明成功率。它衡量的是模型输出能否被 Lean 4 工具链接受，并不直接代表

的能力。要想看真实水平，还需要等 PutnamBench、LeanStep 等更高难度基准上的复现结果。

另外，36.7 万条样本里英文题占主导，中文数学教材题目的覆盖并不充足。如果要做面向中国学生的数学教育产品，还得自己补一批中文数据并做对齐，这是国内团队绕不开的一环。

接下来值得盯三件事：一是面壁是否会放出更大规模的中文扩展数据集；二是是否有高校或创业公司把 MathForm 接到教学产品里；三是它和 Lean Copilot、Kimina-Prover 等同类项目在排行榜上的差距会不会被进一步拉开。开源数学 AI 这一波，正在变得越来越卷。