RecodeX 重构消息，OpenBMB团队开源数学自动形式化框架、数据集与模型MathForm，旨在解决数学形式化中代码可编译但语义不准确的问题。该框架采用检索增强与验证引导的数据构建机制，经最多三轮修正保障代码与语义统一。团队推出含超36.7万个已验证Lean4示例的FormalVerse数据集，基于其训练的模型一致性检查率显著优于同类。核心模型MathForm-8B以四分之一参数体量反超更大模型，在多项基准测试中表现出较强推理与形式化纠错能力。