The Math Harness

A mathematical model can write a proof. A math harness decides what problem the model is supposed to solve, what information it may use, how long the search can retain useful state, which claims deserve another attempt, and what must happen before a result is shown to a mathematician.

I use math harness here for a system whose input is a conjecture stated in natural language and whose success condition is a true, human-readable proof or disproof of that exact statement. This survey covers systems in which an LLM drives the search. Standalone reinforcement-learning and symbolic-search systems with no LLM in the search loop are outside its scope. Bounds, constructions, and precise accounts of a remaining gap may be useful intermediate research artifacts, but they do not count as success. The system may call a proof assistant, computer algebra system, numerical solver, or search program, but none is required. Lean-first systems whose main task is to turn a formal theorem into kernel-checked code are also outside the survey.

The model is only one component. The harness supplies the research loop around it: exact problem statements, context and literature, parallel or iterative proof search, durable memory, computation, adversarial review, and an honest stopping rule. This distinction matters because a larger pile of model calls does not automatically produce better mathematics. A useful harness must preserve the target, accumulate knowledge instead of transcripts, and make an incorrect proof harder to promote than to generate.

This page is a dated map of a fast-moving area, not a leaderboard. Reported solve counts below come from different problems, budgets, release policies, and review standards. They should be read as evidence about system designs, not compared as if they came from one controlled experiment.

Benchmark

A benchmark for a natural-language math harness has an awkward job. The task must be hard enough to require real mathematical work, recent or private enough to resist memorization, self-contained enough that failure does not merely measure missing context, and judged by something stronger than the presence of proof-shaped prose. Cost, abstention, tool access, literature access, and human steering must also be visible.

TCS-Bench

TCS-Bench is the clearest large benchmark currently aimed at research-style natural-language proof generation. Its 300 tasks are extracted from 190 papers published at STOC, FOCS, and SODA between 2020 and 2026. Each task contains up to 10,000 tokens of curated context, a target statement, and a withheld ground-truth proof. The construction recovers a paper’s dependency graph and creates harder variants by hiding intermediate lemmas, so the model may have to reconstruct part of the paper rather than fill one local gap. The task repository is public.

The benchmark uses an automated natural-language proof verifier calibrated against 100 expert-labelled proof attempts; the paper reports accuracy above 90% on that alignment task, although it does not document a separate verifier-prompt test split. In the 13 August 2026 revision, the verifier accepted 204 of 300 outputs from the strongest reported direct model. The paper also evaluates an internal harness called Colosseum, which explores several strategies, decomposes the target, revises a proof, and uses cross-model criticism to choose between two runs. Cross-model selection received 203 acceptances, compared with 162 and 140 for its two individual arms. These are grader verdicts, not established true successes. Colosseum is only sketched in the benchmark paper, so the result is neither a reproducible harness comparison nor enough to place it on a capability-cost frontier.

TCS-Bench has published reference proofs, scalable difficulty, and enough tasks for controlled comparisons. It does not remove the central difficulty of informal-proof evaluation: its grader is still a language model, and 90% agreement is not mathematical certainty. Papers from 2020 also predate current models, while newer additions offer a cleaner contamination test.

FirstProof

First Proof and its second batch test systems on questions supplied by active researchers before solutions are publicly available. The second batch contains ten problems across several fields, allows only public models and tools, gives systems a 24-hour run, and sends the resulting proofs through expert journal-style review. The small sample makes percentages unstable, but the protocol tests something a large extracted benchmark cannot: whether a system can produce a true proof or disproof of a question whose answer is not already in the literature it can retrieve.

FirstProof has become a common proving ground for Aletheia, RMA, and ProofCouncil. Their quoted results must remain attached to the exact batch and review language. Only an expert-verified complete proof or disproof counts as a success here; partial progress, no returned answer, and a result that still needs a substantive repair all count as failures.

MathArena

MathArena continuously publishes problems, model outputs, and costs for many mathematical tasks. Only its Proof-Based Competitions fit this survey: 50 public problems from USAMO 2025 and 2026, IMO 2025, IMC 2025, the 2025 Miklós Schweitzer competition, and Putnam 2025. The protocol varies: USAMO and IMO have four attempts per model and problem, IMC uses one attempt with MathArena’s expert graders, and Putnam and Miklós use official single submissions. All are scored with competition points, so a harness comparison should instead count each completely correct proof as one binary success and ignore partial credit.

