AI数学突破：深度优先搜索与验证器

In May, an internal model at OpenAI found a counterexample to Erdős's unit distance conjecture. Open since 1946. Many experts had tried to prove it. OpenAI found a counterexample instead. A month later, OpenAI published a proof of the Cycle Double Cover (CDC) problem, then solutions to ten more open problems by July. And a proof of Navier Stokes in September. Anthropic published a formalization of the fermat's last theorem, and advanced bounds on Reimann's hypothesis. The models are suddenly good at math.

The question that interests me is whether we can predict what kinds of problems these models will solve. What makes a problem tractable for an LLM, and what do these solutions have in common? If AI solves problems differently from humans, identifying the difference should help us decide where to point it. The unit-distance disproof has the richest commentary, so let’s start there.

Problem complexity

Here is a simple mental model. To solve any given problem, you need a sequence of hints or insights with work between them. This maps surprisingly well to simple everyday problems and to complex ideas like General Relativity1 (see Bonus). The sequence looks something like this:

Insight -> time / effort -> insight -> time/effort -> solution.

An expert would need fewer hints than a beginner would, as they would have more background. In his commentary on unit-distance proof, WT Gowers uses a similar idea: the difficulty of the proof is the shortest sequence of hints that would let experts reconstruct it. He calls it Kolmogorov complexity2 modulo experts. For the unit-distance problem, his hint sequence had three parts:

- Look for a counterexample.

- Take the best known construction and generalize it.

- Try a sequence of number fields of increasing degree, but work with prime ideals of bounded norm.

Gowers’ proposed formula for complexity is 2^k + t, where k is the length of the shortest hint sequence and t is the work required to develop it. It is the sort of formula that looks rigorous right up until you try to put a number into it, which is more or less the point. Complexity grows exponentially with the number of insights you need to solve a problem.

Most problem solving is the work between these insights. You have a eureka moment, then spend months developing the hint until another conceptual jump becomes possible. For an expert, time spent is a useful proxy for this work, hence t. Hand someone the first unit-distance hint and they still have to do enough work to reach the generalized construction.

Useful, but post hoc. You can’t look at the problem and predict it would need x number of hints. So, a problem’s age, the number of tries, and the prize attached to it are common proxies to ascribe difficulty.

Characteristics of a given hint

A typical insight changes the formulation of the problem. The representation and understanding of the problem change. Two things decide how much a hint is worth:

- How unlikely it looked before, against how obvious it looks after supplying the hint → This is harder than people realize. In unit distance, many experts did not consider the counterexample as likely.

- Where it belongs in the sequence: hints are ordered. A third hint is useful only after the work on the first two have made enough progress for it to be actionable. This defeats the naive brute force idea of listing a thousand mathematical techniques and trying every combination3 . Hints sequence traverses a tree. Initial insights change the problem and reveal the choices that follow.

Humans solve problems breadth first

Combine k and t and you get the human search pattern. Generate candidate directions, explore them shallowly, abandon most, and commit to a few. A promising direction is abandoned if it does not give enough encouragement early4 . This is a human constraint: Developing an idea can take months. Before committing, a researcher needs reasons to believe it will lead somewhere: conceptual promise, early results, or experience with similar problems. The longer it takes to find out, the higher the bar for trying the idea.

Most research software exists to shrink this time by automating the tedious, mechanical, repeatable work. AI shrinks it far enough that the search pattern itself flips, and everything downstream follows from that.

AI and complexity

First, t. The model’s equivalent of effort is compute and tokens, spent on one trajectory (test time compute) or spread across parallel agents (parallel test time compute). Pretraining also supplies knowledge that a human researcher would have to locate or reconstruct. No individual expert is aware of every previous development, so occasionally they end up redoing things already done.

The bigger difference is how models search:

LLMs are depth first

Give the model a single prompt and it will give you a solution. Maybe correct, perhaps not. Ask for a proof and it will give you something that approaches a good proof. CoT for these models runs in a greedy depth first manner too. And the process scales. Give parallel agents ten approaches and you get ten attempts developed toward a conclusion. Maybe all distinct, or some overlapping. Each either hits a roadblock or produces an argument that looks right. Left alone, this gets you beautiful false proofs.

This seems like a waste of compute and resources, until you add an automated verifier5 that can prune the completed trajectories and identify the correct ones. With this checker, it is now rational to spend enormous compute on uncertain ideas. You find out whether a given idea works or not within minutes. The catch is that the verifier can only judge finished arguments. It cannot tell you whether a half-developed idea is going anywhere.

The contrast

How good does a hint need to be if you can find out whether it works in five minutes? For humans, the quality bar is high because it could take months of work to pursue a hint. For a model, the bar nearly disappears. The hint can be ordinary, implausible, or barely formed. Following it establishes whether it leads anywhere. LLMs enable us to exchange time for compute, and can help us pursue more problems in a shorter timespan.

Failed attempts are hints for LLMs

The model doesn't need a definitive direction to start. Pretraining already gives it priors about the problem's history and past attempts. Every wrong solution can go back to the model as a negative hint for the next iteration. The system accumulates instructions about what has already failed and why. Roughly, a harness looks like this:

- Drafter: writes the prompts given to the solver model. The prompts are based on model priors, mitigating errors from previous runs, and accounting for all the promising paths that went nowhere (these are negative hints).

- Solver: Takes the prompts and comes up with one or many candidate solutions. It can run multiple subagents and pursue different paths using parallel test-time compute.

- Verifier / Checker: Checks whether the argument is valid and establishes the requested result.

For example, consider this CDC prompt:

Assume for purposes of this task that a complete affirmative proof exists. → This prevents the model from treating the problem’s open status, learned during pretraining, as a reason to stop.

In particular, proofs for special graph classes, constructions of cycle covers with some edges covered other than twice, bounded-length or prescribed-cycle variants, reductions to another unproved conjecture, computational verification through any fixed graph size, and candidate counterexamples without a complete nonexistence certificate are insufficient → This rules out a catalogue of substitutes for solving the actual problem.

Use adversarial agents throughout: every candidate proof must be checked for exact-two multiplicity, repeated-edge closed trails masquerading as cycles, parallel-edge 2-cycles, disconnected graphs, cutvertices, bridges introduced by reductions, and circular use of an