17. Evaluation

math2 makes claims at three levels. It makes claims about mathematics (the status of a node). It makes claims about its own machinery (the battery catches misformalizations; search finds the right node). It also makes claims about its agents (this prompt version proves more for less). Each claim needs a measurement, or it is a slogan. This document says what math2 measures, how it measures it, and what each measurement gates.

The code and data are in tamnd/math2-agent/bench/. The results go to tamnd/math2/reports/eval/<release>/, and the notes of each release give a summary of them.

17.1 Principles

1. The kernel is the only grader that needs no evaluation. math2 grades all other graders, which includes LLM judges, back-translation, the critic, search and extraction. Every grader has a labelled set, a measured error rate, and a version.
2. Gate on regressions, report the levels. Each suite has a gate: on the suite, a new version must be no worse than the old one, within noise. math2 publishes the absolute numbers, but they do not gate. A gate on absolute targets invites quiet changes to the target.
3. Measure cost with quality. Report every result with its cost: tokens, dollars, wall-clock time and Lean CPU time. In 2026, the same model could score 7/10 for $36 or 9/10 for $1,888. The difference came from the harness around the model (document 01). You cannot compare a score that has no cost.
4. Report failures and the selection. The report of a suite says how many items passed and which items failed. It also says how the items were chosen. This follows the AGMAI guideline that labs document failed attempts and how they selected problems (document 01). math2 applies this guideline to itself.
5. Contamination is the default assumption. Any public problem set may be in the training data of a model. Each suite has public, held-out and fresh items (17.6). The headline numbers come from the held-out and fresh items.

17.2 What is measured

17.3 Suites

17.3.1 The fidelity battery

The battery (10.4) is a classifier. Its verdict is faithful, or misformalized with a class. Its evaluation set contains labelled pairs, and each pair is an informal statement and a formal statement:

• Seed. Known misformalizations from the published audits. These include the defective items of ProofNet, the certified issues of the ICML 2026 benchmark audit, the fixed statements of PutnamBench, and the corrected statements of the formal-conjectures repository. Each item has its taxonomy class (10.5).
• Synthetic. Faithful statements from F3 nodes, mutated by one taxonomy class at a time: drop a hypothesis, swap a quantifier, change ℕ to ℤ, add a junk value. A person checks each mutation before it enters the set, because some mutations are also faithful by chance.
• Live. Every not-faithful review (10.6) enters the set, with its class.

Measured: recall per taxonomy class, and the false-alarm rate on faithful items. The report is a confusion matrix over classes. A battery change must not decrease recall on any class by more than the noise band of that class. The band is published with the matrix.

The suite in m2. bench/fidelity has the synthetic part, in the Lean core library, and it reads the live part from the reviews of a math2 tree. The seed part needs the published audits, and it comes later. The noise band is zero items, because the tactics of the battery have limits in heartbeats and give the same result on each run. Thus the test fails when one class catches one item less. The report is attached to each release of tamnd/math2-agent.

17.3.2 Extraction

The suite has five hundred papers across MSC codes, decades and source types (LaTeX, HTML only, OCR). Each paper is labelled by hand with its results, their kinds, their in-paper dependencies, and a reference unfolding of each result. Measured: result recall and precision; kind accuracy; dependency edge F1; unfolding fidelity. People grade unfolding fidelity on a sample, and the back-translation judge of the battery grades it on all items. The report gives errors by source type, so a regression in the OCR path cannot hide behind the LaTeX path.

17.3.3 Alignment

The suite has confirmed and rejected alignments from curation (09, 05.3). Measured: precision at the auto-propose threshold, and recall of known same_as pairs. Precision is more important here, because a wrong same_as edge contaminates everything downstream. The threshold is set so that precision on the held-out set is at least 0.98.

17.3.4 Agent roles

Each role in 12.1 has a suite of tasks with an objective outcome:

The suite of formalize and prove is in bench/agents. Its first items are public, use only the Lean core library, and have a reference solution. Without a model service, a scripted model writes the reference and some wrong attempts, thus the suite checks the goal predicates of the roles on real Lean. A live run with the Claude models gives the items solved and the dollars of each item.

The suites of explain and curate are in bench/agents/explain and bench/agents/curate. They need no Lean. The scripted model writes the reference and wrong attempts, and the scripted grounding check or judge gives the labels or the verdicts of the items. Thus the suites check the mechanical parts of the goals: the citations and the levels of explain, and the locator, the kind and the copy check of curate. A live run also grades the grounding check and the judge alone against the labels and the verdicts of the items, because the goals depend on them.

The suite of review-assist is in bench/agents/reviewassist, and it needs no Lean. Its items are bindings with known verdicts, as the table says. The scripted model writes the packet with the reference concern of each item, and some wrong packets that the goal or the tool must refuse. A live run gives the recall of the critic on the not-faithful items, the concerns on the faithful items, and the length of the packets.

