LemmaBench: When AI Finally Meets Real Mathematics

Most AI math benchmarks still feel like exam rooms.

The model receives a problem. It produces an answer. We score the answer. Everyone argues about whether the problem was hard enough, whether the model saw something similar during training, and whether the leaderboard means anything outside the leaderboard. Very productive. Almost as peaceful as a faculty meeting.

Research mathematics is not an exam room.

A research lemma usually sits inside a paper like a machine part inside an engine. Its meaning depends on definitions introduced three pages earlier, conventions hidden in notation, assumptions that the author no longer repeats, and objects that are obvious only if you have been living inside that paper’s small mathematical universe. To test whether an AI can prove such a lemma, we first have to ask a less glamorous question:

Can we even turn the lemma into a fair standalone task?

That is where LemmaBench becomes interesting.¹ The headline result is easy to quote: current frontier LLMs prove only a small minority of fresh research-level lemmas, roughly in the 7–15% range under stricter judging in the reported evaluations. But the headline number is not the real story. The real story is the machinery required to produce the number at all.

LemmaBench is not just another “hard math benchmark.” It is a live benchmark pipeline: extract lemmas from new arXiv mathematics papers, recover the definitions and assumptions needed to make them self-contained, ask LLMs to generate structured proofs, and then judge those proofs with an independent evaluator, partly calibrated by human mathematicians.

That sounds simple only if one has never read a research paper in mathematics. Conveniently, reality remains rude.

The hard part begins before theorem proving

The common misconception is that research-level mathematical AI can be evaluated by taking difficult problems and asking models to solve them. This works tolerably well for contest-style problems, textbook exercises, and some formal theorem-proving tasks. It works less well for living research.

A contest problem is designed to be self-contained. A research lemma is not.

The paper makes this distinction central. A theorem statement inside a preprint is usually context-dependent: it may rely on objects, choices, notational conventions, and earlier definitions scattered throughout the paper. If a benchmark simply extracts that lemma and asks an LLM to prove it, the test becomes muddy. A failed proof might mean the model cannot reason mathematically. Or it might mean the model was never given the necessary definitions. Or it might mean the benchmark accidentally tested long-context retrieval instead of proof generation.

LemmaBench chooses a narrower and cleaner target: remove as much context dependence as possible before evaluating proof capability.

That choice matters. It turns the benchmark from a raw scraping exercise into a context-construction system.

The benchmark’s central insight is therefore operational: before asking whether an AI can prove research mathematics, we need a pipeline that can manufacture legitimate research-math proof tasks from live research artifacts.

That is less cinematic than “AI solves math.” It is also more useful.

Lemmas are small enough to test, but real enough to hurt

LemmaBench focuses on lemmas rather than theorems. This is a pragmatic choice, not a philosophical downgrade.

Lemmas are usually more granular than headline theorems. They are closer to the working units of mathematical research. They are also more tractable for current LLMs. If a model cannot handle lemmas, there is little reason to declare it ready for autonomous theorem proving. One should not ask a trainee surgeon to perform a transplant because they once opened a lunchbox.

The pipeline first identifies lemma environments in LaTeX sources. The authors note that from the second benchmark iteration, they discard lemmas that bear a reference, since those may simply restate known results from earlier literature. That filter matters because the purpose is to test proof generation on fresh research-level material, not memorized or imported statements.

Then comes the real extraction problem: making the lemma self-contained.

The paper compares two retrieval strategies:

This is the kind of result enterprise AI teams should recognize immediately. Cheap retrieval is attractive until the missing context is exactly what determines whether the output is valid.

Vector retrieval is not “bad.” It is doing what many retrieval systems do: find locally relevant passages. But mathematical self-containedness often depends on dependency chains, not keyword proximity. A symbol can be defined indirectly. A convention can be introduced in prose. A lemma can depend on a structure whose meaning is distributed across several prior paragraphs.

Full-context retrieval is more expensive because it is solving a harder task: dependency tracing inside a technical document.

The business version is familiar. In legal, engineering, finance, and compliance workflows, the answer often depends not on one matching paragraph but on all the assumptions that make a paragraph legally, technically, or financially meaningful. Search retrieves text. Evaluation needs context.

