OmniTools 8月21日消息，面壁智能 OpenBMB 正式推出 MathForm，一个面向 Lean 4 的数学自动形式化开源框架，配套发布 FormalVerse 数据集与训练模型。
FormalVerse 数据集包含超 367,000 个已验证的数学形式化示例。基于该数据集训练的 Consistency Check 模型，在 100K 匹配预算下达成 60.32% 的准确率，高于 FineLeanCorpus（46.53%）和 NuminaMath-LEAN（41.49%）。
MathForm 支持数学命题从自然语言或半形式化表达向 Lean 4 代码的自动化转换，旨在提升定理证明与形式化验证效率。
