# LLMs Can Search More Proofs. Can They Choose the Right One? **Summary:** Timothy Gowers argues that AI's mathematical edge may come from searching more paths, not from a special gift for counterexamples; my read is that the next useful metric is how well a model chooses and abandons proof directions. - Canonical: https://markhuang.ai/news/llms-search-more-proofs - Language: en - Author: [Mark Huang](https://markhuang.ai/about) - Published: 2026-08-12 - Section: News - Tags: AI, Mathematics, LLMs, AI Evaluation, Research - 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/ --- ![A dense chalk search tree with many dead ends and one path reaching a clean geometric construction](https://cdn.markhuang.ai/news/llms-search-more-proofs/hero.webp) *A fast search can visit more branches. The harder question is whether the system knows which branch deserves another hour.* Timothy Gowers has proposed a better question for the latest AI mathematics results: [what style of mathematical search are LLMs good at?](https://gowers.wordpress.com/2026/08/12/what-sort-of-maths-are-llms-good-at/) His essay arrived after OpenAI published [ten results in mathematics and theoretical computer science](https://openai.com/index/ten-advances-in-mathematics/) on August 1, 2026. OpenAI says an internal version of Astra generated the arguments, humans prepared the manuscripts with the model, and the model then formalized each argument as a Lean certificate. The company estimates that finding all ten solutions used about $2,000 worth of tokens at its Sol API rates. My read is that the headline count is less revealing than the shape of the search behind it. A model can know more standard techniques than any one person and attempt them at computer speed. That can produce serious mathematics. It still does not tell me whether the system can recognize a promising direction before brute force becomes too expensive, or abandon a polished dead end before a human reviewer wastes a day on it. ## "Counterexample" describes the result, not the skill Gowers starts from an arresting pattern. Several prominent AI results have been constructions that disprove conjectures, including the Erdős unit-distance conjecture, while OpenAI's August list includes the first construction of a non-sofic group and a superexponential lower bound for multicolor triangle Ramsey numbers. It is tempting to conclude that LLMs have a special talent for counterexamples. He then spends much of the essay showing why that classification is slippery. A mathematical statement can often be rewritten by changing its quantifiers without changing the work required to prove it. An object may be called an example when nobody strongly expected the opposite statement to hold, then called a counterexample when it overturns a belief. The label carries mathematical history and expectation, not merely logical form. A benchmark organized around "proofs versus counterexamples" may measure the packaging of the answer instead of the mechanism that found it. Gowers offers a more plausible hypothesis: current models benefit when broad mathematical knowledge and repeated attempts can cover a large search space. Some existence problems happen to reward that style, but plenty of proofs can too. ## The missing metric is search quality I find the search-tree framing useful because it separates two capabilities that a finished paper hides. The first is breadth: generate many candidate constructions, combine familiar tools, and keep trying. The second is judgment: notice that one weak signal is genuine progress, then prune the other branches. LLMs clearly have an unusual advantage on breadth. The evidence for judgment is harder to read. Gowers writes that his conversations with ChatGPT 5.6 Pro often produce approaches that sound promising until he examines them, or a sequence of supposedly narrower reductions that does not obviously move the problem forward. He is careful not to call this a permanent limit. His point is narrower: polished proofs in training data show successful routes, but usually hide the false starts and choices that led to them. > **Info:** > > A proof benchmark tells me whether the final branch works. A research benchmark should also tell me how many branches were explored, who selected the winner, how failures were counted, and what prior literature the system could retrieve. OpenAI's earlier [First Proof report](https://openai.com/index/first-proof-submissions/) shows why this distinction matters. The company ran an internal model on ten unpublished research-level problems and judged at least five attempts likely correct after expert feedback. It later changed its assessment of problem 2 from likely correct to incorrect. OpenAI also disclosed that humans sometimes suggested retrying strategies that had looked fruitful, selected the best of several attempts, and helped coordinate verification and presentation. The company called the sprint less controlled than it wanted. Those disclosures make the results easier to interpret because they show exactly where human judgment entered the loop. ## Verification is necessary, but it answers a later question Formal verification gives OpenAI's August release a solid base. A Lean certificate can check that a formalized argument follows from its premises. It cannot tell us whether the route was novel, whether a nearby argument already existed in the literature, or how many failed runs preceded the successful one. Someone must also review whether the original informal problem was translated faithfully. Natural-language proof checking remains its own weak point. The July 2026 [AdvancedMathBench paper](https://arxiv.org/abs/2607.11849) evaluates proof generation on 245 undergraduate and doctoral qualifying-exam problems. Under its conservative evaluation, GPT-5.5-xhigh scored 64.5% on the undergraduate split and 48.9% on the qualifying-exam split. Its separate verifier benchmark found that the strongest systems still had trouble rejecting subtly invalid proofs. A model that proposes more candidates also creates more checking work unless verification improves with generation. This is the same reason I am wary of reducing any agent to one leaderboard number, a point I explored in [what AI benchmarks actually measure](https://markhuang.ai/blog/what-ai-benchmarks-actually-measure). For research mathematics, the omitted denominator is unusually important. Ten successes from ten serious attempts would demonstrate something different from ten successes selected from a huge, undisclosed pool. Both may be useful. They imply different costs and different roles for the mathematician. ## What I would ask before trusting the next breakthrough I would want a research result packaged with an account of the search. How many independent runs were made? How much compute did the failures consume? Did a human choose the direction, supply a hint, or select the best candidate? Which literature could the system access? Who checked the informal statement before and after formalization? Public discussion already circles these questions. A [MathOverflow discussion about graduate training](https://mathoverflow.net/questions/511255/what-is-an-appropriate-role-for-llms-in-early-mathematical-research-training/511273) asks whether a model has found a new idea or reconstructed something close to existing work. [Science News's reporting on the unit-distance result](https://www.sciencenews.org/article/ai-guardrails-erdos-math-problem) notes concerns about undisclosed failed attempts, attribution, access, and the burden of checking large volumes of generated mathematics. AI-produced proofs deserve serious attention, along with a clear report of the process that produced them. So, can LLMs choose the right proof? Sometimes, plainly, yes. After ten published results, I cannot write these systems off as pattern matchers that happen to be good at contest questions. But the public evidence still mixes model search, human selection, formal checking, and expert review. Gowers's essay gives me a better way to watch what comes next. I will be most impressed when a system repeatedly chooses a short, surprising route, reaches a valid proof, and shows enough of its search that mathematicians can tell why it worked.