The fixed track is too small and public to be the main benchmark, and its newest slice is already saturated. GPT-5.4 averages 95.24% of the available points on the six USAMO 2026 problems, while GPT-5.5 reaches 98.21%; MathArena flags the latter because the model was released after the competition. A future proof competition could support a useful pre-registered comparison if the base model and harness are run immediately under the same dollar limits. The historical leaderboard cannot establish a current harness advantage, and MathArena’s overall score mixes proof generation with final-answer, visual, and Lean tasks that do not measure this objective.

IMProofBench confirms that harder natural-language research problems exist—GPT-5.4 completely solved 49% of its July 2026 paper set—but its internal evaluation system currently exposes no public interface for arbitrary harness submissions. It could become useful through a blind runner: the organizers execute a versioned harness on hidden problems, broker and meter its model and tool calls, retain the problem and transcript, and return binary success counts with dollar cost. The solving process sees each conjecture while the developer does not; a development split may return per-problem feedback, while the final held-out split should reveal only aggregate results.

LemmaBench

LemmaBench continuously extracts lemmas from recent arXiv papers and rewrites them as self-contained problems. Its latest published slice uses 120 retained lemmas from papers posted in the last week of April 2026. The paper’s preferred whole-proof GPT-5.5 judge accepted 49 of 120 GPT-5.5 outputs at pass@1, or 40.8%; a stricter step-by-step GPT-5.5 judge accepted only 25, or 20.8%. The same 120 outputs received a 65.8% acceptance rate from a Gemini 3.1 judge, and the latest slice has no human validation. The published acceptance score is not saturated, but the judge spread is too large to treat any of these verdicts as a true-success count.

The benchmark is also moving quickly enough that a published score cannot certify suitability for a later model. GPT-5.6 Sol appeared after the latest LemmaBench experiments, and no public GPT-5.6 run exists. Before using LemmaBench to compare harnesses, run the actual base model once on the exact fresh slice and independently verify the outputs. If it already proves or disproves most tasks, generate a newer slice or pre-register a harder band from a separate calibration run; adding a harness to an already-saturated base-model benchmark measures overhead more than proof search.

The public repository contains the pipeline, but its data/ directory currently contains only a placeholder rather than the published benchmark snapshots. Appendix F of the paper gives one complete example. Anyone who wants to inspect a full set must currently run the extraction pipeline on a chosen arXiv week; the exact 120-problem April slice is not available there as a browsable or downloadable dataset.

The most useful development problems occupy a narrow gap: the chosen base model fails in one zero-shot direct attempt, while a harness built from that model produces a verified proof or disproof within a recorded dollar budget. Such cases provide development and regression tests for search, memory, and verification mechanisms; identifying which mechanism caused a recovery requires an ablation. A set selected after observing that separation is a development corpus, not an unbiased benchmark. The final capability–cost comparison must use fresh held-out problems drawn from the same difficulty band, with the direct model and harness given matched model and tool access at several fixed dollar budgets.

Harness

The general-purpose systems below all accept natural-language mathematics and return natural-language mathematical work. They disagree on the unit of memory, the shape of search, and the authority allowed to say that a proof is finished.

Evaluation

A harness has two measured outcomes on a frozen task set: capability, the number of exact conjectures truly proved or disproved, and cost, the total dollars spent by the evaluated system on all attempts, tools, and internal verification. The common blind final adjudication is evaluation overhead outside both arms and is reported separately. Correctness is binary: a false proof, a proof of an easier statement, and partial progress all count as failure.

Compare systems by their Pareto frontier across several budgets. A system is better when it solves at least as many tasks for no more money, with one inequality strict. No single weighted score is needed. Cost-of-pass is a useful derived statistic, but it can hide the difference between a cheap system that solves almost nothing and a more expensive system that reaches a substantially larger set of problems.

The decisive baseline spends the same dollars on independent attempts by the base model and applies the same verifier. Memory, decomposition, parallel workers, and hard gates matter only when they move the harness above and to the left of that baseline. Coverify has not yet run this comparison.

Adjacent training method: MetaMath

MetaMath is a public training recipe, dataset, and family of fine-tuned language models rather than a runtime harness. It uses GPT-3.5 to produce alternative solutions, rephrased questions, and backward questions from GSM8K and MATH, filters generations by their final answers, and fine-tunes base models on the resulting 395,000-example MetaMathQA dataset. In the reported evaluation, each problem receives one zero-shot generation; the released method has no controller, persistent search state, tool loop, critic, or proof verifier. “Self-Verification” is the name of one backward-question augmentation method, not verification of a generated proof. The data, checkpoints, generation code, training code, and evaluators are public.

