AI写数学题，最麻烦的不是答案不够像，而是推理看着顺，却可能悄悄跳步。Magenta把解题变成类似“写程序—看报错—再修改”的循环：模型先用自然语言作答，再把题目和答案改写成Lean 4语句。Lean——一种编程语言兼证明助手——随后逐步检查证明，不会因为措辞流畅就放过错误。
这里最关键的一步，是先检查“送进Lean的题”有没有被偷换。Lean只能证明某条形式化语句成立，却不知道它是否忠实表达原题；Magenta因此加入statement judge，专门拦截遗漏条件、改动常数或让问题变得过于简单的形式化版本。若证明失败，另一名error judge再判断问题出在数学思路，还是Lean代码，只返工对应环节，而非从头盲目重试。
这套流程不需要额外训练。作者报告称，它搭配开放权重的K2-Horizon-7B时解出了IMO 2026全部六题；消融分析还显示，检查题意一致性有助于避免“证明是真的，但证明了错误命题”的假证书。不过这些效果目前来自论文作者的评测。