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. 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 outside this 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

IMProofBench is a stronger current fit. Its July 2026 paper evaluates 77 private, peer-reviewed research-level problems written by professional mathematicians, including 23 open questions; the live leaderboard currently lists 73 active problems. Models work in an agentic environment with web search, Python, SageMath, and shell tools, and the problem author grades the anonymous answer. The published protocol permits up to 300,000 tokens per main problem; GPT-5.4 produced complete solutions on 49% of the paper’s task set, while no GPT-5.5 or GPT-5.6 proof score is published.

For a harness comparison, only the author’s “full solution” verdict should count; the benchmark’s minor- and major-progress grades are not successes. Access requires coordination with the organizers, and the base model and harness would need separate runs at fixed dollar budgets. Subject to that access, IMProofBench is less saturated and closer to the intended research setting than the public competition sets.

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 benchmark I would most trust combines these ideas: recent or private targets; a frozen, self-contained context; natural-language proof output; matched model and tool access; several fixed dollar budgets; explicit abstentions; and independent verification of whether each exact conjecture was truly proved or disproved.

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 on all attempts, tools, and verification. 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.

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 novelty checking 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

Across these projects, the useful common core is smaller than their diagrams suggest:

1. Freeze the target. Keep the exact quantifiers, hypotheses, conventions, and acceptance criterion visible. A correct proof of an easier statement is a failure.
2. Separate search from judgment. Let workers explore freely, but do not let a proof author certify its own output. Reset reviewer context or use a fresh model when path dependence matters.
3. Store mathematical state, not chat history. Facts, dependencies, failed mechanisms, counterexamples, and open obligations survive. Most transcripts do not deserve to.
4. Make failure productive. A dead route needs an obstruction and a condition under which retrying it would be new. Otherwise parallelism buys duplicate attempts.
5. Bind verdicts to artifacts. If the proof, statement, dependency list, or supplied context changes, the old review no longer applies.
6. Distinguish evidence levels. Model-approved, cross-model-approved, human-reviewed, computationally certified, and formally checked are not synonyms.
7. Measure the harness against the direct model. Verification cost belongs inside the budget. More calls, more agents, longer reports, and better-organized partial progress have value here only if they produce more true proofs or disproofs for the same dollars.

Natural-language verification remains the weak joint. A fresh critic can catch a gap and still share the prover’s blind spot. A human-readable proof has no kernel that returns an error at the first invalid inference. Independence, adversarial prompts, cross-model review, and provenance are filters, not truth guarantees; a claimed success still needs independent mathematical verification. When a problem admits a small exact checker, a more specialized design can do better.

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.

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.