数学与形式推理
突破级
暂无讲解视频
收录解读
这篇论文把数学 AI 从单题求解推进到 mathematician-facing agentic workflow。它关注的是如何协助数学家推进研究，而不是只在形式化证明 benchmark 上提高一点通过率。
这种 framing 对本库重要，因为 AI for math 的真正变化可能来自研究协作界面：提出可探索 conjecture、组织证明尝试、维护上下文、把失败路径转成新线索。
它值得正式收录，因为它与近期 theorem proving agent、lemma library、AI scientist 路线形成互补，代表数学研究 workflow 化的一条明确分支。
它没有更高，是因为数学研究协作的长期价值需要真实数学家使用、跨领域案例和可审计成果来证明。