Polymath Swarm

A verification-first multi-agent swarm for research and mathematics. A supervisor breaks a problem into a task graph, and specialist agents (literature, reasoning, computation, Lean 4 formalization, critique, synthesis) work on it in parallel. Every claim in the final answer carries evidence that is re-checked independently: a citation whose quote is re-found in the paper, a computation that is re-run in a sandbox, or a Lean 4 proof that compiles with zero sorry and only standard axioms. Anything unproven is reported as a conjecture.

Why

LLMs are fluent and often wrong, and the errors look just like the right answers. Polymath Swarm never takes an agent's word for anything. Agents produce artifacts (search queries, check programs, Lean proofs, counterexample searches). Code runs them through sandboxed tools, and a verification gate reproduces every piece of evidence before a claim may appear in the answer.

Related MCP server: scholar-memory

How it works

flowchart TD
    U[Problem] --> S[Supervisor / Planner<br/>adaptive team per problem type]
    S --> G[(Task DAG)]
    G --> R{Router<br/>parallel dispatch}
    R --> LIT[Literature<br/>arXiv · S2 · OpenAlex · full text]
    R --> REA[Reasoner]
    R --> CMP[Compute<br/>SymPy · sandboxed Python]
    R --> FOR[Formalizer<br/>Lean 4 + Mathlib]
    R --> CRI[Critic<br/>counterexample search]
    LIT & REA & CMP & FOR & CRI <--> BB[(Blackboard<br/>Postgres + Redis)]
    CRI -.->|refuted → revision round| R
    BB --> VG{Verification gate<br/>re-fetch quote · re-run program ·<br/>re-verify Lean · re-run counterexample}
    VG -->|verified| SYN[Synthesizer] --> OUT[Answer + evidence report<br/>Markdown · JSON · trace]
    VG -->|otherwise| CJ[Conjectures / refuted] --> OUT
    M[(Episodic memory<br/>pgvector)] -.->|similar verified claims| S

• Orchestration: LangGraph, with a Postgres checkpointer, so runs resume after a pause, crash or kill -9. Human plan approval is optional, and budgets cap USD, tokens, wall clock and iterations.

• Tools: every tool is an MCP server (literature, sandbox, sympy, lean, knowledge).

• Memory: papers are ingested into pgvector for hybrid retrieval (full-text + vector, rank fusion, local cross-encoder rerank). Verified claims from past runs are recalled, then re-verified.

• Interop: the swarm and each specialist are A2A agents, and roles can be delegated to external A2A agents.

• Observability: OpenTelemetry traces go to self-hosted Langfuse, with every agent, tool and LLM call and its cost.

Details: docs/architecture.md · design decisions: docs/adr/ · threat model: docs/security.md.

Results

Single agent (one LLM call, same models and checkers) vs. the swarm, from evals/reports/2026-11-05. Small samples, so these numbers are indicative. The run used the OpenAI profile (gpt-5 for Lean, gpt-5-mini elsewhere), with deterministic scoring.

The swarm trades coverage for trust. It proves what the single agent can't, matches it on MATH while backing most of its claims with re-run computations, and never cites a paper that doesn't say what it claims. The single agent answered more research questions, but half of its citations were unsupported. Hybrid retrieval on a labelled set reaches recall@10 = 0.983, MRR = 0.950.

End-to-end demos with committed evidence reports and traces are in examples/. They cover a Lean-verified proof, a reproduced computation, verified literature quotes, and lemma reuse from memory.

Quickstart

Prerequisites: Docker, uv, and an LLM provider key (Anthropic by default; OpenAI works with POLYMATH_MODEL_PROFILE=openai). Node ≥ 20 only if you develop the UI.

git clone https://github.com/Gnanasudharsan/polymath-swarm.git && cd polymath-swarm

cp .env.example .env

Edit .env: set ANTHROPIC_API_KEY (or OPENAI_API_KEY plus POLYMATH_MODEL_PROFILE=openai), and set POLYMATH_API_KEY to any secret string for the HTTP API.

Option A: the whole stack (API + web UI), one command

docker compose --profile app up -d --build

Open http://localhost:3100. The API is on http://localhost:8000, and the A2A Agent Card is at http://localhost:8000/.well-known/agent-card.json.

Option B: the CLI

docker compose up -d --wait

docker compose --profile tools build sandbox

uv sync

uv run polymath solve "Compute the sum of the first 100 primes; is it prime?" --max-usd 0.5

The evidence report is written to reports/<run_id>.md and .json. Useful flags: --approve-plan (review the plan first), --memory (no Postgres/Redis), --no-tools.

Optional extras

A2A interop

The swarm is an A2A agent. Each specialist (literature, reasoner, compute, formalizer, critic) is too, at /agents/<role>/. Cards are public; calls need the x-api-key header.

POLYMATH_API_KEY=... uv run python examples/a2a_client.py "Is 2^10 + 1 prime?"

POLYMATH_API_KEY=... uv run python examples/a2a_client.py --agent compute "Is 97 prime?"

To delegate a role to an external A2A agent, set POLYMATH_A2A_DELEGATES={"literature": "https://other-agent.example"}. Its replies are treated as untrusted proposals and can never be "verified" on the remote's word.

CLI

Configuration

All settings come from environment variables or .env (see .env.example and src/polymath/core/config.py).

Multiple users

uv run polymath keys new alice

This prints Alice's key (shown once) and a hash entry. Put the hash entries in POLYMATH_API_USERS={"alice":"sha256:...","bob":"sha256:..."}. Each user sees only the runs they started, over REST and A2A; users in POLYMATH_API_ADMINS see all of them. The web UI uses the key in its own POLYMATH_API_KEY, so it acts as that one user.

Limitations

• Small evaluations. The published comparison uses 3–6 problems per suite because of budget, and miniF2F is sampled from the easier mathd_* problems.

• Verification-first means abstaining. With no verified claim, the swarm says so rather than guessing, which can lower accuracy on questions a single model answers correctly from memory.

• Lean image size. Lean needs a 15 GB image and about 3.5 GB of RAM per REPL. Without it, proofs cannot be verified (other evidence still works).

• Docker socket. The containerised API reaches the Docker socket to start sandboxes, which is root-equivalent on the host. Bind it to localhost and see docs/security.md.

• Simple users. Users and hashed keys live in configuration (no sign-up, no per-user spend quotas, only user/admin roles).

• Paraphrase in research QA. Keyword scoring penalises paraphrase, and literature results vary run to run because search ranking does.

• Claude profile untested live. The Anthropic profile is the default but was not exercised live during development, which used the OpenAI profile.

Development

uv sync && uv run pre-commit install

uv run ruff check . && uv run ruff format --check . && uv run mypy src && uv run pytest -q

uv run pytest -m integration -q

Integration tests need Docker. Their lean and network subsets need the Lean image and internet access; live tests call real models. The frontend e2e runs with cd frontend && npx playwright test. Project memory for contributors and coding agents is in CLAUDE.md; history is in PROGRESS.md and CHANGELOG.md.

License

MIT