Magenta 将自然语言数学推理与 Lean verification 闭环连接，并用 statement judge 阻止错误形式化获得“假证书”

Magenta 是一个 training-free agentic pipeline：从自然语言数学题出发，先给出解答，再生成 Lean 4 statement 与 machine-checked proof。系统额外加入 statement judge，检查形式化陈述是否忠实保留原题语义；当证明失败时，error-attribution judge 判断问题应回到数学重新推导，还是进入局部 Lean repair。论文报告其在所评测的 olympiad benchmarks 上达到 100% accuracy，并在搭配 K2-Horizon-7B 时解决全部 6 道 IMO 2026 题。