Running an AI agent on a mathematical proof for ten hours is easy. Knowing what can be trusted after those ten hours is the hard part. A long run may produce a valid lemma, a plausible argument that its author has repeatedly self-approved, and a dead route that returns under new notation. If all three enter the same context as facts, more inference time only compounds uncertainty.
The scalable unit in mathematical research is therefore not the proof attempt. It is the claim that another agent can safely reuse.
A useful workflow emerges from Chao Xu's AI Agents for the Working Mathematician, his public Coverify project, and related systems such as Danus. I will call it a dual-loop verification protocol:
- An exploration loop searches broadly, records failed routes, and produces candidate claims.
- A verification loop attacks, reconstructs, and promotes only the claims that survive independent checks.
The name is an editorial abstraction used in this article. Xu's article does not present “dual-loop protocol” as a named framework. The two-loop description is useful because it makes the central design choice explicit: exploration is allowed to be creative and non-deterministic; trusted knowledge has a fixed admission process.
The bottleneck is trusted reuse
Proof generation is getting cheaper. A capable model can produce more conjectures, decompositions, computations, and proof-shaped text than a human can review. This changes the system bottleneck from generation to verification.
The immediate temptation is to add more agents. That increases search bandwidth, but it also increases correlated errors, duplicated routes, and review debt. Ten agents can repeat the same attractive gap ten times. A hundred pages of reasoning can still depend on one unproved compatibility claim.
The better scaling question is:
What evidence must a claim carry before another agent may build on it?
This is stricter than asking whether a proof looks convincing. It requires an interface between uncertain work and trusted memory. Tests, formal checkers, hostile reviewers, fresh reconstructions, dependency records, and human review are all versions of that interface.
The same bottleneck appears in our earlier unit-distance case study, where an AI-generated mathematical result mattered only after outside mathematicians checked it. The dual-loop protocol moves that verification boundary inside the daily research workflow instead of waiting until a final theorem appears.
Loop one: explore without polluting the knowledge base
The exploration loop should maximize useful diversity while keeping its outputs provisional.
Freeze the target
Start with a fixed STATEMENT.md. It should contain the exact claim, every quantifier, conventions, known assumptions, and the success criteria. It should also state what does not count as a solution.
This file prevents a common failure mode: an agent finds a nearby theorem, proves a special case, or reduces the problem to a new conjecture, then quietly treats the original task as complete. The target may be revised by the researcher, but it should never drift inside a run merely to fit an available result.
Search by mechanism, not by agent count
Send workers toward genuinely different mechanisms: extremal arguments, algebraic reformulations, embeddings, induction schemes, reductions, counterexample construction, or computation that produces a small certificate. Group them by mathematical mechanism and terminal gap, not by which agent produced them.
Before an agent starts a route, it checks the failed-route record and answers one question: what is materially new here? A renamed variable or a different prompt does not make a new attempt. A new invariant, source theorem, witness, or scope restriction might.
Workers should return a mathematical artifact: a proved lemma, explicit construction, counterexample, certificate, or precise obstruction. “Promising direction” is activity, not progress.
Record failure at the right resolution
A failed attempt is valuable when it prevents the next agent from paying for the same failure. Record the exact obstruction, the smallest counterexample or missing lemma, the evidence, and the condition under which reopening the route would be justified.
This is selective memory, not transcript storage. Raw conversations, repeated summaries, and scratch calculations increase context without increasing knowledge. Xu's Coverify atomic-attempt design makes the boundary concrete: private attempt artifacts remain local; at most one compact, reviewed change is promoted into the durable mathematical knowledge base.
Four files are enough to start
Xu's practical prompt uses four durable files. They form a small state machine for long-running proof work.
| File | Purpose | What belongs inside |
|---|---|---|
STATEMENT.md |
Freeze the target | Exact theorem, quantifiers, notation, assumptions, success criteria |
REGISTRY.md |
Map the search frontier | Approach family, exact claim attempted, remaining gap, smallest obstruction, next decisive test, status |
FAILED.md |
Stop repeated dead ends | Closed route, exact reason it failed, evidence, and a material reopen condition |
PROVED.md |
Hold promoted knowledge | Checked lemmas, constructions, counterexamples, certificates, dependencies, and evidence labels |
The separation matters. REGISTRY.md describes work in motion. FAILED.md stores reusable negative knowledge. PROVED.md contains only claims that have passed the promotion gate. Mixing them turns “someone tried this” into “this is established” through proximity alone.
A minimal registry row can look like this:
ID | mechanism | exact target | remaining gap | obstruction | next test | status
A failed-route entry should answer:
What was attempted?
Where exactly did it fail?
What evidence closes this route?
What would make a retry materially new?
A promoted claim should include its statement, hypotheses, proof or certificate, dependencies, verification history, and current evidence label. The dependency list is essential because a conclusion cannot inherit more confidence than its weakest premise.
Loop two: verify before promotion
The verification loop begins when exploration produces a complete candidate. Its job is not to improve the prose. Its job is to find out whether the mathematical content can survive separation from its author.
Step 1: hostile audit
A fresh agent receives the statement and the candidate proof. It is instructed to refute the proof by looking for quantifier slips, hidden assumptions, invalid citations, mismatched cases, unjustified recurrences, and “routine” compatibility claims.
This review is adversarial by design. An ordinary reviewer often follows the author's route and checks local plausibility. A hostile auditor searches for the cheapest decisive break.
Step 2: blind reconstruction
Another fresh agent receives the original statement and, at most, the claimed key ideas. It does not see the candidate proof. Its task is to reconstruct an end-to-end argument independently.
Blind reconstruction catches a different class of error. A proof can survive line-by-line criticism because the reviewer has adopted the author's framing. An independent reconstruction exposes missing bridges, hidden dependencies, and ideas that only work when the conclusion is already known.
The two checks are complementary:
| Check | What the verifier sees | Best at catching |
|---|---|---|
| Hostile audit | Candidate proof and target | Local gaps, misuse of results, quantifier and case errors |
| Blind reconstruction | Target and limited key ideas | Hidden dependencies, framing bias, missing global structure |
Passing one is insufficient. A proof that survives attack may still be impossible to reconstruct without its author's unstated assumptions. A fresh proof may repeat the same model family's blind spot.
Step 3: cross-family or human review
Independent samples from one model family remain correlated. Xu explicitly separates a fresh same-family check from an outside-family or human audit. If only one model family is available, the honest label is “promoted, cross-family audit pending,” not “independently audited.”
For high-impact results, a domain expert remains the strongest final check. Responsibility for publication stays with the human researcher even when most search and review work is delegated.
Five evidence labels prevent status inflation
Binary labels such as “proved” and “unproved” hide too much about how a claim was checked. Xu proposes five levels:
| Label | Meaning | May later work rely on it? |
|---|---|---|
candidate |
Produced by an agent, no checks completed | No |
self-audited |
Rechecked only by its author or the same context | Treat the same as candidate |
verifier-backed |
Survived hostile audit and blind reconstruction | Yes, with verification record |
promoted |
Verifier-backed and recorded in PROVED.md |
Yes, as durable project knowledge |
independently audited |
Also checked by a different model family or a human | Preferred for final reporting |
The important boundary lies between self-audited and verifier-backed. Self-reflection may improve a draft, but it does not create independent evidence. The author and its self-review share context, assumptions, and failure modes.
Labels also propagate through dependencies. If a promoted theorem uses a merely candidate lemma, the theorem cannot remain promoted. Evidence behaves like a type system: an operation cannot silently cast uncertain input into trusted output.
This is related to the argument in When Should an AI Agent Get Its Own DSL?. A constrained representation is valuable when it makes illegal states detectable. Here, evidence labels and promotion rules create a small language for mathematical trust.
Formal verification is an additional layer
The dual-loop protocol works with natural-language mathematics, computation, and formal proof assistants. These checks should remain distinct.
A Lean proof gives a powerful guarantee: the encoded formal statement follows from the declared foundations and dependencies. Systems such as Prover Agent combine informal strategy generation, formal proof construction, and Lean feedback. Its published benchmark concerns formalized competition problems, a very different setting from unattended searches over self-selected open problems.
Formal verification still leaves a specification boundary. Someone must check that the formal statement matches the intended natural-language theorem, including all quantifiers, domains, and side conditions. A valid Lean artifact for the wrong statement is a valid proof of the wrong target.
The useful hierarchy is:
- Natural-language audit checks mathematical meaning and scope.
- Blind reconstruction checks whether the argument stands without the author's context.
- Computation checks named finite claims and preserves small certificates.
- A proof assistant checks the formal derivation when formalization is practical.
- Human review checks significance, specification fidelity, and publication responsibility.
These layers reinforce one another. None should borrow a stronger label than the evidence actually provides.
An implementable run protocol
A lightweight system can apply the method without building a new AI4Math platform.
1. Define completion before launching agents
Write STATEMENT.md, including explicit exclusions such as special cases, finite checks, or reductions to unproved claims. Ask the human researcher to approve the target.
2. Create the state files
Initialize REGISTRY.md, FAILED.md, and PROVED.md. Put file schemas and evidence-label definitions in AGENTS.md or a reusable skill so every session applies the same contract.
3. Run exploration in waves
Start with diverse mechanisms. Redirect duplicate workers when several converge on the same terminal gap. Scale concurrency only when the registry and review capacity can absorb the output.
4. Require decisive artifacts
Every worker returns one compact artifact and updates the registry. Computations need a named question, source file, timeout, log, output, and a small certificate. Finite computation may refute a claim or discover a witness; it does not prove an unbounded theorem by itself.
5. Trigger the verification cadence
For every complete candidate, run the hostile audit and blind reconstruction with fresh contexts. Record the prompts, outputs, model family, verdict, and unresolved risks.
6. Promote compact knowledge
Write only the checked result, its dependencies, certificate, and verification record into PROVED.md. Keep raw drafts and transcripts outside trusted memory.
7. Report through a gate
Interrupt the researcher for a complete proof, certified counterexample, proved lemma that removes a named dependency, or exact obstruction that closes a route. New notation and vague optimism stay in the work log.
This is a domain-specific version of the broader Harness Engineering scaling problem. Time, parallelism, and interaction can scale only when state and evaluation scale with them.
What the reported numbers do and do not show
Xu reports that, over several days, his orchestrators used a few hundred subagents. He describes a typical wave as six agents advancing the frontier, followed by a fresh six checking returned work. He also reports trying ten open problems for at least ten hours per problem unless a problem was solved sooner, with three successes.
These are useful operational observations. They are not a controlled evaluation of the protocol.
The article does not publish the complete ten-problem set, full run logs, cost accounting, independent judgments for every success, or a comparison against single-agent and ordinary-chat baselines. “3/10” therefore describes one operator's experience. It cannot establish that the workflow raises the probability of solving open problems.
The defensible conclusion is narrower: long-running mathematical agents need explicit state, independent verification, and honest evidence labels. That conclusion follows from the architecture and its failure boundaries, not from the reported success rate.
Failure modes to watch
The verifier becomes another author
A reviewer that rewrites the proof may hide the original gap. Keep audit and repair separate. First record the blocking flaw; then let an author produce a new candidate.
“Fresh” means a new chat window
A fresh instance of the same model family can reduce context contamination, but it does not remove correlated training and reasoning failures. Label it accurately.
The knowledge base becomes a transcript archive
Saving everything lowers information density. Promote only claims, precise obstructions, small certificates, and decisions that future work can reuse.
Failed routes reopen through paraphrase
Require a material novelty statement before every retry. The burden is to name the new mechanism, evidence, witness, or scope.
Computation replaces proof search
Coding agents naturally write programs. Require each computation to answer a finite mathematical question and preserve a certificate that can be checked independently.
Labels become ceremonial
Enforce the promotion gate in tooling where possible. Danus, for example, separates planners, workers, and a cold-start verifier through role-specific permissions; only verifier-approved facts enter its fact graph. Prompt rules are useful, but permission boundaries make silent status inflation harder.
FAQ
Can AI agents produce valid mathematical proofs?
Yes, in both natural-language and formal settings, but validity depends on the verification path. A proof-shaped response is a candidate. Formal checking, independent reconstruction, outside-family review, and human review provide different kinds of evidence.
Do I need Lean or another proof assistant?
No. Natural-language research can use hostile audits, reconstruction, computational certificates, and human review. Lean adds a stronger derivation check when the theorem can be formalized, while introducing a separate need to verify that the formal statement matches the intended theorem.
Is asking the same model twice independent verification?
It provides a fresh-context check, not full independence. Different samples from one model family can share blind spots. Record them as same-family verification and seek another model family or a human for the independent-audit label.
How many agents should run in parallel?
Use the number your registry, compute budget, and verification capacity can absorb. More workers help only when they explore materially different mechanisms and their outputs can be reviewed. Xu's six-worker waves are an operating example, not a universal optimum.
What belongs in PROVED.md?
Only compact, reusable claims that passed the declared gate: exact statement, hypotheses, proof or certificate, dependencies, evidence label, and verification record. Raw transcripts and unresolved drafts remain outside trusted memory.
References
- Chao Xu, AI Agents for the Working Mathematician, 2026.
- Chao Xu, Coverify and Atomic Attempts, 2026.
- frenzymath, Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory, 2026.
- Kaito Baba et al., Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs, 2025.
- OpenAI, CDC Prompt.
- Google DeepMind, AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems, 2024.