Real ScreenShot
Settings

Math Research Agent: Persistent, Auditable Mathematical Research

Inspiration

Most AI assistants treat a theorem as a one-shot prompt: ask for a proof, receive an answer, and start again when the answer fails. This approach is poorly suited to difficult mathematics.

Open-ended research needs persistent memory, independent criticism, and a clear distinction between a promising idea and an accepted proof. A failed route may contain a useful reduction or counterexample, while an unchecked lemma can waste an entire research session.

Math Research Agent was built to preserve the entire research process: what was attempted, what failed, what remains unresolved, and what has actually been verified.

What it does

Math Research Agent turns a theorem into a durable execution job.

It creates a session, builds a dependency-aware plan, dispatches focused agents, records their work, and sends candidate arguments to independent verifiers. The planner receives structured feedback and can continue, split, retry, or abandon individual routes without losing the rest of the research campaign.

The system supports both short proof obligations and longer research projects. A run preserves the theorem, task graph, whiteboard, intermediate artifacts, configuration snapshot, partial outputs, verifier decisions, failed routes, counterexamples, and recovery context.

This allows a run to survive interruptions and resume from evidence instead of starting over.

Formal verification is an explicit trust boundary. When enabled, a Formalizer generates or repairs complete Lean source. The runtime checks that source with the configured lake env lean process. A generated file, model label, or successful worker response is never treated as a formal proof by itself.

Benchmark results

The advantage of the workflow is measurable on both final-answer accuracy and long-horizon proof quality.

MathArena: final-answer accuracy

We evaluated Math Research Agent on 122 official MathArena final-answer problems across four categories. The baseline was a direct, one-shot Gemini 3.7 Flash response.

The initial agent workflow achieved 102/122 official correct answers. We then targeted the incomplete cases(Cause by network issue) with up to three bounded recovery rounds. Recovery succeeded on 13 of 20 targeted cases, producing a best-of result of 115/122 (94.26%), compared with 105/122 (86.07%) for direct Gemini.

That is an 8.20 percentage-point improvement over the one-shot baseline.

Category	Math Research Agent	Gemini 3.7 Flash direct
AIME 2026	30/30 (100.0%)	28/30 (93.3%)
HMMT Feb 2026	33/33 (100.0%)	30/33 (90.9%)
Apex 2025	8/12 (66.7%)	5/12 (41.7%)
Apex Shortlist	44/47 (93.6%)	42/47 (89.4%)
Overall	115/122 (94.26%)	105/122 (86.07%)

The recovery result is important because it demonstrates more than parallel generation. The system retained failed attempts, routed them back into planning, and used additional reasoning only where the persisted evidence indicated that recovery was possible.

First Proof: long-horizon proof quality

To evaluate research-level reasoning, we ran five problems from the First Proof Second Batch. Each problem was solved by both a one-shot Gemini baseline and the Math Research Agent workflow.

Two reversed-order blind referee passes evaluated mathematical correctness, proof planning, critical-step completeness, useful partial progress, and exposition on a 100-point scale.

Problem field	Math Research Agent	Gemini 3.7 Flash direct
Computability	38.5 / 100	38.0 / 100
Discrete probability	88.5 / 100	44.5 / 100
Metric geometry	20.0 / 100	21.0 / 100
Lattice theory	66.0 / 100	46.5 / 100
Algebraic combinatorics	88.0 / 100	25.5 / 100
Mean	60.2 / 100	35.1 / 100

Math Research Agent won 8 out of 10 blinded pairwise comparisons, with a 25.1-point mean score advantage.

The result also shows where the system still fails. Both metric-geometry submissions were rejected because of a central Stokes/coarea gap. The workflow did not hide that failure behind fluent exposition; it preserved the objection and identified the missing mathematical machinery.

Benchmark reports and artifacts are available in the repository:

How we built it

Math Research Agent is a TypeScript monorepo with a browser-based Proof Workbench and a backend proof core.

The Workbench communicates with the backend through an HTTP/SSE API. It receives typed progress events for planning, task dependencies, worker results, verifier verdicts, formalization attempts, and final state transitions.

The runtime owns the orchestration and trust boundaries:

a Planner selects the next actions;
ready tasks execute in bounded parallel batches;
Workers make focused mathematical contributions;
independent Verifiers inspect those contributions;
a submission gate decides what can be accepted;
the Formalizer and Lean process handle formal proof modes.

Tasks can declare dependencies, success criteria, and continuation relationships. The runtime computes the ready frontier, carries predecessor results into dependent tasks, persists every transition, and recovers incomplete work after interruption.

The hosted demonstration runs the Workbench and API together on Google Cloud Run and uses Gemini through Google Vertex AI. The full local profile additionally supports Lean and Mathlib-based formalization.

Why it is agentic

Math Research Agent is not a chat wrapper around a single model call. It is a multi-agent research process with distinct roles and different failure responsibilities.

Planning, exploration, falsification, verification, formalization, and synthesis are separate stages connected by durable artifacts. Independent workers can explore different approaches, while verifiers provide adversarial feedback instead of simply repeating the original model’s reasoning.

The runtime can react to partial outputs, compiler errors, failed routes, and newly discovered dependencies. When a worker stops before completing its task, the unfinished result becomes durable PARTIAL state and can be continued. When a verifier rejects a route, the objection is preserved and returned to future planning rounds.

The core loop is:

$$ \text{plan} \rightarrow \text{explore} \rightarrow \text{verify} \rightarrow \text{repair or redirect} \rightarrow \text{submit} $$

Challenges

The hardest challenge was reliability over long horizons. Language models can produce fluent mathematics with subtle gaps. Multi-agent workflows introduce additional problems: duplicated routes, context loss, incomplete outputs, dependency mistakes, and contamination between supposedly independent branches.

We addressed these issues with typed planner actions, explicit dependency edges, bounded concurrency, independent verifier sessions, persistent artifacts, continuation tasks, evidence receipts, and runtime-owned state.

A second challenge was defining success honestly. In mathematical research, a failed proof attempt or a counterexample can be valuable progress. Math Research Agent preserves those results instead of rewriting them as success.

The runtime distinguishes states such as PARTIAL, CANDIDATE_READY, PROVED, FAILED, BLOCKED_FORMAL, and BLOCKED_PROVIDER. In particular, CANDIDATE_READY means that a candidate passed independent verification; it does not mean that the theorem has been accepted. PROVED is reached only when the configured submission path succeeds, including the Lean process gate when formal verification is required.

What we learned

The most important lesson is that AI-assisted mathematics works better when the model is part of a research process rather than treated as an oracle.

Separate roles create useful friction. Persistence turns failed attempts into reusable evidence. Runtime-owned state makes the process inspectable and recoverable. Independent verification and compiler feedback provide concrete boundaries around what the system is allowed to claim.

The goal is not to make every model response look complete. The goal is to make progress measurable, failures informative, and accepted proofs auditable.

What’s next

We are extending Math Research Agent’s research map, evidence retrieval, corpus projection, and formal repair loops.

The long-term goal is to make autonomous proof discovery more reproducible and transparent: mathematicians should be able to inspect not only the final argument, but also the routes explored, the objections raised, the evidence used, and the exact reason a result was accepted or rejected.