The benchmark is “live” because contamination is a moving target

Static benchmarks decay.

Once a benchmark becomes famous, it enters the training and tuning ecosystem. Models may see the exact problems, near-duplicates, solutions, discussions, or synthetic variants. Even when no one cheats, benchmark leakage becomes hard to exclude. This is especially awkward in mathematics, where recent progress has been fed by large corpora of competition-style and formal math data.

LemmaBench responds by taking problems from newly uploaded arXiv papers. The authors present two iterations: one based on papers from the last week of August 2025, evaluated in September 2025, and another based on papers from the first week of February 2026, evaluated in February 2026.

The idea is not merely “newer data is better.” The stronger idea is that a benchmark pipeline can be rerun. Old benchmark instances can become training data without destroying the validity of future benchmark instances, because tomorrow’s benchmark is produced from tomorrow’s research stream.

That changes the incentive structure.

A static benchmark rewards optimization against a frozen artifact. A live benchmark rewards capability that transfers into newly produced expert work. It does not eliminate gaming, but it makes contamination structurally harder. The leaderboard treadmill becomes slightly less ridiculous. Slightly.

Self-containedness is the first quality gate

The paper’s extraction evaluation is not a side detail. It is the condition that makes the proof results interpretable.

In the reported extraction tests, the authors evaluate whether the generated lemma-plus-context items are actually self-contained. They use LLM judges and human mathematician review. The human validation results show that among lemmas judged self-contained by the LLM, a substantial proportion were indeed self-contained: depending on model and retrieval mode, reported positive predictive values range from 75.5% to 96.5%.

The full-context approach performs better than vector retrieval across the reported comparisons. For example, Gemini 2.5 Pro with full context is reported at 96.5% human-confirmed self-containedness among judge-approved items, while its vector retrieval version is lower at 88.4%. GPT-5 full-context extraction reaches 90.0%, while GPT-5 vector retrieval reaches 85.0%. GPT-4 variants are weaker, especially under the o3 judge, but show the same broad pattern: full context gives stronger self-containedness than vector retrieval.

The important interpretation is not “full context wins, therefore always use long context.” That would be too easy, and therefore suspicious.

The more useful interpretation is:

1. Self-containedness is measurable enough to be a pipeline gate.
2. The gate has false positives and false negatives.
3. Different judges apply different implicit standards.
4. Human review is still needed to calibrate trust.

The paper’s cross-model validation is especially useful here. GPT-5 appears to act as a conservative validator: when it confirms Gemini-extracted lemmas as self-contained, manual inspection finds very high reliability, but GPT-5 also rejects some items that humans later consider self-contained. In business terms, this is a high-precision, lower-recall filter.

That is often the right trade-off for benchmarks. A benchmark item that is unfairly included can corrupt downstream conclusions. A valid item that is excluded is regrettable, but less damaging. In evaluation design, false positives are often more toxic than false negatives.

Proof evaluation: the pass rates are low, but the low number is not the only message

Once LemmaBench has self-contained lemmas, frontier models are asked to generate structured proofs. The protocol requires numbered proof steps, explicit subgoals, citation of hypotheses when used, and clear announcement of known theorems. An independent LLM judge then evaluates each proof step, and the whole proof is accepted only if all steps pass.

This is strict, but appropriately so. In mathematics, one broken step is not a charming stylistic flaw. It is the proof equivalent of a bridge missing a support beam.

The reported September 2025 iteration evaluates a benchmark of around 240 usable elements. Proof acceptance rates are low:

The human confidence score is important. It reflects the proportion of LLM-accepted proofs that human experts also considered correct, based on a reviewed subset. The sample is limited, but it gives a calibration signal: LLM judges are not arbitrary, yet they are not perfect.

The February 2026 iteration is larger in extraction scale. The authors select 100 preprints, extract 677 lemmas from 81 of them, and report that 405 lemmas, or 59.8%, are judged self-contained after GPT-5 full-context extraction and judging. The resulting benchmark contains 358 elements.