The suite of align is in bench/agents/align, and it needs no Lean. Its items are crosswalk edges and Mathlib bindings with a known reference. The scripted model makes the reference change and some wrong changes, and the scripted judge gives the verdicts of the items. Thus the suite checks the mechanical parts of the goal: the edges that a source allows, the decisions of the register and the type hash of a Mathlib binding. A live run gives the precision and the recall of the edges, as 17.3.3 says, and it grades the judge alone against the verdicts of the items.

The suite of bump is in bench/agents/bump, and it needs no Lean. Each item is a replay of a bump, with the pinned Mathlib after the bump in the file of the items. The public items are made up, and the held-out items are replays of past Mathlib bumps from git history, as the table says. The scripted model makes the rebinds of the reference and some wrong rebinds that the goal or the tool must refuse, and the suite checks that bump.AutoMerge gives the value of each item. The goal refuses a rebind to another type hash unless the job has the constraint type_change. A live run gives the share of the breakages that the role repaired, the share of the repairs that can merge with no review, and the repairs that change a type hash with no flag, which must be zero.

The suite of explore is in bench/agents/explore, and it needs no Lean. Its items are planted problems of the second form of the table: plausible statements that are false, each with a small counterexample, the program that finds it and the output of the program. Without flags, a fake sandbox gives the output of each program, and the scripted model files the reference counterexample through a computation that verifies, after a lookup of the claim. The goal or the tool must refuse the wrong attempts: no output, a claim that the output is new, a conjecture that no computation checks, a counterexample with no computation, a wrong output hash and a change of the target. A live run runs the computations in docker and gives the three metrics of the table. Each target of the public items is false, thus a person reads each conjecture of a live run, and a conjecture that the person finds false is a false conjecture that the falsify step did not catch. The items with withheld known conjectures are not in the suite yet.

Every role suite has three splits. Public items can be anywhere. Held-out items are never published. They are in a private repository that the tools of the agents cannot reach. Fresh items were made after the training cutoff of the model. Fresh items come from new Mathlib declarations, new formal-conjectures statements, new arXiv results with formal statements, and items that the maintainers write. Each model version is compared on all three splits. If public scores are much higher than fresh scores, the report gives the difference as a contamination signal.

17.3.5 Explanations

Explanations (12.6) get grades on three axes. Correctness: every mathematical claim in the explanation is grounded in a cited node, or it is marked. Level: an L1 explanation uses no concept outside the prerequisite set of its level. A mechanical check against the graph confirms this. Usefulness: people grade it. People grade a monthly sample, and a judge grades everything. math2 also publishes the agreement between the judge and the people on that sample. LLM judges are least reliable on explanations. Thus an improvement that only a judge sees does not pass the gate without a human-graded sample.

17.4 Run data

Every agent run is a record (11.6). Together, the records are math2's own dataset:

• Outcome per target: solved or not, with cost, model, prompt version and the retrieval used. The orchestrator uses this data to learn which ladder rung to start at for each kind of target (11.4).
• Premise use: which retrieved premises appeared in the final proof. This data trains the premise reranker (14.5).
• Failure classes: timeout, elaboration loop, wrong decomposition, statement mismatch, injection attempt detected. The classification is automatic, and people check a sample.
• Cost curves: solve rate against spend, by role, tier and model. The weekly report (12.9) plots this curve, and the budget split (11.5) is tuned on it.

The transcripts of merged runs are public (11.6), so their outcome data is public too. Each quarter, math2 also publishes a dataset of all runs, merged or not. It contains targets, outcomes and costs, but no transcripts for unmerged runs. This applies the AGMAI and Tao position on the report of negative results and resource use (document 01) to the project's own agents.

The package agent/dataset and m2 agent dataset make the dataset of a quarter as JSON Lines, with one row for each run that started in it. A row has the job, the role at its version, the models, the outcome, the budget, the spend and the verdicts of the novelty check. It has no transcript, and the transcripts of the merged runs stay in their run records (11.6). A job on behalf of a person gives only the word person, and the free texts lose their email addresses, keys, tokens and home directories.

17.5 The novelty check

Some outputs can be described as new: an explore conjecture, a proof of an open node, a counterexample. Before that, the output goes through a novelty check, and the result of the check is attached to the node:

