# 大模型能搜出更多证明，但会选对路吗？

**Summary:** Timothy Gowers 认为，AI 的数学优势可能源于搜索了更多路径，而非对反例有特殊天赋；在我看来，下一个有用的评估指标是模型选择和放弃证明方向的能力。

- Canonical: https://markhuang.ai/zh/news/llms-search-more-proofs
- Language: zh-CN
- Author: [Mark Huang](https://markhuang.ai/about)
- Published: 2026-08-12
- Section: News
- Tags: 人工智能, 数学, 大语言模型, AI 评估, 研究
- Source: [Gowers's Weblog](https://gowers.wordpress.com/2026/08/12/what-sort-of-maths-are-llms-good-at/)
- License: https://creativecommons.org/licenses/by-nc/4.0/

---

![一棵密集的粉笔搜索树，有许多死胡同，只有一条路径通向一个干净的几何构造](https://cdn.markhuang.ai/news/llms-search-more-proofs/hero.webp)

*快速搜索可以遍历更多分支。更难的问题是，系统是否知道哪个分支值得再花一小时。*

Timothy Gowers 就最新的 AI 数学成果提出了一个更好的问题：[大语言模型（LLMs）擅长哪种数学搜索？](https://gowers.wordpress.com/2026/08/12/what-sort-of-maths-are-llms-good-at/) 这篇文章写于 OpenAI 在 2026 年 8 月 1 日公布[十项数学与理论计算机科学成果](https://openai.com/index/ten-advances-in-mathematics/)之后。OpenAI 表示，论证由其内部版 Astra 模型生成，人类与模型协作整理手稿，再由模型将每条论证转化为 Lean 形式化证明。该公司估计，找到这十个解法总共消耗了约 2000 美元的 Sol API 调用额度。

在我看来，比起最终成果的数量，背后搜索的形态更能说明问题。一个模型可以掌握比任何个人都多的标准技巧，并以计算机的速度尝试它们。这确实能产出严肃的数学成果。但它依然无法告诉我，系统能否在暴力穷举变得过于昂贵之前识别出有希望的方向，又能否在人类审稿人浪费一整天之前，及时放弃一条精致的死路。

## “反例”描述的是结果，而非技能

Gowers 注意到了一个引人注目的现象：近年来几项亮眼的 AI 数学成果，都是用来推翻猜想的构造——Erdős 单位距离猜想就是其中之一；OpenAI 八月公布的成果里，也包含首个非 sofic 群的构造，以及多色三角形 Ramsey 数的超指数下界。很容易由此得出一个结论：LLMs 天生擅长找反例。

但他用文章大半篇幅说明，这种分类其实站不住。一个数学命题常常可以换一种量词写法，证明难度丝毫不变。没人强烈预期反面成立时，构造出来的东西叫“例子”；等它推翻了一个普遍信念，又变成了“反例”。这个标签背后是数学史和人们的预期，不只是逻辑形式。

围绕“证明 vs. 反例”来设计基准测试，衡量的可能只是答案的包装方式，而非找到答案的思路。Gowers 提出了一个更合理的假设：当前模型之所以表现好，是因为广博的数学知识加上反复尝试，能覆盖足够大的搜索空间。某些存在性问题恰好适合这种打法，但很多证明问题同样吃这一套。

## 缺失的指标是搜索质量

我觉得搜索树这个框架很有用，因为它把最终论文里看不见的两种能力分开了。一种是广度：大量生成候选构造，组合熟悉的工具，一遍一遍地试。另一种是判断力：察觉到某个微弱的信号其实是真正的进展，然后砍掉其他分支。

LLMs 在广度上的优势显而易见，但判断力的证据就没那么好读了。Gowers 写道，他跟 ChatGPT 5.6 Pro 聊天时，对方经常给出听起来很有前途的思路，等他仔细一看就不行了；或者一连串号称在缩小范围的归约步骤，走完发现离问题并没有更近。他谨慎地没有把这说成永久性限制，他的观点更具体：训练数据里那些打磨好的证明展示的是成功路线，但把路上的弯路和取舍全藏起来了。

> **Info:**
>
> 证明基准只能告诉我最后那条分支通不通。研究基准还应该告诉我：一共探索了多少分支、谁拍板选了赢家、失败怎么算的、系统能查到哪些已有文献。

OpenAI 早先的[《首次证明报告》](https://openai.com/index/first-proof-submissions/)正好说明了这种区分。他们在十个未发表的研究级问题上跑了内部模型，经过专家反馈后，判定至少五次尝试可能是对的。但后来又把问题 2 的评估从“可能正确”改成了“不正确”。OpenAI 还透露，人类有时会建议重试那些看起来有希望的策略，从多次尝试里挑出最好的，还帮忙协调验证和呈现。公司自己都说这次冲刺的控制程度不如预期。这些细节让结果更好理解，因为它们清楚地标出了人类判断在哪些环节介入了。

## 验证是必要的，但它回答的是后续问题

形式化验证给 OpenAI 八月这批成果打了个好底子。Lean 证明能检查形式化后的论证是否从前提推出，但它回答不了这条路线是否新颖、附近有没有已经发过的类似论证、成功之前到底失败了多少次。原始的非形式化问题有没有被忠实翻译过来，也得有人去看。

自然语言证明检查依然是短板。2026 年 7 月的[AdvancedMathBench 论文](https://arxiv.org/abs/2607.11849)用 245 道本科和博士资格考试题评估了证明生成能力。在保守评估标准下，GPT-5.5-xhigh 本科部分得分 64.5%，资格考试部分只有 48.9%。他们单独的验证器基准测试也发现，最强的系统在识别那些微妙出错的证明时仍然吃力。模型生成的候选越多，需要检查的量就越大——除非验证能力也能跟着生成能力一起涨。

这也是为什么我一直警惕把任何智能体简化成一个排行榜数字，我在[《AI 基准测试究竟衡量了什么》](https://markhuang.ai/blog/what-ai-benchmarks-actually-measure)里讨论过这个问题。对研究数学来说，那个被忽略的分母尤其关键。十次认真尝试拿到十次成功，和从一个巨大的、未公开的池子里筛出十次成功，完全是两码事。两种都有用，但意味着不同的成本，也意味着数学家扮演不同的角色。

## 在相信下一个突破之前，我会问什么

我希望看到的研究成果，能附带一份搜索过程的说明。跑了多少次独立实验？失败的那些烧了多少算力？方向是人选的、提示是人给的、最佳候选是人挑的吗？系统能访问哪些文献？形式化前后，谁检查过原始的非形式化陈述？

公开讨论已经在围绕这些问题展开。[MathOverflow 上关于研究生培养的讨论](https://mathoverflow.net/questions/511255/what-is-an-appropriate-role-for-llms-in-early-mathematical-research-training/511273)就在问：模型到底是找到了新想法，还是重构了接近现有工作的东西？[《科学新闻》对单位距离结果的报道](https://www.sciencenews.org/article/ai-guardrails-erdos-math-problem)也提到了人们的担忧：未公开的失败尝试、署名权、访问权限、以及检查大量生成数学内容带来的负担。AI 生成的证明值得认真对待，但也需要一份清晰的过程报告，说明它们是怎么来的。

那么，LLMs 能选出正确的证明吗？有时候，答案显然是肯定的。十项成果发表之后，我没法再把这些系统简单看成碰巧擅长竞赛题的模式匹配器。但目前的公开证据仍然混杂了模型搜索、人类选择、形式化检查和专家评审。Gowers 的文章给了我一个更好的视角来看接下来的发展。什么时候一个系统能反复挑出一条简短而出人意料的路径、给出一个有效证明、并且把搜索过程展示得足够清楚，让数学家能看懂它为什么行——到那时候，我才会真正被打动。