Under the most critical judge, GPT-5 proving judged by GPT-5 reaches 55 accepted proofs, or 15%. Other judges are more generous. Claude Opus 4.5 judges GPT-5 proofs at 35%, while Gemini 3 Pro judges them at 19%. For Gemini 3 Pro as generator, GPT-5 accepts only 3%, while Gemini 3 Pro accepts 16% and Claude accepts 29%. For Claude Opus 4.5 as generator, GPT-5 accepts 2%, Gemini 3 Pro accepts 14%, and Claude accepts 17%.

These numbers need careful reading.

The strict version says: the best reported model under the strictest judge proves about one in seven self-contained research lemmas. That is not autonomous mathematician territory.

The generous version says: depending on the judge, acceptance can look materially higher. That does not necessarily mean the model is better. It may mean the evaluator is more permissive. The paper itself treats judge reliability as part of the benchmark problem, not as an invisible detail to be politely ignored.

The business lesson is simple enough to be uncomfortable: AI evaluation is never just about the model being tested. It is also about the evaluator, the task construction process, and the calibration regime behind the score.

If your vendor reports “35% success” and your internal review standard says “15%,” both numbers may be produced by a coherent process. Only one may be useful for your risk tolerance.

The appendix is not a second thesis; it explains operational coverage

The appendix material supports the pipeline story rather than introducing a separate argument.

The related-work appendix positions LemmaBench against other math benchmarks, especially those built around curated advanced problems, formal theorem proving, or research problems with directly verifiable answers. This distinction matters because LemmaBench chooses broader coverage over deterministic answer-checking. Other benchmarks may be easier to verify; LemmaBench aims to be closer to the messy distribution of actual research lemmas.

The domain breakdown shows that the benchmark spans multiple mathematical areas, including combinatorics, probability, analysis of PDEs, mathematical physics, category theory, statistics theory, and others. The distribution is not uniform, and some domains have very few lemmas. That is a boundary on interpretation, not a defect. A one-week live sample will reflect the uneven flow of arXiv submissions.

The algorithmic appendix clarifies the pipeline as a directed process: source retrieval, parsing, extraction, self-containedness judgment, proof generation, proof judgment, and dataset consolidation. This reinforces the main point: LemmaBench is not primarily a dataset. It is a repeatable evaluation workflow.

The example lemma in the appendix, involving a Hilbert–Schmidt operator, shows the kind of task produced by the pipeline: assumptions are gathered, the lemma is stated, and proof steps are generated in a structured form. The HTML rendering loses some mathematical notation, but the intended role of the example is clear. It demonstrates what “self-contained enough to test” looks like in practice.

This is a useful discipline for reading AI papers: not every table is a new claim. Some tables define the measurement instrument. In LemmaBench, the measurement instrument is the product.

The business value is live evaluation, not “math AI” alone

For most businesses, research-level mathematics is not the immediate use case. Few companies urgently need an AI to prove a lemma in symplectic geometry before lunch. Some may; most do not. But the benchmark design generalizes.

LemmaBench offers a pattern for enterprise evaluation in expert domains:

1. Start from newly produced expert work.
2. Extract task units from that work.
3. Make each task self-contained by recovering hidden context.
4. Use model judges as scalable first-pass evaluators.
5. Calibrate those judges with expert human review.
6. Repeat the process over time so the benchmark stays alive.

This pattern applies naturally to domains where static QA sets become stale or contaminated: legal analysis, compliance review, engineering design, scientific literature screening, financial research, medical coding, cybersecurity incident analysis, and internal knowledge workflows.

The key is not to copy LemmaBench mechanically. A legal benchmark does not need theorem-proof formatting. A compliance benchmark does not need arXiv. An engineering benchmark may require simulations or design constraints. The transferable idea is the live pipeline.

This is where the paper becomes relevant beyond mathematics. Enterprises do not merely need better models. They need better ways to know what their models can do this month on the work that actually matters.

A frozen benchmark answers: “How did the system perform on a known test set?”

A live benchmark answers: “How does the system behave against the current stream of expert tasks?”

The second question is more expensive. It is also closer to reality. Reality, unfortunately, keeps updating without asking the leaderboard committee.

The governance lesson: evaluator quality becomes part of model quality

