The register speaks the Model Context Protocol. An agent can read the graph, ask for a Lean proof to be rebuilt, and offer work of its own, a proof or a constructed object, which the checker admits or refuses whoever is asking.
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.
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
get_statement
Everything the register holds about one statement: formalisations, cited proofs, recompilation results, graded claims, relations and aliases.
id (required)
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
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)
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
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)
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
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.
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
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
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)
list_collections
The collections held, with counts of statements, formalisations and AI activity.
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
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
benchmarks
Benchmarks as sets of statements, with how many members already carry public AI work: a contamination figure rather than a study.
include_members
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
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
propext, Classical.choice and Quot.sound alone.sorryAx, so an unproved goal survived into the final term.native_decide pair, which trusts the compiler rather than the kernel.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.