In recent months several long‑standing open mathematical problems have seen claimed solutions attributed to large language models (LLMs). In May 2024 an internal OpenAI model produced a counterexample to Paul Erdős’s unit–distance conjecture (open since 1946). The following month OpenAI published a proof of the Cycle Double Cover (CDC) problem, and by July reported solutions to ten more open problems; in September they announced a proof of the Navier–Stokes problem. Anthropic released a formalization of Fermat’s Last Theorem and reported progress on bounds related to the Riemann hypothesis. These episodes indicate that models have recently become unexpectedly effective at certain mathematical tasks.
What makes a problem tractable for an LLM?
A simple mental model treats every solution as a sequence of insights separated by development work: insight → work → insight → work → solution. The difficulty of a problem can be seen as the length of the shortest such insight sequence plus the effort required to develop the steps—an idea Tim Gowers expresses as a kind of Kolmogorov complexity modulo experts.
Complexity grows exponentially with the number of required insights: most of the work is the development between conceptual jumps. Experts need fewer hints than novices, because they carry more background. Because you cannot generally predict how many hints a problem needs just by looking at it, researchers use proxies—age of the problem, number of failed attempts, prizes—to estimate difficulty.
What makes a single insight valuable?
An insight typically re‑frames the problem, changing its representation and the subsequent search space. Two things determine its value:
- how surprising it seemed before yet how obvious it looks after; and
- its position in the ordered sequence, since a later hint is only useful after earlier work makes it actionable.
This ordering defeats naive brute force: the hint sequence explores a tree of possibilities where early choices shape later available directions.
Humans search breadth‑first
Humans tend to generate many candidate directions, explore them shallowly, abandon most, and commit to a few promising ones—a breadth‑first pattern. A direction is abandoned if it doesn’t yield encouraging early evidence, because fully developing an idea can take months and researchers require reasons (conceptual promise, early results, or past experience) before committing. Research software attempts to shorten that development time. AI can shorten it enough to flip the search pattern: what used to be prohibitively slow to explore can now be tried end‑to‑end, shifting the whole process.
AI trades compute for time
For models the analogue of effort (t) is compute and tokens: spent on a single trajectory or distributed across parallel agents. Pretraining supplies priors comparable to the background knowledge an expert would need to gather. The bigger difference lies in search style: LLMs perform depth‑first search. Give a model a prompt and it often returns a complete attempt; chain‑of‑thought runs greedily too. Run parallel agents and you get several fully developed attempts in parallel—each either fails or yields an argument that looks plausible.
Left alone, this produces convincing but false proofs. The crucial addition is an automated verifier that can prune completed trajectories and identify correct ones. With such a checker, it becomes rational to expend large compute on uncertain ideas because you can find out within minutes whether a direction works. The limitation is that verifiers can only judge finished arguments, not whether a half‑baked idea is promising.
Different quality thresholds for humans and models
How good must a hint be if you can validate it in five minutes? For humans the quality bar is high—pursuing a hint can mean months of work. For a model the bar is much lower: hints can be ordinary, implausible or barely formed, because the system can rapidly determine whether following them leads anywhere. LLMs therefore let us exchange human time for compute and explore more problems in a shorter span.
Failed attempts become negative hints
The model does not need a definitive direction at the start. Pretraining gives priors about history and past attempts; every failed solution is fed back as a negative hint for the next run. Typical harness structure is:
- Drafter: crafts prompts for the solver using priors and past failures;
- Solver: produces one or many candidate solutions, possibly via multiple subagents;
- Verifier/Checker: validates whether an argument establishes the claimed result.
Prompts used in the CDC campaigns explicitly instructed the model to assume the existence of a complete affirmative proof (so that the model wouldn’t stop just because the statement was open in its training data) and to exclude catalogues of partial or substitute results. They also listed adversarial checks—exactly the catalogue of failure modes the verifier should guard against. Each of these lines encodes previous failed paths as instructions steering future runs.
Reconstructing the unit‑distance counterexample
Gowers’s three hints for unit‑distance map neatly to the harness pattern:
- Hint 1 — look for a counterexample: hard because both community priors and model pretraining tend to assume the conjecture is true. The drafter likely adopted this because solvers repeatedly failed trying to prove it.
- Hint 2 — generalize the best known construction: a standard community move; the heavy development work sits here.
- Hint 3 — try number fields of increasing degree: standard machinery once the problem is reframed by the first two hints.
Order matters: starting at hint 3 without the counterexample framing would not point toward a disproof. Even with the three hints, the remaining effort was large. Jacob Tsimerman (recently hired by OpenAI) worked on the counterexample; he knew the number theory and considered increasing degrees, but stopped—not from lack of skill, but because of the human cost of persisting in a swamp with no clear evidence of payoff. Models do not face the same psychological costs and can keep playing in treacherous regions until a crucial idea appears.
Other proofs and what changed in models
OpenAI’s Navier–Stokes proof, per a cursory reading, completes the program of Córdoba and Martínez‑Zoroa; the manuscript is long and corrected often, but conceptually it does not introduce many more leaps. Anthropic’s Fermat and Riemann artifacts show the same skeleton: hundreds of failed ideas, multiple agents under orchestration, many scripts and checkers, and a small number of conceptual jumps shouldering most of the work.
Three capabilities improved this year and help drive such proofs:
- models are better at chaining primitives across long horizons (reducing t);
- self‑verification lets models catch incorrect steps inside a trajectory before a human or external verifier sees the output (cheaper internal pruning);
- orchestration: models can command subagents, use memory to steer runs and build up negative hints (coordinated search).
Branching factor and where models excel
Gowers’s informal formula omits branching factor b: if there are b plausible next hints at each step, k hints give b^k paths to explore. Humans keep effective b small via taste and judgement; models often pursue many plausible branches but can do it quickly. This implies models perform well when b^k × compute cost is small—i.e., when the search space is narrow or when an early insight collapses many branches. The unit‑distance counterexample worked well because the counterexample hint collapsed the solution space and reduced b.
That also explains why some domains (e.g., certain cybersecurity tasks) fell early: professionals know the solution shapes in advance and the intermediate branching is low, so a model can fill the technical slots quickly.
Where humans may retain the edge
Humans likely keep an advantage on problems whose search trees are both deep and highly branching: very large b and/or large k where intuition and rigorous pruning matter. Humans are good at shrinking branches; models are good at shrinking the wall‑clock time to prune an individual branch. The complement works best if we can inspect the models’ failed attempts, because much insight resides in why certain approaches failed. If all we ever see is the final result, we lose the explanatory journey that builds communal understanding.
Terence Tao describes solving problems as a proxy for the deeper goal of mathematics: increasing our collective understanding. A final theorem announced without the surrounding development risks missing the community‑level advances that come from explaining why approaches were tried and why some failed.
Short thought experiment: could an LLM rediscover General Relativity?
Some have proposed training a model on data up to 1901 to see whether it rediscovers the General Theory of Relativity. The argument here is that the key hint—treat gravity as geometry—collapses the solution space sufficiently. The mathematics after that is hard, which is a domain where a model could excel. A depth‑first chain‑of‑thought might reach the geometric framing after many failed attempts; once that hint appears, verification could confirm the theory. The example highlights the broader point: a few surprising conceptual jumps plus heavy technical development is precisely the circumstance in which current LLM pipelines perform well.
Conclusion
Recent LLM successes in mathematics arise from a combination of depth‑first search, the ability to trade compute for human time, internal and external verification layers, and orchestration of parallel agents. These systems can pursue many weak hints cheaply and accumulate negative hints to steer future attempts. Humans and models bring complementary strengths: human intuition narrows the search, while models can quickly explore and prune many branches. Problems demanding many conceptual jumps or having very large intermediate branching remain hard for both; much of the value of solving problems will continue to lie in the shared understanding built by the process, not only in the final statements.