Its transferable idea is distillation. Repeatedly useful proof transformations, failure repairs, and counterexample patterns could become training examples so later runs need fewer prompt tokens and search rounds. That changes the base model rather than the harness, so it needs a separate comparison that charges or amortizes data generation and fine-tuning. MetaMath reports final-answer accuracy on school and competition problems and no dollar cost; it cannot be placed on the capability–cost frontier for research proofs.

Aletheia

Aletheia, from Google DeepMind, runs a generator, verifier, and reviser around Gemini Deep Think until the verifier accepts a solution or the run reaches a limit. It is explicitly end-to-end natural language. The system itself is not released, but prompts and research outputs are public.

Its 700-problem sweep over questions then marked open in the Erdős Problems database is instructive. Aletheia returned 212 candidates; human review found 63 technically correct answers, but only 13 that addressed the intended mathematical question through a relevant argument or literature result. The paper groups four autonomous solutions and partial solutions to open questions rather than reporting a binary count of exact resolutions, so that number cannot enter the capability-cost comparison. The large drop from plausible candidate to meaningful answer shows why target interpretation and exact source matching belong inside the harness, not after it.

Rethlas

Rethlas is an open-source natural-language reasoning agent with theorem retrieval through Matlas and an iterative worker–verifier loop. It explores literature, constructs toy examples and counterexamples, plans a proof, writes an informal argument, and sends it to a separate natural-language verifier. Its recursive-proving skill can dispatch several subagents across decomposition plans. The same project pairs Rethlas with Archon for optional Lean formalization, but Rethlas itself is useful without Lean and its code is public.

Rethlas combines retrieval and verification with a coding agent. Danus retains that worker–verifier core while adding persistent concurrent workers, global orchestration, and fact-graph memory.

Danus

Danus organizes parallel Rethlas workers around a content-addressed fact graph. A main agent chooses directions; workers attack claims, counterexamples, or toy cases; a stateless verifier is the only component allowed to admit a claim into the graph. Each accepted fact carries its proof and dependencies. The graph, rather than any agent transcript, becomes the shared mathematical state from which a final paper is assembled. Danus is open source.

The paper presents six case studies in algebraic geometry, singularity theory, and combinatorics. In its strongest matched case, three Rethlas runs failed while Danus, using the same worker and verifier models, produced a candidate that human review found locally incomplete but repairable. Under the binary criterion here, that run is a failure. It may motivate a controlled test of parallel search and fact-level memory, but it does not establish a capability gain.

ProofCouncil

ProofCouncil uses an author–critic loop. The author edits a proof, research notes, and references; a stateful critic follows revisions; every few rounds a fresh critic resets the review context. The author may call a council of other model families or a compute agent equipped with computer algebra systems. The proof returns only after the author, stateful critic, and fresh critic agree. Both the harness and its DAG-based agent library are public.

On the second FirstProof batch, expert referees judged six of ten submissions correct up to at most minor revisions. On 30 researcher-supplied problems, 21 received feedback: five were judged complete, two possibly complete, eight useful partial progress, four had no apparent errors but little substantive progress, and two answered easier interpretations. The official FirstProof run cost about $350 per analyzed problem, while a roughly $12 one-query baseline received the corresponding positive verdict on four of nine analyzed problems rather than six. These categories must be converted to the same binary truth criterion before either system can enter the capability-cost comparison.

QED

QED separates literature survey, proof planning, proof generation, structural verification, detailed verification, selection, and the retry decision. Its harder mode represents the proof plan as a dependency DAG. A regulator distinguishes an execution error from a bad plan and a bad overall approach, triggering proof revision, plan revision, or a complete rewrite. Different coding-agent backends can generate and verify in parallel. The implementation and proof artifacts are public.

The paper evaluates 18 research projects and reports five original works accepted by the corresponding domain experts. Two of those projects have separate public manuscripts that explicitly attribute their proofs to QED: lower bounds for advection–diffusion equations and the return probability of a lamplighter walk on a regular tree. Both papers include a QED developer as an author, so they demonstrate output rather than independent third-party adoption. In the subset using one reported verifier configuration, all 17 verifier-accepted candidates were later accepted by experts. This is useful positive evidence, but not an estimate of false-acceptance probability: rejected candidates were not all independently labelled, and the projects were not a frozen random test set.

RMA

Research Math Agents (RMA) combines problem analysis, controlled literature search, a compact knowledge bank, proof-generation agents, verifier agents, and disk-based structured memory. RMA reports eight correct solutions on the first FirstProof set under its own blind expert evaluation, compared with several direct and agentic baselines. The paper also reports ablations over memory, number of proposers and verifiers, and number of rounds.