LemmaBench also exposes a governance problem that will become more common as AI systems move into expert work.

When outputs are open-ended, evaluation is no longer trivial. A proof is not a multiple-choice answer. A legal memo, architecture recommendation, diagnosis summary, or risk report is not a single number. If the evaluator is another model, then the system has two layers of uncertainty: generation uncertainty and judgment uncertainty.

The paper handles this by separating generator and judge, requiring step-level proof evaluation, and using human mathematicians to estimate judge reliability. This is not perfect. It is, however, more honest than pretending that open-ended expert output can be scored like a spreadsheet cell.

For business deployments, the lesson is direct:

• Do not report model performance without reporting evaluator design.
• Do not trust automated judges without calibration.
• Do not compare vendors unless the task construction and scoring standards are aligned.
• Do not treat a generous judge as evidence of a brilliant model. Sometimes it is just a lenient examiner with better manners.

The enterprise version of LemmaBench would need audit logs, reviewer sampling, disagreement analysis, escalation rules, and versioned evaluation sets. In other words, evaluation becomes an operating system, not a slide in the procurement deck.

Boundaries: what LemmaBench shows, and what it does not

LemmaBench is strong because it measures something closer to living research mathematics. It is limited for the same reason.

First, the sample sizes are still modest. A few hundred benchmark items are useful for signal, but not enough to make sweeping claims about all mathematical domains. Some fields are represented by many lemmas; others by only a handful.

Second, the proof evaluation depends on LLM judges. Human validation suggests the approach is useful, but not definitive. Judge disagreement in the February 2026 table is large enough that any single acceptance rate should be treated as conditional on the judge.

Third, the benchmark tests natural-language proof generation, not necessarily fully formal proof in Lean or another proof assistant. That makes it closer to how mathematicians often write, but less mechanically verifiable.

Fourth, the live nature reduces contamination risk; it does not magically abolish all evaluation risk. If models gain access to recent preprints, if benchmark construction becomes predictable, or if task-generation rules leak into training workflows, new forms of gaming may emerge. Evaluation is an arms race with better stationery.

Finally, the current results do not prove that LLMs are useless for research mathematics. A model that proves 15% of fresh lemmas under strict conditions may still be valuable as an assistant, a proof-suggester, a reviewer of candidate arguments, or a generator of partial strategies. The paper’s results mainly argue against premature claims of autonomous research-level theorem proving.

That distinction matters. “Not autonomous” is not the same as “not useful.” It means the workflow still needs humans, tools, verification, and careful task design. A depressing discovery only if one expected the machine to replace the department by Friday.

The real contribution is a benchmark factory

The most important thing LemmaBench contributes is not a leaderboard.

It contributes a benchmark factory.

The pipeline takes live research papers and turns them into proof tasks that are self-contained enough to evaluate. That factory can be rerun. It can produce future benchmark instances. It can generate historical training data. It can steer domain composition. It can reveal judge disagreement. It can incorporate human audits without requiring experts to handcraft every problem from scratch.

The low proof acceptance rates are therefore evidence inside a larger argument. They show that current models still struggle with fresh, context-heavy research-level mathematics. But they also show why static benchmark success should not be overinterpreted. Once the task distribution moves from curated exercises to live expert production, the performance story becomes much less flattering.

That is useful. Benchmarks should make reality harder to ignore.

For Cognaptus readers, the broader point is this: the next stage of AI evaluation will not be won by collecting a bigger pile of old questions. It will be won by building systems that continuously transform current expert work into fair, auditable, domain-grounded tests.

Mathematics is merely the sharpest version of the problem. It punishes missing assumptions. It exposes invalid reasoning. It makes judge quality visible. Business domains are often messier, but the structure is similar.

The practical question is no longer:

Can AI solve impressive benchmark problems?

It is:

Can AI perform reliably inside the live stream of expert work, where the context is incomplete, the standards are domain-specific, and the evaluator must itself be evaluated?

LemmaBench gives one answer: not yet at human-level autonomy, but far enough to measure seriously.

That may be less exciting than another gold-medal headline. It is also more durable.

Cognaptus: Automate the Present, Incubate the Future.