来源： Invited Talk 03 · Tim Gehrunger 播客： ICML 2026 · AI4Research 分类： AI 研究 原文发表： 2026-07-10 纪要生成： 2026-07-13
面向数学家的"如何实用地用 AI 做研究"实操指南：先教"能省钱就别上 agentic"（订阅内模型、arXiv-math 基准、Codex/Claude Code 查稿），再深入介绍 ETH 团队开源的 ProofCouncil harness（offer + stateful critic + fresh critic + LLM council + compute worker），并给出其在 First Proof 竞赛第二批上的硬核战绩——9 题解出 6 题、成本约为 GPT-5.5 Pro 单查询的 30 倍但解题数从 4 提到 6；核心结论：agentic 系统能解真实开放数学问题、超过单次查询，但只有配最强模型才值得。
Gehrunger 特意让讲座对"只做数学/只做研究"的人也可懂（会解释一些 ML 术语，请 ML 听众包涵）。他用一个"小测验"开场，三题：
要点：大量 agentic AI for math 的本质，就是以结构化方式追问模型"看看你的输出、真的对吗？"
Agentic AI 的通俗定义：给模型一个目标，让它自行规划、调用工具、检视输出、迭代，全程无需你再输入。注意它贵——多数应用要通过 API 调用（按用量计费，不含在订阅里）。他的第一条建议就是：先试订阅内能不能解决，agentic via API 贵得多；而如今用较新的贵模型一次调用就解出研究级问题的概率并非微不足道。
一个例证是 Math Arena 上的 arXiv-math benchmark：每月从 arXiv 抽取"有最终答案"的文章题目（最终答案可能是 23、或多项式 x^5−2），检查那些训练截止早于文章发表、且无法访问原文的模型能否找出该最终答案。当然模型可能答案对而证明是胡说，但检查证明会难得多。结果最新模型都到很高：Fable 86%、GPT-5.5 近 80%——而这两个都含在 $20 订阅里。也就是说，便宜模型也能在四分之三以上的研究级问题上给出正确最终答案（未必正确证明）。所以：先试非 agentic AI。
另一省钱法是用命令行界面（CLI）——它驻留在你的命令行、能访问文件、在你的机器上跑代码。例子：OpenAI 的 Codex、Anthropic 的 Claude Code。它们重度为编码优化、做数学比前沿模型稍弱，但仍可用。一个极佳用例是检查论文草稿：把文章源文件的副本给 Codex/Claude Code，让它写一份报告——常常效果很好，现在的模型已强到能找出严肃的数学错误。用"写报告"而非直接改，你对任何改动完全可控。他见过一些对 AI 很怀疑的人，一旦让他们用这种方式审自己的文章，立刻就很上头。
要做长时运行、榨出模型最大性能的工作流，目前唯一现实的方式是 harness。harness 是一个编排系统：决定以何种方式调用哪些模型以达成目标——它不发明新模型、不训练模型，只是调用并下指令。使用方式类似聊天机器人：给一个（或一列）问题，返回一个 tex 文件。
在 First Proof 竞赛（一群高水平数学家把自己尚未发表的研究做成题目）里，一支以 ETH 为主的团队开发了 ProofCouncil harness，表现优异（大概正因如此他被邀来讲）。
流程从左侧的问题陈述开始：
记忆的内容：当前证明草稿、offer 已找到的研究笔记与参考文献、critic 的反馈、council 的回答、compute worker 的输出。compute worker 能存文件、随时间累积一个代码库。
一轮的样子：offer 更新证明文件 → critic 找证明漏洞或认可 → 若 stateful critic 认可，fresh critic 再找问题。停止条件：offer 与两个 critic 都认可（返回解）；或触及预设上限——如只到第 30 轮、只花 $1000、证明至多 30 页、或只算一天等。
部署建议：让 Codex 帮你 clone GitHub repo、装依赖、配 API key、跑测试、把输入题目整成正确格式——避免手误烧钱。机器需始终联网，建议用服务器（AWS 或高校的）；但别太担心租服务器的钱，因为 API 调用比任何 AWS 费用贵好几个数量级。再次强调：先用常规 AI 复核你的问题是否良定义、有无简单解/错误，能省大量预算。
备赛时他们请 ETH 数学家提供自己的开放问题（因为相信自己 setup 够强、也不想麻烦对方去想"已知答案的题"）。最终拿到 21 份反馈（他说做 slide 后又多了些）：5 题验证为对之前开放问题的完整解、2 题仍在核验但大概也对、还有若干有用的部分产出。有两题几乎到"100%"却被标为"误解问题"——他不甩锅给模型：所谓"误解"其实是模型注意到项目/题目陈述里有小瑕疵、可被利用，能构造出使陈述实际为假的边缘情形，这是人（他们）没提前检查好，不是模型的错。
赛前 ETH 的开放题用完后，他们跑了几道 Erdős problems（Erdős 留下约上千问题；近来"LLM 解出部分 Erdős 题"成趋势，多数并非顶尖研究级，有些只是无人问津）：
First Proof 第二批是受控环境（第一批不那么受控，大 AI 公司随便发挥）：所有提交的 harness 必须开源（他们的也是）；10 道由数学家未发表工作改成的真实问题；每题配一份人类写的 8 页解答（由出题者提供）。规则：提交的 harness 只收题目、返回 LaTeX 解答文件、只能用公开可得的模型与工具、24 小时跑完全部。他们的系统尝试了全部 10 题。而且——First Proof 组织方真的付钱请数学家逐份评阅、每题至少两人独立打分，这份投入很不寻常。
结果（人类逐题细评、每题≥2 人独立）：
最终 9 题解出 6 题。
总花约 $3000：offer 占近一半，critics 占约三分之一（council 三个模型 Gemini、Claude、GPT，其成本差异很大），compute worker 不贵（AWS 成本 < API 成本的 1%）。每道被分析的问题约 $350。且近一半的钱花在没解出的题上。
critic 审查每份草稿的漏洞、错误、缺失假设、引用问题（也看 LaTeX 是否编译，但现代模型这不成问题）。fresh critic 多次救场：如问题 10，stateful critic 在 7 次迭代中都认可了中间版本，但 fresh critic 全部否掉——即有记忆的 critic 几乎与 offer"合谋"、被 offer 诱导认可不该认可的东西。也有两处失误：问题 8 被认可但实有漏洞（一处只是被模型断言、无证明，critic 却说"当然对"，人类指出这里需要证明）；问题 3 stateful 与 fresh critic 反复拒绝，但人类评审最终认可（判断只需小修）。两个方向各一次失误，但其余情形都能猜中人类会怎么判。
council 是一组前沿模型，在主 critic 循环外回答 offer 的定向提问，共三个：
多模型的初衷是多样性或有帮助。是否真有用尚需更多测试，但 Claude 在问题 3 的纠正（同一轮里 GPT 没找到）可算证据——说明"不止放 10 个同款模型副本"或许有用。
跑在 Codex 上，处理定向计算、代码开发、繁重的文献核查，有持久工作区可累积代码库，并被授予 GAP、SageMath 等数学软件。它在 5 道较难题上被大量使用，主要角色是文献搜索与直接核验草稿中的断言，多次找到模型陈述的反例，效果很好。一条批评是：有些解答的引用不支持所作断言——明确的改进点，未来或让 critic 也配一个 compute worker 专门逐条核查引用。
First Proof 组织方跑了 GPT-5.5 Pro 基线（单次查询）：9 题解出 4 题，而 ProofCouncil 解出 6，但贵近 30 倍——这也印证"先看便宜方案能否解"。在两者都解出的题上，ProofCouncil 只贵约 4 倍（较宽慰），说明钱主要花在没解出的题上。此外，GPT-5 Pro 单查询对所有题都声称给出完整解、且完全不表达不确定；而 ProofCouncil 会说自己对哪两个答案没把握（其中一个最终仍对）——"希望模型对正确与否更诚实些"。
Q1（听众，做物理方向）： 这类 agentic harness 是真的带来根本性的新能力，还是只是略微增强单模型？我自己在物理（模型在物理上不如数学强）跑这些 harness 的经验是后者——也许比单模型好一点，但等几个月，下一代模型就比整个 harness 还强。 A1： 谢谢。我要是知道确切答案，大概就去 AI 公司赚更多钱了。在开放问题测试里，我们感觉它明显更强：有些解出现在很深的轮次——一道开放题在第 25 轮才解出（作者写、critic 审的循环发生了约 25 次）。所以在我看来这不止是 GPT-5.5 到 5.6 那种提升。当然，未来会给出答案。
Q2（听众）： critic（无论有无记忆）拒绝时的反馈多详细？比如会说"你第 17 步错了"吗？ A2： critic 会给 offer 一个 tex 文件，说明"这错了、为什么错"，并尽力解释清楚。
Q3（同一听众追问）： 你们测过吗——当 critic 判错时（它给的"错误原因"本身是错的）？ A3： 问题在于这需要真正深入这道题的数学；而我们拿到的大多问题不在我的方向（arithmetic geometry）上，所以没那么细看。但这确实很值得做。（主持人补充：所有日志都公开，有兴趣者可自行查看。）