RMA is evidence for a modular research workflow, but not yet a reusable public harness: the May 2026 paper says that solutions and implementation will be released upon acceptance. Its results should remain labelled as author-reported until the system and complete run artifacts can be inspected.

AI co-mathematician

The AI co-mathematician is broader than a proof-returning loop. A project coordinator negotiates goals with a human, launches parallel workstreams, delegates to literature, reasoning, coding, and review agents, and writes incremental and final reports into a shared workspace. Human steering remains available while work continues. The current prototype’s proofs are informal; formal provers are described as optional future components.

Its case studies emphasize collaboration rather than autonomous pass rates: a mathematician can inspect a failed proof, salvage its strategy, supply the missing idea, and ask the system to rebuild and review the argument. This workflow may eventually produce a true proof, but preserved state and partial assistance do not count as successes in this survey.

qmd-prover

qmd-prover turns a natural-language theorem, rough idea, or existing proof development into a dependency-explicit natural-language proof project. Claude Code or Codex writes definitions, statements, and proofs as plain-text Quarto Markdown blocks with stable identifiers and explicit citations. The TypeScript tool locks the main statement, checks the document and dependency graph mechanically, optionally sends each proof with only its cited premises to a fresh AI reviewer, composes the local verdicts through the dependency graph, and can render the result as a navigable Quarto book.

The host coding assistant still supplies the proof search, and the optional reviewer remains a language model rather than a formal kernel. Model separation is configured rather than enforced, assumed facts may be permitted, and the default review policy allows advisory gaps that strict mode would reject. The repository reports a 34-fact Gödel-completeness demonstration, but publishes no benchmark or auditable verifier transcript. I found no public paper that cites qmd-prover or attributes a research result to it as of 14 August 2026.

Coverify

Coverify is my open-source attempt to make the verification and durable-state contract explicit. One campaign freezes one exact statement, sends independent workers down different routes, records dead routes and precise gaps, and keeps every candidate, audit, reconstruction, and promotion as plain files. A candidate passes through a hostile audit, a check that the reconstruction brief does not leak the proof, a blind reconstruction from that brief, and a comparison between the independent reconstruction and the candidate. Reuse of a verifier record is keyed to the candidate, frozen statement, promoted-premises view, and the stage-specific dependency bundle, then checked against the saved artifact hash.

Coverify is not a proof assistant. “Promoted” means that specified language-model reviews passed on exact saved bytes; it does not mean the theorem is machine-checked or true. The current implementation is a working research harness with live campaign experience. It has not yet produced a capability-cost curve against the raw proof-search workflow, so cost-efficiency remains a design target rather than a result.

Public attribution ledger

Rethlas has the largest traceable public-paper footprint I found. This is a bibliography of disclosed use, not an evaluation metric: publication count is neither capability nor cost, and no manuscript counts as a benchmark success merely by appearing here. For this snapshot I counted a distinct public result manuscript only when its own text names the harness and credits it with generating, discovering, completing, materially structuring, or verifying mathematical content. I excluded each harness’s system paper, benchmark reports, private or repository-only artifacts, ordinary related-work citations, and statements that one harness merely descends from another.

One manuscript credits both Rethlas and Danus, so the first two rows contain 31 distinct manuscripts rather than 32. The counts measure disclosed use, not mathematical correctness, autonomy, importance, or independent adoption. They are lower bounds dated 14 August 2026: papers can appear faster than indexing, and authors vary in how much AI assistance they disclose.

Rethlas attribution ledger

The 21 manuscripts behind the leading count are:

1. A Counterexample to Problem 19 on Integer-valued Polynomial Rings
2. An Integrally Closed Reduced Ring with McCoy Localizations That Is Neither McCoy nor Locally a Domain
3. On a question of Kollár and Kovács
4. An example of a very non-movable effective divisor
5. Optimal bend-and-break for foliations
6. On a question of Mauri and Moraga
7. A question on klt type varieties of Han and Jiang
8. Shokurov’s global index conjecture for threefold foliations
9. Boundedness of total Cartier indices for rational singularities in families
10. Degenerate constants in degree inequalities for Sobolev circle maps
11. On some open problems in commutative algebra resolved by Rethlas
12. Lift-independence problem in the p-adic Simpson correspondence for curves
13. A counterexample to the near-quadratic Elekes–Rónyai expander conjecture over \mathbb R
14. On Injectivity of Phase Retrieval
15. Criteria of isolated weighted homogeneous hypersurface singularities using Logarithmic vector fields
16. Involution-equivariant topological recursion and mirror symmetry for the affine binary dihedral Calabi–Yau threefold
17. Kazhdan–Lusztig polynomials of matroids need not be unimodal
18. Analytic Bertini theorem II — The local case
19. A counterexample to the zero-mass conjecture
20. Factorial asymptotics of the Matryoshka numbers
21. On a conjecture of Esser, Totaro, and Wang

