问Lean 4自动证明离数学家多远？

面壁智能 OpenBMB 开源了 MathForm，尝试把自然语言数学题自动转成 Lean 4 可验证证明。谁最需要这类工具：数学家、形式化工程师，还是训练推理模型的 AI 团队？它究竟解决什么问题，是降低形式化门槛、扩充训练数据，还是直接替代人工证明？项目给出的 FormalVerse 已包含 367K+ 个验证示例，这个规模让“可执行的数学语料”第一次具备了工程化想象空间。

为什么 Consistency Check 值得关注？在匹配 100K 预算下，MathForm 训练模型达到 60.32%，而 FineLeanCorpus 为 46.53%、NuminaMath-LEAN 为 41.49%。但一致性提高不等于数学创造力已经解决：什么时候可以信任模型生成的形式化结果，什么时候仍必须由专家检查？如果训练集、证明器版本或题目分布变化，这些结果应该在哪里复现和审计，才能排除数据泄漏、模板记忆与指标偏差？

如何判断 MathForm 是一次数据集突破，还是数学研究工作流真正转折点？可以选一批竞赛题、教材定理和研究级命题，比较形式化成功率、人工修订时间、Lean 4 编译通过率及跨版本稳定性。进一步追问：人应保留选题、定义与证明策略，还是只负责验收？欢迎做过 Lean、定理证明或数学大模型的朋友分享真实案例：它在哪类任务上已经省时，在哪类任务上仍会“形式正确但思路无效”？