Proof-oriented execution for difficult mathematics.
A persistent runtime for planning, verifying, formalizing, and auditing mathematical work.
Quick start · Architecture · API · Development
Math Research Agent treats a theorem as a durable execution job rather than a single model request. Runtime-owned state, independent verification, formal process gates, and evidence receipts determine what can be accepted.
Expand
- Overview
- Hackathon submission
- Quick start
- Architecture
- Core capabilities
- Proof execution model
- Effect showcase
- MathArena benchmark
- First Proof long-horizon benchmark
- Durability and evidence
- Runtime states
- API
- Formal verification
- Long-running research
- Configuration
- Cloud Run
- Repository layout
- Development
- Documentation
- Design invariants
- License
Math Research Agent is a TypeScript system for persistent mathematical proof execution. It accepts a theorem, creates a session, plans work, dispatches focused tasks, records intermediate artifacts, verifies candidate arguments independently, and exposes the result through an HTTP/SSE API.
The project has two execution scales:
| Scale | Runtime | Purpose |
|---|---|---|
| Tactical | ProofRuntime / ProofWorkflow |
Solve and verify a single proof obligation |
| Strategic | ResearchRuntime |
Maintain a long-running research project with claims, evidence, routes, checkpoints, and root closure |
The model supplies mathematical work and planning proposals. The runtime owns task dependencies, persistence, recovery, provider boundaries, evidence metadata, and submission gates.
This project is submitted as an entry to the All Things Agentic Hackathon. The submission uses Gemini through Google Vertex AI and includes a Google Cloud Run deployment profile for the hosted demonstration.
- Node.js 22 or later
- pnpm 11 or later
- Google Cloud CLI and Vertex AI access for real model calls
- Lean 4, Lake, and the pinned Mathlib environment for local formalization
git clone https://github.com/dongxuelian2/math-research-agent.git
cd math-research-agent
bash scripts/install.sh
bash scripts/start.shThe installer runs a frozen pnpm install and builds the TypeScript backend. Open:
- Workbench: http://127.0.0.1:3080
- Proof API: http://127.0.0.1:43100
- Health: http://127.0.0.1:43100/health
To run only the proof API:
pnpm start:apiFor Windows, use scripts/install.ps1 and scripts/start.ps1.
The default profile uses Google Vertex AI through @google/genai. Authenticate with Application Default Credentials:
gcloud auth application-default loginCredential values are read at runtime. Configuration stores environment-variable names, not credential JSON or private-key material.
Click the diagram to open the original PDF reference.
The architecture is organized around six boundaries:
| Layer | Main components | Responsibility |
|---|---|---|
| Experience | Proof Workbench, CLI/API clients, local mode, Cloud Run mode | Accept theorem requests and present proof state |
| API control plane | Proof API Server, session lifecycle, event stream, ConfigService | Expose stable HTTP resources and configuration snapshots |
| Core execution | ResearchRuntime, ProofRuntime, dynamic planner, workers, verifier pool, formalizer, state reducer | Execute proof and research state transitions |
| Tool plane | Role Factory, Agent Core, scoped tools, Provider Registry | Construct configured roles and constrain model/tool access |
| External systems | OpenAlex, Git remote, Cloud Identity | Literature, optional corpus publication, and cloud authentication |
| Durable data and trust | Session Store, Run Workspace, Research Store, evidence receipts, corpus archive | Persist state, artifacts, verification evidence, and controlled projections |
The original reference is available as PNG and PDF.
| Capability | Implementation |
|---|---|
| Dynamic task planning | Planner action protocol with spawn, dependency edges, success criteria, and continuation tasks |
| Ready-frontier execution | Only tasks whose dependencies are complete are dispatched; independent tasks can run concurrently up to maxWorkers |
| Independent verification | Worker results are inspected by a separate verifier pool before candidate submission |
| Proof repository | Candidates, merged feedback, failed routes, and whiteboard state remain available across planning rounds |
| Durable recovery | Sessions, runs, configuration snapshots, step state, and partial outputs survive process restarts |
| Formal process gate | Lean source is checked by the configured lake env lean process before formal acceptance |
| Evidence-aware research | Research tools record artifact reads, searches, references, and trust receipts |
| Provider isolation | Provider adapters are selected by configuration; role definitions do not grant arbitrary tool permissions |
| HTTP/SSE integration | The GUI uses the public API and event stream without importing proof runtime internals |
| Controlled corpus projection | Canonical corpus publishing is a separate, opt-in outbox and reconciliation path |
flowchart LR
theorem["Theorem"] --> session["Session"]
session --> api["Proof API"]
api --> planner["Planner"]
planner --> frontier["Ready frontier"]
frontier --> workers["Parallel workers"]
workers --> verifiers["Independent verifiers"]
verifiers --> candidate["Verified candidate"]
candidate --> submission["Submission gate"]
submission --> result["Proof result"]
submission -. "prove_and_formalize" .-> formalizer["Formalizer"]
formalizer --> lean["lake env lean"]
lean --> result
result --> artifacts["Durable artifacts"]
artifacts --> planner
The default workflow mode is dynamic. A planner round receives the theorem, whiteboard, repository index, previous outputs, failed routes, budget, and current task graph. It returns typed actions that the runtime validates before execution.
Each task may declare:
dependsOn— predecessor task IDs that must complete first;successCriteria— the local result required from the task;continuationOf— the previous task when work is partial or retryable;- a scope and contribution kind — for example a local lemma, route analysis, or synthesis task.
The runtime computes the ready frontier, runs independent tasks in bounded batches, sends merged worker/verifier feedback into the next planner round, and persists every transition. maxWorkers limits concurrency; it does not decide how a theorem should be decomposed.
legacy mode remains available for compatibility with the fixed Planner/Worker/Verifier workflow.
| Role | Responsibility |
|---|---|
| Planner | Select the next proof actions and task graph |
| Worker | Produce a focused mathematical contribution or candidate proof |
| Verifier | Independently check the worker result and report a verdict |
| Synthesizer | Assemble accepted contributions into a final research or proof artifact |
| Formalizer | Produce or repair complete Lean source |
| Research Director | Select strategic research actions and target obligations |
| Corpus Bootstrapper | Import configured mathematical corpus material |
| Secondary Auditor | Re-check final research evidence and closure conditions |
The role factory resolves model profiles and tools from trusted configuration. A task description can state what an agent is for, but it does not itself grant access to tools.
The two responses below address the same q-Kneser graph problem. Only representative proof checkpoints are shown; this is an output-quality comparison for one difficult problem, not an aggregate benchmark.
| Proof checkpoint | Direct response | Structured agent response |
|---|---|---|
| Minimum eigenvalue | Derives the same spectrum and reaches lambda_min = lambda_1 through a parity split and a Gaussian-binomial ratio comparison. |
Makes the monotonicity checkpoint explicit: f(j) = |
| Extremal-family uniqueness | Uses a “general position” choice of a subspace and asserts that a weighted sum becomes non-integral. The required existence argument and the contradiction are not established. | Counts W_(L,U), derives N1 c_L + N2 (1 - c(U+L)) = 0, obtains c_L = 0 for L not subset U, and forces F = F_(L0). |
| Theta and capacity | Uses edge-transitivity to state that an SDP optimizer has the form J + cA, then applies the sandwich bound. The symmetry reduction is stated rather than independently checked. |
Writes the same candidate matrix and spectral calculation as a concrete derivation, while the runtime still treats the result as a candidate until verification and the selected formal gate pass. |
The comparison is most visible in the transition from a claimed geometric construction to a checkable counting argument.
Choose Y in general position so that no positive-weight point is contained in Y.
Then sum_(L subset Y) c_L is claimed to lie in (0, 1).
This contradicts the {0, 1}-valued indicator.
The missing step is the construction of such a subspace Y and the proof that the weighted sum has the asserted value.
N1 c_L + N2 (1 - c(U+L)) = 0
c(U+L) = 1
c_L = 0 for L not subset U
support(c) subseteq intersection_(U in F) U
F = F_(L0)
For the spectrum, the same response also exposes the independent audit trail: f(0) > f(1) > ... > f(k), followed by lambda_min = lambda_1.
The project preserves this distinction at runtime: a worker result is independently verified, passed through the submission gate, and formalized with lake env lean when the selected proof mode requires it.
We evaluated Math Research Agent on 122 official MathArena final-answer problems across four categories. The Agent result uses the complete execution workflow: parallel workers, independent verification, and continued repair/recovery until success or a terminal wall. Gemini is the original direct-response baseline on the same problems.
| 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 complete workflow gives the Agent an 8.20 percentage-point overall lead. The strongest separation appears on Apex 2025, where the Agent solves 8 of 12 problems versus 5 of 12 for direct Gemini; the Agent also reaches 100% on both AIME 2026 and HMMT Feb 2026.
Benchmark artifacts:
- Performance chart (PNG) · editable SVG
- Official score summary
- Retry and recovery audit
- Benchmark runner · chart generator
To measure proof planning rather than only final-answer accuracy, we ran five research-level problems from the First Proof Second Batch. Each problem was solved by a one-shot Gemini baseline and by the dynamic planner/worker/verifier workflow. Two reversed-order blind referee passes scored correctness, plan execution, 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 |
The agent wins 8/10 blinded pairwise comparisons, with a +25.1-point mean lead. The result is primarily a proof-quality signal: the strongest agent submissions preserve a multi-stage plan, verify boundary cases, and stop at a precise open obstruction instead of forcing a false classification. A larger workflow budget does not guarantee correctness—the metric-geometry submissions are both rejected for a central Stokes/coarea gap.
Benchmark artifacts:
- Performance chart (PNG) · editable SVG · chart data
- Detailed report · review summary
- Benchmark runner · recovery tool · blind referee · chart generator
Each proof run has its own workspace under .math-agent/proof-runs/:
.math-agent/
├── sessions/
│ └── <session-id>.jsonl
├── proof-runs/
│ └── <session-id>/<run-id>/
│ ├── THEOREM.md
│ ├── THEOREM.lean
│ ├── WHITEBOARD.md
│ ├── run_config.json
│ ├── state.json
│ ├── PROOF.md
│ ├── PROOF.lean
│ ├── repo/
│ └── steps/
│ └── step_NNN/
│ ├── planner_context.json
│ ├── planner_response.txt
│ ├── planner_plan.json
│ ├── actions.json
│ ├── worker_*_output.md
│ ├── verifier_*.json
│ └── step_status.json
└── research/
└── <project-id>/
├── state.json
└── artifacts/
The session JSONL contains typed lifecycle entries. The run workspace contains the full theorem, plans, prompts, outputs, verifier records, whiteboard, repository, and formal attempts needed for recovery and audit.
Research artifacts carry content hashes, provenance, references, and authority classifications. Tool use is recorded separately from the mathematical result. A worker may discover or read evidence, but a claim becomes authoritative only through the configured verification, reduction, and closure path.
The corpus archive is a projection layer. Raw planner, worker, verifier, scratch, candidate, and audit outputs are not published directly to the canonical Git corpus.
| State | Meaning |
|---|---|
CANDIDATE_READY |
A candidate passed independent verification and is waiting for the submission gate |
PARTIAL |
A budget or step limit was reached while resumable work remains |
PROVED |
The configured submission path passed; formalization also passed when required by the selected mode |
FAILED |
The workflow ended without an accepted route |
BLOCKED_FORMAL |
The formalization project or Lean process is unavailable |
BLOCKED_PROVIDER |
A model, literature, or remote tool provider is unavailable |
CANCELLED |
The caller cancelled the run |
CANDIDATE_READY is not a final proof state. A model label, a generated file, or a successful worker response is not sufficient for PROVED.
| Method | Endpoint | Purpose |
|---|---|---|
GET |
/health |
Runtime and deployment health evidence |
GET |
/v1/config |
Read the effective configuration |
GET |
/v1/config/document |
Read the editable TOML document |
PUT |
/v1/config |
Apply a revision-checked configuration update |
GET |
/v1/config/models |
Read the redacted model catalog |
| Method | Endpoint | Purpose |
|---|---|---|
POST |
/v1/sessions |
Create a session |
GET |
/v1/sessions |
List sessions |
GET |
/v1/sessions/:sessionId |
Read session state |
POST |
/v1/sessions/:sessionId/theorem |
Submit a theorem |
POST |
/v1/sessions/:sessionId/proof-runs |
Start a proof run |
GET |
/v1/sessions/:sessionId/proof-runs |
List runs for a session |
GET |
/v1/sessions/:sessionId/proof-runs/:runId |
Read run state |
GET |
/v1/sessions/:sessionId/proof-runs/:runId/events |
Stream typed events over SSE |
GET |
/v1/sessions/:sessionId/proof-runs/:runId/result |
Read the final result |
POST |
/v1/sessions/:sessionId/proof-runs/:runId/cancel |
Request cancellation |
API_URL=http://127.0.0.1:43100
SESSION_ID=demo-session
curl -fsS -X POST "$API_URL/v1/sessions" \
-H 'content-type: application/json' \
-d '{"sessionId":"demo-session"}'
curl -fsS -X POST "$API_URL/v1/sessions/$SESSION_ID/theorem" \
-H 'content-type: application/json' \
-d '{"theorem":"For every integer n >= 1, 1 + 3 + ... + (2n - 1) = n^2."}'
curl -fsS -X POST "$API_URL/v1/sessions/$SESSION_ID/proof-runs" \
-H 'content-type: application/json' \
-d '{"mode":"prove"}'Copy the returned runId and inspect the stream, state, and result:
RUN_ID=<run-id>
curl -N "$API_URL/v1/sessions/$SESSION_ID/proof-runs/$RUN_ID/events"
curl -fsS "$API_URL/v1/sessions/$SESSION_ID/proof-runs/$RUN_ID"
curl -fsS "$API_URL/v1/sessions/$SESSION_ID/proof-runs/$RUN_ID/result"| Mode | Required output |
|---|---|
prove |
A candidate that passes the informal submission path |
formalize_only |
A process-verified PROOF.lean |
prove_and_formalize |
An accepted informal proof and a process-verified Lean proof |
The full local profile enables formalization. A Formalizer may generate a Lean declaration and proof, or preserve a caller-provided exact declaration and fill its proof. The result is stored as an untrusted draft first; the configured Lean process is the acceptance authority.
The runtime uses lake env lean in the session project. Compilation failure is persisted as a formal attempt and routed back into the workflow for repair. Proof-local sorry, admit, axiom, constant, and opaque escapes are rejected.
Run the repository formalization project directly:
cd formalization
lake env lean MathResearchAgentFormalization.leanSee formalization/README.md and docs/PROOF_WORKFLOW.md for the complete formalization contract.
ResearchRuntime is the strategic layer above tactical proof runs:
Research project
-> corpus bootstrap
-> research director
-> tactical directive
-> ProofRuntime
-> evidence receipts
-> ResearchStateReducer
-> root readiness
-> synthesis and independent audit
Research projects persist:
- root objective contracts and claims with revision history;
- dependencies, support edges, routes, coverage, and open obligations;
- corpus documents and bootstrap reports;
- execution plans, task attempts, artifacts, and evidence receipts;
- trust receipts, authority receipts, checkpoints, and final-proof history;
- formalization status and root-closure readiness.
Core research routes include:
| Method | Endpoint | Purpose |
|---|---|---|
POST |
/v1/research/projects |
Create a research project |
GET |
/v1/research/projects |
List research projects |
POST |
/v1/research/projects/:projectId/root |
Set the root objective contract |
POST |
/v1/research/projects/:projectId/start |
Start a research campaign |
POST |
/v1/research/projects/:projectId/resume |
Resume a campaign |
GET |
/v1/research/projects/:projectId/frontier |
Read the current research frontier |
GET |
/v1/research/projects/:projectId/root-readiness |
Check root closure readiness |
POST |
/v1/research/projects/:projectId/synthesis |
Run root synthesis and audit |
GET |
/v1/research/projects/:projectId/audit |
Validate persisted research invariants |
Corpus publishing is disabled by default. Its outbox, reconciliation, retry, and optional Git projection are controlled independently from research truth.
Configuration is TOML-based and revisioned. An active proof run keeps the configuration snapshot created at run start; later edits affect subsequent runs.
| Profile | Use | Formalization |
|---|---|---|
configs/math-agent.toml |
Full local runtime | Enabled; creates session Lean projects |
configs/math-agent-cloud-run.toml |
Lightweight Cloud Run demo | Disabled; uses non-formal prove mode |
The configuration controls:
- runtime host, web/API ports, and data directory;
- proof mode, workflow mode, worker concurrency, and step limits;
- formalization, literature, research, budget, and corpus policies;
- scoped tool capabilities and allowed executables;
- provider profiles, model parameters, and role mappings;
- corpus roots, import authority, archive behavior, and optional publication.
The provider registry includes Google Vertex AI, Google, OpenAI-compatible, OpenRouter, DeepSeek, Anthropic, Codex CLI, and Mock adapters. The default profile uses Google Vertex AI with gemini-3.7-flash.
The Cloud Run deployment runs the GUI and proof API in one service and exposes them from one run.app origin. The service routes /health and /v1/... to the in-process API and serves the Workbench from the same port.
export CLOUD_RUN_PROJECT="your-gcp-project-id"
export CLOUD_RUN_REGION="us-central1"
export GOOGLE_CLOUD_LOCATION="global"
bash scripts/deploy-cloud-run.shThe deployment uses docs/CLOUD_RUN_DEMO.md. Cloud Run storage is temporary, so this profile is for a bounded demonstration rather than a durable multi-instance research archive.
.
├── apps/
│ └── proof-workbench/ Browser Workbench and thin static server
├── backend/
│ ├── src/agent/ Agent core and role execution
│ ├── src/api/ HTTP API and resource routes
│ ├── src/proof/ ProofRuntime, planning, verification, and formalization
│ ├── src/providers/ Provider adapters and registry
│ └── src/research/ ResearchRuntime, evidence, closure, and corpus
├── configs/ Local and Cloud Run TOML profiles
├── docs/ Workflow, runtime, deployment, and architecture docs
├── formalization/ Lean 4/Lake project
├── projects/ Local example and runtime project data
└── scripts/ Install, start, deploy, and repository utilities
Install dependencies and run the main checks:
pnpm install --frozen-lockfile
pnpm run typecheck
pnpm run test:proof
pnpm run buildUseful commands:
| Command | Purpose |
|---|---|
pnpm run build:proof |
Compile the backend |
pnpm run build:gui |
Check the Workbench and server entrypoints |
pnpm run typecheck |
Run the backend TypeScript typecheck |
pnpm run test:proof |
Build and run backend proof/research tests |
pnpm run corpus -- status --project <project-id> |
Inspect the corpus archive outbox |
pnpm start:api |
Start only the proof API |
pnpm start |
Start the local Workbench and API |
The backend tests cover configuration parsing, role and model validation, provider behavior, persistence, proof planning, dynamic dependencies, continuations, formal gates, HTTP/SSE resources, research reduction, authority receipts, and restart recovery.
GitHub Actions is currently disabled for this repository; there are no active repository workflows.
| Document | Scope |
|---|---|
docs/PROOF_WORKFLOW.md |
Tactical proof workflow, planner protocol, artifacts, states, and formal gate |
docs/WORKFLOW_RUNTIME_V2.md |
Dynamic DAG execution, ready frontiers, dependencies, and recovery |
docs/MATHEMATICAL_RESEARCH_RUNTIME.md |
Strategic research runtime and project lifecycle |
docs/MRR_V1_INVARIANTS.md |
Research truth, evidence, authority, and closure invariants |
docs/CORPUS_ARCHIVE_PROTOCOL.md |
Corpus outbox, reconciliation, and publication policy |
apps/proof-workbench/README.md |
Browser Workbench boundary and local serving model |
formalization/README.md |
Lean toolchain and process verification |
docs/CLOUD_RUN_DEMO.md |
Cloud Run deployment and runtime evidence |
- Model prose is input to the runtime, not the authority for truth.
- A worker result must pass independent verification before candidate submission.
PROVEDis emitted only after the configured submission and formal gates pass.- Provider failure, formal-tool failure, and mathematical failure remain distinct states.
- A resumed run uses its persisted configuration and artifacts rather than silently mixing current settings into old state.
- Research claims require evidence and authority receipts; a verified subtask is not automatically a proof of the root objective.
- Corpus publication is an explicit projection and cannot rewrite research truth when Git or remote publication fails.
Math Research Agent is released under the MIT License.