On July 18, 2026, Chao Xu, Associate Professor at the School of Computer Science at UESTC, published AI Agents for the Working Mathematician. He shared how he organized hundreds of subagents to search for proofs, counterexamples, and intermediate lemmas for open mathematical problems over extended periods.
The most conspicuous feature of this protocol is its rigorous quality control: candidate proofs must undergo targeted error-finding, reconstruction from scratch, and cross-model review. However, viewing it merely as a stricter peer-review mechanism misses its deeper design. The protocol also manages the route exploration that precedes the formation of conclusions.
These two activities pull in opposite directions. Route exploration requires tolerating a large volume of immature ideas; without that, new paths cannot be discovered. Subsequent derivation, however, must isolate those immature ideas to prevent hidden logical gaps from becoming premises for the entire project. Chao Xu’s approach splits them into two feedback loops: one decides what the next round of budget should explore, and the other decides which results can enter the shared premise. This is its most intriguing insight for AI knowledge work.
Suppose we are proving a fixed mathematical proposition. Before writing begins, no one can pre-list the complete proof route. The search for a proof is highly open-ended: one may look for counterexamples, pivot to an intermediate lemma, or try a different construction. The target is fixed, but the paths leading to it are unlimited.
Yet once a candidate proof is written out and enters the judgment phase, the requirements become extremely strict. Even if the entire derivation is profoundly illuminating, a single misused quantifier, a missing boundary condition, or a key step that depends on an unproven premise will render the proof invalid. Under a frozen proposition, logical gaps admit no compromise.
Strict judgment does not mean checking is easy. If candidate proofs are written in formal language, we can hand them to a proof assistant for verification; if they are concrete counterexamples, we can compute the substitution directly. However, natural-language proofs that have not yet been formalized currently lack cheap universal checkers. The AI Co-Mathematician paper notes that AI can generate dozens of pages of proof drafts in minutes, while a human expert may need days to verify them. This creates an extremely asymmetric verification cost.
Mathematical research sits precisely at the intersection of these two contradictions. On one hand, like other forms of knowledge work, it requires open-ended exploration along unknown paths. On the other, like software testing, it demands logical judgment with no room for negotiation.
This does not mean there are mutually exclusive boundaries between professions. In fact, tasks shift across phases: a software project, for example, moves from requirements exploration to implementation after the specification is frozen. The task map below illustrates this dynamic distribution: the same task, after being formalized or having tests written, changes both its verification difficulty and its position on the map.
This tension is also widespread in security vulnerability analysis, novel algorithm design, and complex scientific discovery. Mathematics serves as a high-contrast case because it pushes the tension to the extreme: routes cannot be pre-scripted, judgment cannot be compromised by preference, and natural-language proofs lack cheap automated tests. To resolve this conflict, exploration and judgment must be decoupled into two different loops.
When exploring an open proposition, a long-duration run does not mean letting a single model write online for dozens of hours. Instead, the coordinator must frequently switch among activities such as proof derivation, counterexample search, and intermediate lemma construction, allocating compute budget across multiple solution routes.
The system must persistently record the state of the entire
exploration process. First, the coordinator writes the target
proposition into STATEMENT.md, thereby fixing the research
endpoint.
In specific path searches, the agent records every attempt in
REGISTRY.md. This route log registers not only “what has
been tried” but also where each route got stuck, what logical obstacles
were encountered, and which next-stage test will determine life or
death. When new agents take over a task, reading this log prevents them
from retrying routes already shown to be dead-ends due to sampling
randomness.
If a proof search gets stuck on an unknown lemma that is as difficult
as the original proposition, the system does not label this route as
“close to success.” The coordinator marks it as blocked, records it in
FAILED.md, and immediately cuts the compute budget for that
direction. Only when other exploration branches produce new mathematical
mechanisms, constructions, or evidence may this blocked route be
reactivated.
After repeated attempts and rollbacks, the exploration loop may
eventually produce a proof that appears complete. At this point, the
system labels it candidate. Even if the agent that
generated the proof performed a self-check, the label can only be
upgraded to self-audited. To subsequent agents, these two
labels are indistinguishable: neither may be cited as an established
theorem.
When a candidate proof emerges from exploration and needs to serve as a credential for downstream derivation, the promotion loop is triggered, cross-verifying it through multiple lines of defense.
First, the proof must undergo a hostile audit. The agent playing the adversary is solely responsible for finding flaws: attempting to construct concrete counterexamples, checking for logical leaps, hidden premises, and missing boundary conditions.
If the candidate proof passes this stage, the system dispatches a fresh agent for blind reconstruction. This new agent sees none of the original derivation text. It receives only the target proposition and the key ideas recorded in the registry, and reconstructs the proof from scratch in an isolated environment. This step verifies whether the core idea holds independently of the original derivation’s narrative. Its emphasis differs from that of the hostile audit, but if the models in both stages come from the same family, they may still share the same blind spots inherited from common training set biases.
Only after passing both checkpoints can the candidate proof be
upgraded to verifier-backed. When the system writes it into
PROVED.md, its status is formally promoted to
promoted, and subsequent path searches are allowed to cite
this premise. To obtain the independently audited label, a
different model family or a human expert must be introduced. Simply
launching a new instance of the same model family does not count as
cross-family independent review, because they are highly prone to making
the same kind of errors.
The two loops feed back into each other in precisely this way. If the
hostile audit discovers a gap, the proof loses its promotion
eligibility, and the associated route, carrying the latest vulnerability
information, returns to REGISTRY.md or is even written into
FAILED.md and frozen. If the proof is successfully written
into PROVED.md, it becomes a legitimate premise that the
next round of exploration may depend on. The system does not need to
perform global verification on every search, nor does it allow a freshly
generated piece of text to quietly slip into the derivation chain.
It is worth emphasizing that the promotion protocol manages the flow of trustworthy states; it does not directly produce mathematical truth. Cross-model consensus can still be jointly wrong. Chao Xu reported in his post that he deployed hundreds of subagents to attempt ten open mathematical problems, successfully solving three, with each problem running for at least ten hours (unless solved earlier). This is the author’s self-reported empirical data. The problems and run trajectories are not public, and there are no controlled comparisons with the same budget baseline or independent mathematical adjudication; therefore, these should not be treated as a universal benchmark.
Additionally, traces of the protocol’s design mechanisms can be found in prior work. OpenAI’s CDC prompt already contained the ideas of route registration and blocked budget control; Danus explicitly separates generation and verification authority; Chao Xu’s earlier coverify is also a verification scaffold based on multiple reviewers. Chao Xu’s contribution lies in organizing these disparate verification actions into a continuously runnable, resumable long-term mathematical contract.
In the evolution of mathematical research, the ultimate verification tool is formalization. The proof assistant Lean acts like a logic compiler, capable of directly verifying propositions and derivations written in formal language. However, it only checks the formal code that the machine reads; it cannot determine whether a human has faithfully translated a natural-language proposition into code. Its ecosystem library, mathlib, preserves a large body of reusable definitions and lemmas. If a concept not yet in the library is needed, one must define it oneself, fill in the lemmas, and subject them to review. OpenAI’s cdc-lean demonstrates the combination of natural-language drafts with Lean formal proof files. Formalization requires enormous upfront investment, but once a result enters the mathlib library, the verification cost drops dramatically. Chao Xu’s protocol manages precisely the blank territory beyond formalization coverage.
This approach—loosen during exploration, tighten before citation—can directly inspire non-mathematical knowledge work.
Many decision-making, analysis, and strategic planning tasks lack a single arbiter comparable to mathematics. A report may be defensible under several different trade-offs. But even when standards are pluralistic, key intermediate premises still have truth values: cited facts can be inaccurate, and data can be miscalculated. When downstream tasks need to rely on such inferences, we should separate “freshly generated drafts” from “shared premises that the team can directly reuse,” register failed routes, and isolate unverified premises.
Here, we cannot simply promote an entire decision as the single correct answer. A more appropriate unit of promotion is the facts, causal judgments, and constraints within a recommendation. We promote only objective facts with solid evidence to shared premises; for recommendations that depend on value trade-offs, we should preserve their boundary conditions and opposing evidence. Through this isolation, the exploration loop can continue to allow problems and directions to evolve, while the promotion loop only prevents unverified hypotheses from masquerading as team consensus.
The position of software engineering also shifts with phases. During requirements discovery and architectural design, teams likewise need a high degree of exploration, and specifications often crystallize through implementation. Once the specification is frozen, we should prioritize executable checks such as compilers, automated tests, schema validation, and dry runs. For these lower-cost verification methods, automated test coverage should be expanded first; “consensus” arrived at by a few agents discussing among themselves must never substitute for actual tests. Only premises that lack automated test coverage yet will affect downstream implementation—such as SDK compatibility judgments or security assumptions that cannot be auto-tested—are suitable candidates for isolation and fresh-agent blind reconstruction.
This dual-loop workflow does not eliminate the creativity of research. It preserves exploration’s most important freedom: once a target is set, routes can be reconstructed at any time. At the same time, it establishes an explicit constraint: an idea is free to appear, but before it alters anyone else’s derivations, it must first demonstrate which checks it has passed.