1. Graph. Search the statement plane for the statement, its negation, and its specialisations and generalisations (14).
2. Record plane. Search aligned and unaligned results from the literature. Use the formula, embedding and lexical channels.
3. External indexes. Query zbMATH Open, TheoremSearch, TheoremGraph and Matlas where their APIs allow (09.6). Also query arXiv full text of licence-permitted papers through tamnd/arxiv. Query MathOverflow and Math.SE through the Stack Exchange API.
4. Problem databases. For a problem node, check these sources: the status and comments in the erdosproblems database, the solved markers in the formal-conjectures repository, the comments of the OEIS entry, and the LMFDB.
5. Verdict. known (with the source), likely-known (close matches that a person should read), or no-match-found. No verdict says "new". no-match-found means that these searches found nothing. Only a person makes a statement of novelty, after they read the matches.

The check is in the novelty package. novelty.Check runs each search on the claim and keeps each search and each match in the result, thus the run record of the output can keep them. The searches are novelty.Graph on the search index of the build, novelty.Records on each source of the record plane with the channels of the aligner, and novelty.ZbMATH, novelty.ArXiv, novelty.StackExchange and novelty.OEIS on the web. The records of the problem databases give their status to the match. A judge compares the claim with the three best matches of each search. A match that states the claim, or a result that implies it, makes the claim known. A related match, or a match that the claim generalizes, makes it likely-known. With no judge, each match makes it likely-known, because a person must read it. A search that fails is in the result, and the check does not give no-match-found when a search failed. A match keeps only its source, its id, its link and the verdict of the judge (09.6). The goal of explore (12.5) runs the check on each conjecture and counterexample of the run, and the field novelty of the run record keeps the result by node id.

math2 evaluates the check like everything else. Its suite contains results that are known to be in the literature. Each result is phrased as it would come out of an agent. The suite includes the 2025 to 2026 rediscoveries (document 01). Measured: recall of known. Sometimes the novelty check misses a rediscovery and a person finds it later. That rediscovery then goes into the suite.

The suite is in bench/novelty. Its first items are classical results in the words of an agent output, with the node of the test tree or the paper of the suite that makes each one known, and some results that the searches do not have. With an oracle judge, the recall of known measures the searches: the match must be in the three best matches of a search. With the judge of explore, it also measures the judge, and the items with no match measure how often the judge calls a result known by mistake. The rediscoveries of 2025 to 2026 are not in the suite yet, because each item needs a source that a person checked.

17.6 External benchmarks

math2 does not optimise for public benchmarks. But it runs them, for two reasons. They put the agents of math2 on a common scale with the agents of everyone else. And the fresh benchmarks are useful held-out sets. Each release reports the results with their costs. These results never replace the suites above.

Contamination rules for every external benchmark:

• During an evaluation, no context that an agent sees contains the items or their solutions. Search excludes them (bench_exclude in the run configuration), and the canary rule checks for leaks.
• The report gives results separately for items published before and after the training cutoff of each model.
• When a run solves an item, it reports whether search returned the solution of the item or a close neighbour. Thus a "solve" by retrieval is labelled as one.

17.7 Graders: judges and people

Many checks in math2 end in an LLM judge: back-translation (10.4), the critic, alignment, explanation grading, and the ranking in the novelty check. The 2026 evidence about judges is mixed (document 01):

• On competition proofs, the best judges agree with human graders at about 90%. This is about as often as human graders agree with each other.
• Agreement fell when the proofs came from AI pipelines that were optimised against judges. One study found a 31.7% false-positive rate.
• Judges show a "reviewer-pleasing" bias towards confident, well-formatted text.
• A minimum over several judges reduced overestimation.

Thus math2 applies four rules to every judge:

1. Judges triage. They never certify. No judge verdict raises the E-level or F-level of a node. Judges decide what a person examines first, and which items go to the kernel for a check.
2. Min over a panel. Sometimes a judge's verdict gates something (for example, F1 needs a back-translation pass). Such a gate uses at least two judges from different model families and takes the more severe verdict.
3. Judges are evaluated on adversarial items. The suite of every judge includes outputs from math2's own agents that people marked wrong. If a judge cannot tell a wrong proof by an agent from a right one, math2 does not use that judge to grade agents.
4. Human grading follows First Proof. When people grade agent output in an evaluation, they do not know the source: agent or human, and which model. They use a rubric that gives separate scores for correctness, exposition and attribution. A wrong answer scores lower than an abstention, so a confident wrong answer costs more than no answer.

17.8 Reporting

The notes of each release include an evaluation section that is generated from reports/eval/<release>/:

• the status error bounds: the share of sampled E2 to E4 nodes whose evidence did not support their level (0.5% of each level per month, re-checked by a curator who did not add the evidence), and F-level re-review disagreement (10.8);
• the battery confusion matrix and its change since the last release;
• search headline metrics against the external baselines (14.7);
• per-role solve rates, dollars per solve, and contamination gaps between public and fresh items;
• external benchmark results with costs;
• known failures: the items each suite failed, linked.

If a number got worse, the notes say so first.

Markdown · Source · Edit