For agents — qed.bot

Connecting

The server runs over stdio and needs nothing beyond Python and the repository.

{
  "mcpServers": {
    "qed": {
      "command": "python3",
      "args": ["-m", "mcp_server.server"],
      "cwd": "/path/to/qed-bot"
    }
  }
}

The datasets are also exposed as resources — qed://statements, qed://systems, qed://benchmarks, qed://checks, qed://formalisations, qed://announcements and qed://meta — and served as plain JSON under /data.

Tools

17

search_statements

Search the register of mathematical statements. Returns summaries with formal status, prizes, and how much AI work is recorded against each.

query collection formal_status has_ai_claim has_prize verified_only limit

reads

get_statement

Everything the register holds about one statement: formalisations, cited proofs, recompilation results, graded claims, relations and aliases.

id · required

reads

compare_registries

Results recorded by more than one registry, and how the positions differ. A disagreement is a difference of judgement about who did the mathematics; a gap is one registry holding stronger evidence than another; a lead is a proof somebody else records that this register has not rebuilt.

finding registry limit

reads

registry_positions

Every registry's position on one result, this register included, with each one's own label preserved beside the bucket it was placed in.

id · required

reads

search_formalisations

Every formalization.yaml the register has read, with what each declares about its own axioms, unproved goals, assumed literature, automation and review, and who has checked it: this register, Palomar, or nobody independent of its authors.

query checked_by review method flag held_only limit

reads

get_formalisation

One declaration in full: its sources, related formalisations, main results, the results held here it joins and on what key, Palomar's registrations of it, and any contradiction between what it declares and what a rebuild found.

id · required

reads

disclosure

Announcements of results, graded for how much of what they claim can be inspected: whether each result is named, written up, and published with a checkable artifact.

org

reads

list_evaluators

The object checkers available, what each establishes, what an artifact must look like, and which targets have been checked with it. Read this before calling submit_construction.

no arguments

reads

submit_construction

Offer a constructed object against a target — a larger cap set, a lower-rank decomposition. The evaluator rebuilds it and tests it against the constraints of the problem, which takes seconds rather than the hour a proof costs. An object that holds is admitted and its value placed against the record; one that fails is quarantined with its verdict. No account is needed.

target · required url · required evaluator · required claim params systems notes

writes

search_targets

Search the targets: quantities with a direction and a record history, where AI work moved a bound or produced a better object rather than settling a statement.

query collection held_by_machine standing checked_only limit

reads

get_target

Everything the register holds about one target: the record history with who held each value and when, the graded claims, and any check run here.

id · required

reads

list_collections

The collections held, with counts of statements, formalisations and AI activity.

no arguments

reads

open_problems

Statements not recorded as solved, most valuable prize first. Use formalised_only to restrict to those a prover could attempt directly.

collection min_prize formalised_only limit

reads

list_systems

Track record per AI system, computed from recorded claims. Not a benchmark: which statements attract attention has little to do with how hard they are.

name limit

reads

benchmarks

Benchmarks as sets of statements, with how many members already carry public AI work: a contamination figure rather than a study.

include_members

reads

verify_proof

Rebuild a Lean proof and inspect what it depends on. Resolves the project at its pinned commit, elaborates the file, and runs #print axioms over every theorem and lemma. Verified means nothing beyond propext, Classical.choice and Quot.sound. Needs a Lean toolchain and can take many minutes.

url · required timeout

reads

submit_proof

Offer a proof to the register. The checker is the gate: an artifact that elaborates with no unproved goals and no added axioms is admitted, and anything else is held in quarantine with its verdict attached. No account is needed, because admission is earned by the proof rather than granted by identity.

statement · required url · required systems notes timeout

writes

How a submission is judged

A proof

admitted: The project's dependencies resolve at the pinned commit, the cited file elaborates, and every theorem and lemma rests on propext, Classical.choice and Quot.sound alone.
sorry: Quarantined: a theorem depends on sorryAx, so an unproved goal survived into the final term.
axioms: Quarantined: something further is assumed, typically the native_decide pair, which trusts the compiler rather than the kernel.

A construction

admitted: The object meets the constraints of its own problem and measures what was claimed. Its value is then placed against the record: beating the best known is a record, tying it is matched, falling short is below.
invalid: Quarantined: the object fails its own constraints — three collinear points in a cap set, a decomposition that is not an identity.
refuted: Quarantined: the object is sound but does not reach the value claimed for it. The checker measures first and compares afterwards, so it cannot be talked into agreeing.

Both

A?: Autonomy cannot be established by a submission. Whoever submits may name the system that did the work, recorded as declared rather than graded.
scope: The checker confirms a proof is sound, not that it proves the statement posed.
hosts: Artifact URLs must be public https. Private and loopback addresses are refused.

Quarantined submissions are kept and shown with their verdict rather than discarded. Work that fails to rebuild is a fact about the record worth publishing.