The Rethlas results repository preserves raw outputs for several of these projects. The individual manuscripts remain the attribution authority: some describe complete autonomous proofs, others a discovered construction, repaired proof, verified computation, or substantial proof architecture later checked and rewritten by humans. The latter categories document adoption but are failures if the harness’s assigned conjecture was not truly proved or disproved.

What the systems are converging on

Most general harnesses use the same loop. A controller sends the fixed conjecture to one or more proof workers, sends candidates to separate critics, and uses the criticism to accept, repair, decompose, or restart the search. Aletheia uses generator–verifier–reviser cycles; ProofCouncil combines author revision with stateful and fresh critic contexts; Rethlas uses generation–verification rounds; RMA uses proposer–verifier rounds; QED routes failures at the proof, plan, or approach level; Danus admits verified claims into a fact graph.

A second recurring choice is structured mathematical state: a proof-plan DAG, fact graph, knowledge bank, or dependency-bound artifact set. Later calls can reuse accepted work without paying to reconstruct an entire transcript. Retrieval, code, and exact checkers are tools behind this loop, not its common architecture.

This convergence does not establish an advantage. Every worker, critic, retry, and memory operation costs money, and model agreement does not make a proof true. On a frozen task set, the architecture earns its complexity only if, under the same correctness adjudication and matched total dollar budgets, it returns more true proofs or disproofs than direct attempts, or the same number for fewer dollars. Partial progress, consensus, publication, and well-organized state are not additional outcomes.

Experiments worth running

Every experiment below uses frozen held-out tasks, the same available model and tool pool, the same sources and user-set total dollar budgets, and one blind final adjudication procedure; only the named intervention changes. Compare each mechanism with an otherwise identical arm without it and with independent direct attempts, spending any saved dollars on additional calls.

• Target and relevance lock. Freeze the original quantifiers, admissible assumptions, and exact proof-or-disproof certificate before search; reject candidates only when they change the statement or cite a result whose hypotheses and conclusion do not settle it. Compare this gate with an otherwise identical arm that sees only the original problem. Novelty is not required: a correctly matched existing theorem still proves the conjecture.
• Failure-level routing. Ask a critic whether a failure is local to a derivation, invalidates the proof plan, or defeats the whole approach, then repair only that layer; compare this with a fixed “revise the proof” loop.
• Typed fact-graph memory. Store each claim with its exact statement, proof, dependencies, and status, and give a worker only the dependency closure it needs. Numerical hints, unchecked lemmas, finite certificates, and human-checked theorems retain different types through every summary.
• Specialized proof and disproof routes. Within each user-set budget, allocate independent workers to constructions, counterexamples, toy cases, limiting cases, reductions, and literature; compare this allocation with same-dollar generic “prove or disprove” calls. Route specialization changes where the stated budget is spent, not how long proof search is allowed to continue.
• Persistent and fresh criticism. Let one critic track whether earlier defects were repaired while another sees only the frozen statement and current proof. Send disagreements to a third fresh critic, and compare the pair with stateful-only, fresh-only, and same-dollar direct attempts.
• Blind reconstruction. Turn a candidate into a dependency brief that states premises and obligations without copying its prose, ask a fresh solver to reconstruct the proof, and compare the two arguments at their load-bearing steps.
• Smallest-counterexample feedback. When an exact or one-sided checker exists, return the smallest violated instance, uncovered region, or failed obligation rather than a scalar score; require the next candidate to explain why its repair generalizes.
• Executable derivation trees. Couple each proposed symbolic transformation to code that tests adversarial parameter values, prune falsified branches, and require an independent natural-language proof for the surviving derivation.
• Witness evolution followed by proof. For finite construction problems, evolve diverse generator programs under an exact checker, then give the best witness to a separate worker that must prove why it settles the assigned statement. Compare the archive with best-of-N witness programs.
• Verifier extraction. When several natural-language attempts fail at the same checkable bottleneck, turn that bottleneck into a project-owned checker and compare localized feedback with binary accept/reject feedback.
• Evidence-based allocation. Within each fixed user-set dollar budget, use predeclared checkpoints to shift more of the remaining money toward routes that have produced a verified lemma, explicit obstruction, exact witness, or checker improvement; compare this policy with equal funding per route. These artifacts are routing signals, not additional outcomes, and the policy creates no default budget, timeout, or universal per-route cap.

