面壁智能 OpenBMB 推出 MathForm，一个面向 Lean 4 数学自动形式化的开源框架、数据集与模型。该项目旨在降低数学证明形式化的门槛，让研究者能更高效地将自然语言数学命题转化为机器可验证的 Lean 4 代码。

其核心组件 FormalVerse 数据集包含 367K+ 个已验证示例，为模型训练提供了扎实的语料基础。在匹配 100K 预算的评测条件下，基于该数据集训练的模型在 Consistency Check 任务上达到 60.32% 的准确率。

打开网易新闻 查看精彩图片

这一成绩显著优于同类开源方案：FineLeanCorpus 为 46.53%，NuminaMath-LEAN 为 41.49%。

打开网易新闻 查看精彩图片

目前，MathForm 的框架、数据集与模型均已开源，可供社区使用与二次开发。