这个工具是做什么的
OpenBMB 开源的数学自动形式化方案（Apache-2.0）：含 MathForm-8B 模型权重、约 36.7 万条经 Lean 4 验证的数据集 FormalVerse、评测代码与 Pass@k 脚本。通过检索 Mathlib 加编译器反馈迭代生成可验证的 Lean 4 命题，8B 模型在多个基准上超过 32B 专用形式化模型，BF16 加载约需 16GB 显存即可本地运行。
基本信息
- 分类：开发者工具
- 厂商 / 团队：OpenBMB
- 价格：开源免费
- 收录日期：2026-08-23
- 官网：github.com
适用场景
数学形式化 · Lean 4 · 开源 · MathForm · OpenBMB