Measurement and efficiency

The reported frontier still has two coordinates: exact tasks passed and total dollars. Token counts and elapsed time diagnose why a system moved on that frontier. They are not additional mathematical outcomes, and raw tokens are not money: models price fresh input, cached input, cache writes, and output differently.

Record every paid leaf

Each model or tool request should be written once, at the paid leaf that incurred the charge, with complete parent edges from campaign to run, wake, dispatch, verification stage, and provider request. Usage fields store leaf deltas; rollups and cumulative snapshots are marked and excluded from sums. A useful request record contains:

• requested and served model, provider, model revision, reasoning effort, experimental arm, replicate, and seed;
• actual billed dollars or the price schedule in force, with provider lanes kept separate;
• fresh-input, cache-read, cache-write, total-output, and reasoning-output tokens, plus the provider’s convention for whether cached input is included in total input;
• attempt count, since a retry can rebill the whole context without adding another visible turn; derive the provider-request count from the transcript when one exists, and otherwise record it once at the paid leaf;
• start, admission, first-token, and completion times, together with queue, rate-limit, backoff, tool, and retry spans;
• a content hash and token count for every prompt component, including the statement, contract, durable state, retrieved routes, transcript tail, wake delta, and tool output;
• cache namespace, reusable-prefix hash, hit or miss, expiration if known, and the exact input hashes governing any reused verifier result;
• links to claim-level premise records and a run-level terminal record whose reason is verified resolution, exhausted user-set dollar budget, user stop, or external failure.

Missing usage remains marked unmetered rather than becoming zero. Reasoning tokens are a subset of output on providers that report them that way; adding both double-counts. A subscription call has no honest per-call cash price, so controlled dollar comparisons should use metered APIs or predeclare an allocation rule and label list-price conversions as counterfactual.

Token and dollar savings to test

• Candidate-readiness gate. Run expensive verification only after a candidate states the exact target, dependencies, and complete proof skeleton; audit a sample of rejected candidates for false negatives. One Coverify campaign spent 30.7 million billable tokens and produced no promotions before candidate-scope discipline; this is motivating evidence, not a controlled saving estimate.
• Dependency-scoped packets. Send each role the frozen statement and only the facts it may use, not the campaign transcript or whole evidence tree.
• Indexed durable memory. Retrieve ranked obstruction snippets and a paged route inventory instead of replaying the full failed-route ledger. In one campaign, repeatedly presenting a 31 KB ledger accumulated about 40.4 million tokens presented in the reasoner lane.
• Stable prefixes and delta wakes. Keep the contract, statement, and accepted state byte-identical at the front of prompts; append only new evidence so provider prompt caches can be reused.
• Artifact-first tool output. Save full logs and computations once, then send bounded diagnostics plus content hashes and paths rather than reinserting raw output on every turn.
• Content-bound reuse. Content-address retrieval and computation caches. Reuse a saved verifier response only when every input hash and saved output byte matches, the earlier verification sequence stopped before completion, and the response did not influence a repair. Never reuse a candidate–reconstruction comparison or a PASS from a completed verification sequence.
• Route deduplication. Match a proposed mechanism against active and failed routes before dispatch, then measure both avoided duplicate calls and successful ideas incorrectly suppressed.
• Model and effort routing. Use cheaper models for mechanical coordination, retrieval, and preliminary checks, escalating disagreements and proof candidates to stronger models; compare the entire capability–cost curve, not token savings alone.
• Cheap checks first. Put deterministic checks of statement identity, dependency integrity, citation resolution, syntax, exact algebra, and finite-witness validity before expensive language-model audits without weakening the final verification policy.
• Finite role outputs. Request the candidate, dependencies, obstruction, and evidence without an exploration diary. Measure later repair spend as well, since a short first answer that causes more retries is not a saving.

Elapsed-time savings to test

• Event-driven scheduling. Wake the coordinator when evidence arrives instead of polling, and coalesce several completed reports when the delay is cheaper than replaying the prompt prefix.
• Parallelism sweep. At the same dollar budgets, test several user-set worker counts and measure the critical path, duplicate routes, and coordinator overhead. This finds a workload-specific knee rather than a universal agent limit.
• Immediate cancellation after verified resolution. Cancel remaining work only after the terminal proof passes independent verification; record cancellation latency, dollars spent after that gate, and provider work that continued after cancellation.
• Asynchronous exact checks. Run independent retrieval, numerical tests, finite checkers, and critic calls concurrently when none consumes another’s output; preserve serial dependencies where one result changes the next prompt.
• Checkpoint and resume. Resume from content-addressed durable state after interruption or compaction instead of reconstructing a transcript. Charge the compaction call and every mandatory state reread.

