大模型数学与Lean之争
_AndrewZhao · x · 2026-07-19
转发讨论大模型在数学任务上为何不大量使用 Lean。作者把“在单轮里把 Terminal Bench 跑满”的做法比作一种奇怪的优化方向，并借一则夸张的“Achieves perfect IMO 2026 scores, with Lean proofs attached”来反讽。 核心意思是：真正值得关注的不是单纯刷题分数，而是**数学推理、形式化证明与评测设计**之间的关系。帖子本身没有给出新结论，但指向了一个研究与工程都在意的问题：大模型数学能力到底应该怎样被验证、怎样和 Lean 这类形式化工具结合。