Saving time by parallelism can spend more money; saving tokens can increase output or repair cost. No wall-clock timeout should truncate proof work. The time report should separate end-to-end duration, critical path, queue delay, tool time, and time to the first independently verified result rather than summing overlapping calls.

Fair comparison

Preregister the held-out task set, user-set dollar budgets, replicate count, and stopping rule, then run paired trials at every budget. Freeze model snapshots, tools, literature access, and the final judge, and freeze every variable other than the intervention; when concurrency is the intervention, keep provider quotas and the model pool fixed. Isolate caches between arms and randomize arm order. The autonomous track permits no human steering. Any human-assisted track stays separate, predeclares how human time is converted to dollars, and includes that cost. Every internal controller, critic, tool, and verifier belongs inside the arm’s cost. One blind external adjudication procedure applies to both arms outside their budgets.

Cold-cache and steady-state trials should remain separate. Warm each arm independently and amortize warm-up over a predeclared number of tasks. Report the capability–dollar pair at each budget, failed-run dollars, paired uncertainty by task, provider splits, cache dollars, and token/time diagnostics. Development tasks selected because zero-shot fails and the harness passes are useful for choosing mechanisms once; the final comparison must use untouched problems from the same difficulty band.

Problem Specific Harness

A problem-specific harness changes the interface between creative search and correctness. Instead of asking a language model to judge an entire unfamiliar proof, the designer identifies a restricted object—a polynomial inequality, interval certificate, geometric rule, finite witness, or candidate construction—that software can test exactly or conservatively. The model searches over meaningful mathematical objects; the domain-specific verifier supplies dense, local feedback.

This approach gives up generality. Its verifier can expose why a candidate failed and turn the next model call toward a smaller defect. That mechanism counts as useful only when a controlled comparison shows more true proofs or disproofs for the same dollars.

Grothendieck constant

Long-Horizon AI Research for Grothendieck Constant describes a system built around one analytic optimization problem; the complete mathematics appears in a companion paper. A natural-language reasoning model chooses directions and develops arguments. A coding agent runs experiments and certifies one-dimensional inequalities with Arb interval arithmetic. A human-editable bulletin steers the live search, while session reports preserve proofs, code, failures, and explanations for later sessions.

The run lasted from 16 June to 24 July 2026: roughly 240 research sessions, 2,091 reasoning-model calls, 152 million tokens, an estimated $5,400 in API cost, and about 40 dated human directives. The system discovered and first proved the lower bound K_G \ge 6\pi/11; the authors then independently checked and rewrote the proof. The upper-bound construction in the companion result came from an earlier conversation with a reasoning model and predates the reported long-horizon harness. Several stronger bounds produced later remain labelled “system-tested” because their certificates have not yet been checked by the authors.

The most valuable failure is documented. An exploratory numerical score lost its caveat during repeated state compression and was treated as a record for 25 days before a later test withdrew it. The full archive still contained the warning; the compact research state used for decisions did not. Long-term memory is therefore not solved by saving everything. The harness must preserve the few facts that govern whether later conclusions are valid.

Gilbert–Pollak and the Steiner ratio

Towards Solving the Gilbert–Pollak Conjecture via Large Language Models narrows proof search much further. The model does not attempt the conjecture end to end. It generates rule-constrained geometric lemmas as executable structured code. Those lemmas instantiate verification functions whose shape reduces a continuous inequality over a region to checks at finitely many vertices, with symbolic algebra and recursive subdivision supplying the certificate. The prompts, code, and certificate are public.

The search–verify–reflect loop reports a certified Steiner-ratio lower bound of 0.8559, improving the prior 0.824 bound while remaining below the conjectured \sqrt{3}/2. When a candidate set of lemmas fails, the verifier returns a localized region in which coverage is missing; that structured failure becomes the next prompt. The certificate is a true theorem about the lower bound, but the run is not a success if the assigned target is the Gilbert–Pollak conjecture.

The system is not fully autonomous. The paper states that every model-proposed lemma was manually checked before being installed as a verification function, and its cylindrical-algebraic-decomposition verifier becomes expensive as dimension and degree grow. Those limitations define the bargain: human and symbolic effort build a narrow certified search space, and the language model explores it at a scale that manual lemma design could not.

Cosmic-string radiation integral

Solving an Open Problem in Theoretical Physics using AI-Assisted Discovery couples Gemini Deep Think to a PUCT tree search over derivations of a singular integral governing gravitational radiation from cosmic strings. Each node contains an intermediate LaTeX expression and executable Python code. A high-precision numerical evaluator scores the expression on random parameter values and feeds errors or tracebacks back to the model. The search explored about 600 nodes and pruned more than 80% for algebraic errors or numerical divergence before finding six analytic approaches, including an exact Gegenbauer expansion.

The numerical evaluator is a search instrument, not a proof checker. It can reject a false identity at a sampled point but cannot certify a universal identity. The final result is also a human–AI handoff rather than a fully autonomous run: a researcher manually started a second session with a stronger model, which corrected an error in the first spectral recurrence and simplified an exact infinite series to a finite analytic expression. The paper supplies the derivations, so the integral has an exact human-checkable solution. Under an autonomous protocol, the initial run is a failure; under a human-assisted protocol, the second model run and the researcher’s intervention must be priced and included in total cost.

Evolutionary search for exact witnesses

FunSearch, AlphaEvolve, and the open-source OpenEvolve share a useful problem-specific pattern. An LLM edits a program that generates mathematical objects, an executable evaluator checks validity and assigns task-specific fitness scores, sometimes giving invalid prospects graded scores based on their violation counts, and an evolutionary archive selects which programs return to the model. The harness is generic, but every application depends on a local representation and evaluator. FunSearch’s cap-set construction and AlphaEvolve’s rank-48 algorithm for multiplying two complex 4\times4 matrices are exact finite witnesses for improved existence bounds; neither establishes an optimum.

A 67-problem AlphaEvolve study shows how this can return to natural-language proof. For a three-dimensional finite-field Kakeya construction, Gemini Deep Think derived a natural-language proof and exact size formula, and AlphaProof formalized the proof. Deep Think also produced harder four- and five-dimensional proofs of asymptotic size estimates, which the authors checked by hand. The results improve construction bounds rather than resolve the finite-field Kakeya problem.

The same pattern has produced proof-relevant results once the finite witness is connected to a mathematical argument. AlphaEvolve-generated gadgets support new NP-hardness ratios for MAX-4-CUT, MAX-3-CUT, and metric TSP; exact verification of the final gadgets is only one component of the accompanying proofs. In Ramsey-number search, exact clique and independence checks certify nine improved lower bounds. Those are successes when the assigned statement is the stated lower bound, not when the target is the exact Ramsey number.

The cleanest target closure in this family comes from OpenEvolve search for Zarankiewicz matrices. The LLM mutates programs that output binary matrices; the evaluator counts ones and forbidden all-one 3\times3 submatrices, and the final reported witnesses contain none. Three generated constructions meet previously proved upper bounds, determining Z(11,21,3,3)=116, Z(11,22,3,3)=121, and Z(12,22,3,3)=132. The paper reports a search cost below US$30 per parameter combination. The other 41 new constructions improve lower bounds but do not determine the corresponding Zarankiewicz numbers.

k-server potential search

k-server-bench asks LLM agents to write Python potential functions for the k-server conjecture and evaluates them against millions of graph-structured linear inequalities. Best-of-N, ShinkaEvolve, LoongFlow, and a human-guided Codex run receive violation counts and related diagnostic metrics. On the open k=4 circle case, the best Codex candidate reduced the count from 17 violations for the human baseline to 3 among roughly seven million checked inequalities.

This is a strong development environment and currently a zero under the capability metric. A violation rigorously refutes a candidate, but zero violations on the finite instances would still not prove the unbounded conjecture. The reported search found no zero-violation k-competitive candidate for the open case. Its resolved k=3 instances can test whether an LLM loop learns from exact local feedback. The open k=4 case remains a development environment; it becomes a capability success only if the system turns that feedback into a proof of the unbounded conjecture.

The design opportunity

The boundary between general and problem-specific harnesses should stay movable. Begin with natural-language search and durable adversarial review. When repeated attempts hit the same checkable bottleneck, extract that bottleneck into a project-owned verifier and feed its smallest counterexample or uncovered region back to the search. Do not put domain logic into the general harness, and do not pretend that a finite checker proves an unbounded theorem unless the mathematical reduction to that checker has itself been proved.

The long-term shape is a thin general harness around many local instruments. Natural language remains the interface for stating the question, choosing a direction, explaining a proof, and involving a mathematician. Exact tools enter where the problem supplies an exact interface. Lean can be one such tool. It does not have to be the center of the system.