Architecture Decisions

Distributed crowdsourced Lean 4 proof network for open mathematical problems. Decisions only, thematically grouped; each states its rationale and overturning condition. Hover any dotted term — like Lean 4 — for its definition.

v3.48 · 2026-10-25 · Evidence base Harness_Architectures_research_v2.md — where the two disagree, this document governs · numbering frozen as citable identifiers at Stage 0 · v3.9 folded in the Stage 0 build readings (D-3, D-4, D-5, D-19, D-23, D-27, D-28, D-34, D-35, D-36, Stages); v3.10 the readings from specifying F01–F11 (D-3, D-4, D-13, D-16, D-28, D-29, D-35, Stages); v3.11 made D-4 step 9 a property of the statement, not of each artifact (D-4, Stages) — the F00 rehearsal finding; v3.12 rebuilt D-9's second rung as screened-and-signed on the 2026 fidelity evidence and fixed the three rules that follow from inheriting statements — drift, attempt counting, related-variant relevance (D-4, D-6, D-9, D-10, D-30) — and gave skeleton holes their own origin, the value D-25 already published and nothing could emit, with the annex citation as what distinguishes them from a partial proof's residual holes (D-3, D-9, D-12, D-28, D-31); v3.13 let a theorem keep every proof: a later complete proof of a proved node merges beside the first as an alternate, checked like a proof, not asked step 9, never judged for similarity, and credited at write-up (D-3, D-4, D-25); v3.14 let a check that carries no authority be delegated to a named hosted elaboration service, through one logged endpoint and its tool (D-4, D-28, D-35); v3.15 made a listed target claimable at once and moved the human check onto the proof: step 9 is waived by a certificate or by catalog evidence at five points, never by provenance alone, and a conjecture may carry several formalizations linked by equivalence exhibits (D-4, D-6, D-9, D-10, D-33); v3.16 scoped step 4's kernel replay on a Mathlib-pinned graph to the modules the graph builds, trusting the pinned Mathlib in the gate image, because a fresh replay of all of Mathlib exceeded the step cap on the first live partial (D-4); v3.17 gave open problems stewards: a named mathematician must commit to digest and write up a problem's result before it can be claimed, mathematicians may propose their own problems, explainers may be signed as a comprehension claim, and a resolved target shows its digestion state and is never announced before its paper (D-3, D-6, D-9, D-10, D-21, D-22, D-27, D-32, D-33, D-36, Stages); v3.18 said how a revision reaches the statements that depend on it — their dependencies are read through the revision and never rewritten, and stale lifts on the gate's evidence, not on anyone's say-so — and struck D-13's differential credit, which D-19 had already ruled out and no code had ever paid (D-8, D-13, D-18): the first outside contributor to work a revised hole found that its parent could never close; v3.19 said a decomposition never blocks the node it decomposes — a reduction's new node and a partial's holes are children the parent may draw on once they are proved, never dependencies it waits on, so the parent stays open to a direct proof and to rival decompositions and only the three closing artifacts settle it (D-12): the owner's reading, on seeing that the first merged partial had locked its root for everyone; and, the same day, that a proposer's speculative label yields to a merged artifact (D-14), found by reading the derivation for the Docs state map; v3.20 said what D-4 step 9 is for — the person who checks that a Lean statement says what its conjecture says is asked at the moment the conjecture is claimed settled, so step 9 is asked only of an artifact that would settle a target's root, never of a hole, a crux, a skeleton or a variant beneath it, and never on a calibration target, which claims nothing new — and that resolved is a fact about the root, so a variant proposed beneath a resolved root is open work (D-4, D-27, D-30, D-33): the owner's rulings on the 2026-09-19 run in which four outside agents proved versions of the infinitude of primes and spent most of each session waiting for a person; v3.21 said a node keeps every different proof and never a copy, so a submission identical (comments and whitespace aside) to one merged or open for the node is refused before any pull request opens, a hole takes one witness at a time and a statement is proposed once, and a losing racer's proof is moved to its alternate path by the service that opened it (D-25); that no hole may restate any statement its node reduces, not only the node's own goal, and that a decomposition shown circular by a gate-checked exhibit takes its hole off the frontier with nothing rewritten (D-12, D-16): the owner's rulings on the 2026-09-23 run, in which nine agents on three targets found the queue frozen, copies accepted without a word, and two skeletons whose hardest hole was the problem itself; v3.22 took a whole established circular path off the frontier with one claim, the ancestor staying open (D-12), and let a hole's witness skip what its decomposition already proved (D-29): the owner's rulings on the 2026-09-24 run; v3.23 turned the circularity exhibit round: it proves the hole's statement implies the ancestor's, because the implication v3.21 asked for is met by every provable hole and says nothing about ease (D-12, D-16): tester 69-C's finding on the 2026-09-29 run, and the owner's reading that circular is literal — you start at the premise and you end at it; v3.24 let a partial carry the witnesses of its holes, each held to step 7 before the merge, so that a hole whose witness was carried is created with it and is never blocked for want of one (D-29, D-3): the owner's ruling on the 2026-10-01 run, in which every level of a skeleton chain cost a second pass through the merge queue for a witness the precheck had already described; v3.25 let a proof declare uses — import lines after its statement's header naming a definition module of its target or the merged proof of another node of its target — held by the gate to the kernel term and to the statement's own meaning, and never followed into a cycle (D-3, D-4, D-8, D-12, D-29): the owner's rulings of 2026-10-01 on the testers' item B1, approved as drafted on 2026-10-03; v3.26 let an annex name its steps, held by the gate to the holes of a skeleton that cites it (D-31), gave a crux statement an append-only pointer to the node it was proposed for (D-14, D-3), and had the products list every way a target is proved, each with the nodes its proof term rests on (D-25): the owner's reading of erdos-1050's problem page, which could not say which nodes the proof needs, how its crux statements relate to it, or which outline it followed; v3.27 said what a verdict rests on — step 4 judges a contributor's compiled modules in a run that executes none of their code, for every artifact that claims a statement, whatever uses it declares (D-4) — let a listed curator withdraw a status record or a defect claim by an append-only withdrawal record, so that disputed has an exit (D-14, D-18), and let a listed curator correct a ledger line by a correction record the post-merge job applies by revoking the old entry and writing the corrected one (D-18, D-19): the owner's rulings on the re-audit of 2026-10-04, sections 1 to 3 approved as drafted; v3.28 said what a proposed statement may hold — its imports, open and namespace lines, doc comments and its declarations, so that nothing in a module of record runs code when it is loaded (D-3) — that every defect claim is shown and none blocks on its own (D-16), that a dispute is accepted for adjudication by a curator's disputed record naming the claim (D-18), and that the service reserves pseudonyms and issues write tokens that lapse after ninety days unless renewed, with no minimum age asked of a GitHub account (D-19): the owner's acceptance, the same day, of the five recommendations that followed the re-audit; v3.29 rebuilt v3.28's lapsing tokens for operators whose agents keep no memory between sessions — a token lapses only after a long stretch without use, so nothing has to be renewed, the human operator keeps a single-use recovery code that mints a new token for the same identity, and an agent is told to keep its token where the machine remembers it (D-19): the owner's reading that an agent forgets every credential between sessions, so a policy that depends on an agent remembering is built backwards; v3.30 gave every Lean file a mathematical version — an outline of every merged proof among the products, a gloss of every statement, witness, relation and definition module and an explainer of every proof, each drafted by the network and labelled unverified, then corrected by stewards version by version, with nothing edited and nothing machine-written in a product (D-3, D-23, D-28, D-33, D-35, D-36): the owner's request that a reader who does not know Lean can read every proof, every line one click from the Lean, and his rulings of the same day; v3.31 made the words contributors' work rather than a paid drafter's — the network drafts nothing, a contributor names the model that helped, a version earns its author credit when a steward or curator approves it, one writer at a time per file, and the words are read section by section, a section a person wrote or verified being closed to models while a person's change to approved words waits for approval (D-3, D-19, D-25, D-28, D-33): the owner's rulings of 2026-10-05 on the first drafts' cost and on keeping people's words from being overwritten; v3.32 held one writer to a chain's head as well as to a new chain, so a version superseding a head is refused while another open pull request supersedes the same head (D-3): the 2026-10-06 run, in which two versions superseding one head merged in one batch and forked the chain; v3.33 brought stewards and curators onto the site: a steward record and a words approval may be made by signing in with GitHub and signed by the network’s approval key, admission is a policy switch that starts open, curators are named by the owner, and a steward’s or curator’s own version is final once they sign it (D-3, D-22, D-28, D-32, D-35, D-36); v3.34 gave each target a panel of stewards that decides by motions, counting only votes cast, admits new stewards and experts by vote or by a curator, caps and lapses stewardships, makes signers of the write-up its coauthors, and shows the write-up at its highest stage from drafted to accepted, every number a value in policy.json, through three routes and the steward form (D-32, D-35); v3.35 made a merged circularity claim a published fact rather than a removal, because its exhibit is met by every reduction and by the last open hole of any decomposition, and gave a node a literature status — open, known, or elementary — proposed by any contributor and confirmed by a steward or curator, whose own page lists what waits for them (D-3, D-12, D-16, D-25, D-32): the owner’s rulings on the 2026-10-08 run of three testers on erdos-1094; v3.36 was reserved for the formalization review's draft (2026-10-09) and is not used, the review being applied as v3.39; v3.37 let a resolved target be registered in Palomar, the registry of Lean-verified mathematics, by a curator from a wrapper the pinned gate exports, named the two licences D-23 had left unnamed, made the per-merge disclosure of models and tooling a structured block with method, models and framework required, gave a registration its authors from the ledger with an opt-in display name, and added two append-only records, one read tool and two write tools (D-3, D-10, D-19, D-23, D-25, D-28, D-32, D-35): the owner’ v3.38 made a hole that restates a node under another branch a lemma of its parent &mdash (built 2026-10-10 as v3.36 and renumbered at its merge, v3.37 having been applied first); v3.39 made the fidelity pass a formalization review (D-9): candidates from people and models filtered by kernel-checked exhibits and intent tests with three probes, pairs recorded per direction with refutations kept, two signers named by role with the ladder earned under the review, a reading not chosen a variant (D-30), back-translation out of the pass, the evidence page where the proposer answers and the App tells them (D-36, D-35, D-28), who may open a review a policy setting; existing targets reviewed in the background, step 9 waiting for a complete review or catalog evidence — drafted 2026-10-09, settled 2026-10-10, prototyped twice, applied 2026-10-12 (F26);s rulings of 2026-10-10 after the Palomar read; v3.40 published a target’s routes and sufficient sets as facts — each merged decomposition with its holes’ facts aggregated, and every set of statements whose proofs would close the root — through the products, one read tool and the target page, the choice between claiming a hole and proposing a route staying with the operator’s filter (D-25, D-28, D-36): the owner’s request of 2026-10-15 after route lock-in on erdos-1094, built unattended as written (F27); v3.41 let the network write the proof that joins a node’s merged decomposition to its proved holes, or a proved hole to the ancestor its own circularity claim names, or a proved resolves variant to the root, and submit it through the gate like any proof, prechecked as any plain-git submission is, so one proof climbs the target one checked merge at a time; a node is proved only when that proof merges, a composed proof is never kept beside a real one, and the join earns no ledger line (D-12, D-25): the owner’s question on erdos-1094, whose node --h2--h2--h2--h2 had every hole proved and still read ready (F28); v3.42 replaced that proof file with the structure itself: a node whose decomposition, own circularity claim or (at the root) resolving variant has every input proved is proved by closure — the post-merge job joins the assembly with its inputs’ proofs at the level of terms, the kernel accepts the theorem, and a record signed with the gate key stands beside the node, so one merge closes a whole chain; the root reads proved only with its statement vouched as step 9 accepts (D-4, D-12, D-25): the owner’s question the same day, “by construction you should be able to close parent nodes” (F28); v3.43 retired the circularity claim and its label (D-12, D-16, D-25): the gate’s refusal of a hole definitionally equal to an ancestor is the whole rule, because for a one-hole decomposition or a last open hole the implication the claim proved is the assembly restated, so the label marked only where someone had filed (its closing link had gone in v3.42, F28-Q12); new claims of the class are refused, the merged ones stay as history, and the products drop the field — the owner’s ruling of 2026-10-15, built as F08-T42 and F04-T53, renumbered from v3.42 when F28’s rewrite took that number first; v3.44 gave every statement a label and a claim in notation and every route an approach, all contributors’ words on the record — a statement gloss may carry a label; a partial names, in its own comments, its approach, a licence for those words and each hole’s label and claim, is refused by the service before any precheck and by the gate at step 4 without them, and the post-merge job files them as the author’s gloss on each hole it writes; the products carry each node’s label, claim and where the label came from and each route’s approach; the target page navigates the sufficient sets by a tree of the route choices, each leaf one set, each interior node the family beneath it, built from the enumerated sets and never from the graph (D-3, D-12, D-25, D-28, D-36): the owner’s request of 2026-10-17 on reading erdos-1094’s frontier as an illegible mess, and his rulings the same day (backfill by agents through the service with no human sign-off, labels changed under the existing gloss rule, the table kept beneath the tree); v3.45 let a steward or curator dispute a proposed literature status as well as confirm it, the signed record naming the proposal it rejects and carrying the signer’s own reading, which the products publish beside the rejection; and put each literature record’s summary and references into the node’s context bundle, so an agent reads what is known without a second fetch (D-25, D-28, D-32): the owner’s request of 2026-10-19 after the reading of erdos-1094 against the literature; v3.46 let a route settle a conjecture either way — a refutes variant whose Relation.lean proves variant → ¬root, a proved one refuting the root by derivation through the same closure the resolving variant uses, every sufficient set saying which side it is on and the selector forking on the side first; a revision may give a proposed crux its relation with its routes intact; and proposed cruxes leave the proof tree for a band of their own, joined to it only by the lines the record has measured, lit on hover (D-8, D-12, D-14, D-25, D-28, D-30): the owner’s reading of erdos-257’s page on 2026-10-21, where the refutation side — three proved bookkeeping holes and one open core — was hidden behind a toggle and a proved spec pointed at an unproved root by a line that meant nothing; v3.47 let a steward of the target or a curator shelve a statement, or retire a merged decomposition, by a signed record with a cause — a judgment that it does not serve the root, not a verdict on it: the statement keeps its status, leaves the frontier, refuses work, and is drawn only on request with its hole children, while a shared hole another live route still needs, a statement a merged proof uses, and the root are never reached; a later unshelved record by the same roles lifts it and nothing is edited or deleted (D-14, D-25, D-28, D-32, D-35): the owner’s reading of erdos-257’s route 2 on 2026-10-24, fourteen proved special cases and two open holes that do not help the root, with no act on the site to take them off it; v3.48 replaced the home page’s counts with what happened lately on the record and one problem drawn, every sentence it says of the network true of the record it is rendered from (D-36): the owner’s reading of the home page on 2026-10-24, which led with a zero

Decisions only, thematically grouped. Evidence base is Harness_Architectures_research_v2.md; where the two disagree, this document governs. The Overview and Glossary are orientation, not binding; each decision is stated as: decision, one-line rationale, overturning condition — visible by default. Rules, mechanisms, tables and evidence sit in a collapsed Detail block beneath; they are binding too, just not needed for a first read. Research-grounded decisions carry an Evidence line with primary-source links; decisions without one are original design reasoning with no external precedent.

Overview§

What this is

A distributed network in which humans and AI agents collaborate to resolve open mathematical problems with machine-verified proofs. A curated mathematical target — typically a genuinely open Erdős-style conjecture, with no known proof — grows a graph of small, precisely stated lemmas along conjectured attack routes — proposed and refined largely by the contributors themselves, including proofs of honestly-labeled weaker variants of the target. Anyone may claim a lemma, prove it in the Lean 4 proof language using whatever tools they like, and submit the proof. An automated gate checks every submission mechanically; contributions that pass are merged, recorded, and credited. When a chain of lemmas closes the root, the conjecture is resolved and fully verified by the Lean kernel — new mathematics, not a translation of existing mathematics — and the record shows exactly who contributed what. Because the route is conjectured, refuted routes, counterexamples, and partial progress are first-class outcomes, not failures of the process.

Motivation

Three facts converged in 2025–2026. AI proving became cheap and started resolving genuinely open problems (AlphaProof Nexus, Astra) at token costs inside a hobbyist's subscription — an enormous idle proving workforce with nowhere to point itself. The Lean kernel makes a proof's correctness checkable perfectly and cheaply, but whether the formal statement says what the mathematician meant — fidelity — is not machine-checkable and fails often (6.5% correct under the intended interpretation, 2026). And no coordination layer exists for this work. Human crowdsourced projects (ETP, PNT+, FLT) proved the sociology works but assume good faith and hand-run coordination. Agent swarms that formalize known results (unsorry) proved the git-as-queue, kernel-as-gate infrastructure is tractable, and stop there: no curation, no fidelity review, credit that is farmable by construction, humans kept out of every loop, and — by their own roadmap — no open conjectures. The network's answer: trust artifacts, not parties. Every claim of progress is a machine-checkable object; what cannot be machine-checked — statement fidelity above all — gets a separate, adversarial human review layer applied only at roots and definitions, not at every lemma.

Who participates

The primary proving population is AI agents operated by math enthusiasts using spare subscription credits — not professional mathematicians. The repo itself is the agent interface: machine-readable task lists, structured context bundles, a local pregate script. Humans hold the judgment roles:

Role What they do
Prover (mostly agent-operated) Claims lemmas, submits proofs and structured failure reports
Curator Decides what mathematics enters the network, with prior-art and feasibility evidence; repairs defective root statements by versioning; consolidates duplicate nodes; declares a target dormant on published evidence (D-33)
Statement reviewer Adversarially audits whether formal statements match the intended mathematics
Auditor Spot-checks merged approvals and proofs after the fact
Adjudicator Resolves disputes
Writer Turns a target's finished record into the paper (or state-of-the-problem note) a human referee can read; proposes the retrospective significance and contribution statement
Steward (v3.17) A mathematician who commits, before an open problem can be claimed, to understand and write up whatever the network produces on it; may prove on it and earn proof credit like anyone, and may sign its Lean statement's fidelity where D-9's non-author rule allows; holds the writer role for that problem

Identity attaches to the human operator; agents are tools acting under their operator's account and accountability. Externally, the network leans on the existing ecosystem: Mathlib (the shared mathematics library), the Formal Conjectures registry and erdosproblems.com (statement sources and review venues), and the Lean Zulip community.

How conflicts are handled

How recognition works

Credit is an inclusive public ledger, not a prize — modeled on how large collaborative papers list contributions, not on winner-take-all bounties. Six separate lines: statement authorship, proof authorship, review, documented failed attempts, upstreaming to Mathlib, and write-up. Key properties:

The load-bearing ideas

  1. The gate is the sole arbiter. Acceptance is a property of the artifact — pinned toolchain, clean kernel replay, allowed axioms only, statement untouched — never of the contributor's reputation, effort or tools.
  2. Fidelity and integrity fail independently. Integrity (does the artifact prove the statement?) is mechanical and automated. Fidelity (is the statement the right mathematics?) is not automatable and gets graded human certificates on roots and definitions only.
  3. Everything is a checkable artifact — proofs, counterexamples, vacuity certificates, partial proofs, postmortems, and the gate's own verdicts, reproducible bit-for-bit.
  4. Informal arguments are input, never output. Prose attaches to a node as untrusted material and earns nothing until someone skeletonizes it — lemma structure in Lean, assembly proved, lemmas left open (D-31).
  5. Harness agnosticism. The protocol never blesses a tool; a hand-written proof and one from any AI system are indistinguishable to the gate.
  6. Public by default. Public claiming, attempt logs and review; exclusivity exists only on bountied nodes.
  7. Measure what's measurable. Planted canaries make review performance a number; escape rate is estimated from catch rate, never guessed.

Core protocol§

D-1 — Harness agnosticism§

The protocol specifies artifacts and a gate. It never specifies a toolchain. LeanMarathon, Goedel-Architect, hand-driven Claude Code or Codex, Aristotle, unaided hand-written Lean — all indistinguishable to the gate, which re-derives everything from a pinned toolchain in a clean sandbox.

Rationale: the only stance compatible with contributors on their own credentials; survives harness turnover; process is unenforceable against someone who controls their own machine, artifacts are not. Overturns if: submission quality varies so much by harness that the gate can't distinguish cheaply — in which case harden the gate, still don't bless a harness.

Detail evidence23 words

Evidence: research §1, §5 — LeanMarathon itself ran on Codex subscription with API-equivalent cost reporting; the gate cannot and need not distinguish harnesses.

D-2 — Unit of contract is the node; unit of intake is the target§

Claims, submissions, merges and credit are node-scoped. Targets are curated as a root plus its definition closure; the graph beneath them grows emergently (D-29). Subgraph claiming is permitted: a contributor may claim a connected set of ready nodes and submit together; the gate applies per node regardless. There is no paper-level contract.

Rationale: immutable statements, declared-dependency checks, and non-vacuity witnesses are all node properties; paper-scoped contracts reinstate a trusted orchestrator inside an untrusted contributor. Overturns if: subgraph claiming becomes the norm — then it is a paper-level market and node-scoping is overhead.

Detail evidence12 words

Evidence: research §1 — BlueprintRepair (node-named typed operations), Goedel-Architect (dependency-scoped parallel workers).

D-3 — Node layout§

nodes/<node-id>/
  META.yaml         # id, status, deps, statement-hash, origin (authored|compiler-derived|variant|skeleton-hole — v3.12), provenance, tutorial (D-27: off-ledger)
  Statement.lean    # signature, body `sorry`. Content-hashed. Immutable.
  Witness.lean      # instance satisfying the hypotheses
  Context.lean      # signatures of declared deps, bodies `sorry`
  Proof.lean        # the node's first merged proof: created once by a merge, never modified (v3.13; later proofs are alternates, D-25; the tutorial node excepted, D-27)
  Relation.lean     # variants only (D-30): the kernel-checked implication to or from the root; gate-checked at admission, immutable after
  attempts/         # append-only: postmortems (D-13), partial assemblies (D-12) and the witnesses they carry for their holes (D-29 v3.24), alternate proofs (D-25 v3.13)
  annex/            # content-hashed informal arguments, untrusted input only (D-31)
  literature/       # what the literature says of the statement, and its confirmation by a steward or curator (D-25 v3.35)
  explainer/        # post-merge prose accounts of Proof.lean: hashed, attributed, unverified (D-36); versioned (v3.30)
  gloss/            # prose saying what each Lean file of the node says: hashed, attributed, unverified, versioned; any status (v3.30)
  proposed-for/     # append-only: which node of the target a crux statement was proposed for, by its proposer or a curator (D-14 v3.26)

A submission is a PR touching exactly one Proof.lean (or several, for a subgraph) plus appends to attempts/ and annex/. Any diff touching Statement.lean, META.yaml, or another node's directory is rejected mechanically, before review. v3.13: once a node's Proof.lean has merged it is never modified; a later proof of the same node is submitted as one new attempts/<ts>-<pseudonym>-alternate.lean (D-25), and a diff that modifies a merged Proof.lean is rejected mechanically — except on the tutorial node, which D-27 keeps permanently open: every operator proves it again and it earns nothing, so its proof file is a rehearsal slot, not a record.

Explainers (explainer/). Once Proof.lean has merged, any contributor may append a prose account of the proof: what the argument does, why the route works, what the lemma buys the target. Explainers are content-hashed, attributed (human author plus drafting model if any, per D-23), and immutable — a correction is a new entry, never an edit. They are commentary on a kernel-checked object, not evidence about it: nothing in the network reads an explainer for truth, the website (D-36) labels them unverified wherever it shows them, and they earn on the write-up line (D-19), never the proof line. An explainer PR touches only explainer/ and is accepted by the path check alone, with no gate run. On a node with no merged proof it is rejected: that text is an annex (D-31) misfiled. v3.17 — signed explainers. An explainer may carry a signature by a real-identity contributor affirming one sentence: I can explain this proof without the tool that produced it. The signature claims nothing about the mathematics and changes no verdict. Its signer is accountable under D-22, and a signature its signer cannot stand behind is a D-17 ground (iii) matter. Only signed explainers count toward a target's digestion state (D-33).

v3.30 — versions. An explainer names the proof it describes — the node's Proof.lean, an alternate or a merged partial assembly — and may name the outline steps (D-35) each of its sections describes. It may supersede one earlier explainer of the same proof: the latest of its chain, never one already superseded. That is how an explainer is corrected; a version that has been signed may be superseded only by a steward of the target or a curator. Its author, a steward of the target or a curator may withdraw a version by a withdrawal record (v3.27); a chain's current version is its latest that is not withdrawn. Nothing is edited and every version stays in the tree.

v3.30 — glosses (gloss/). Any contributor may append a gloss to a statement, witness, relation or definition module, on a node of any status: prose saying what that file says, naming the hash of the exact text it describes. A gloss is content-hashed, attributed, unverified and immutable, and is versioned and withdrawn as an explainer is. A steward of the target or a curator may sign one, affirming that they have read it against the Lean and it says what the Lean says; that signature changes no grade, status or digestion state. A gloss of text that has since changed is shown as describing an earlier version. A root's words of record remain its curated informal statement (D-6, D-9). A gloss is not an explainer: an explainer's signature is a claim about a proof, and a statement has none to digest.

v3.30 — drafts. The network may draft the first gloss of every Lean file a merge creates, other than a root's statement, and the first explainer of every merged proof from its outline, through the same path as anyone's, attributed to the network's drafter and the model and version that wrote it, with no human author (D-23). A draft earns nothing, is labelled machine-drafted and unverified, and is a starting point for a steward, not an account. Model text lives only in such a record, never in a product (D-35).

v3.31 — no drafts; contributors write. The network drafts no words: v3.30's drafts are withdrawn as a mechanism. Glosses and explainers are written by contributors, whose agents may draft them; a version a model drafted names the model in drafted_with (D-23). The drafts filed on 2026-10-05 stay, attributed to the drafter, and may be superseded; no new record with a drafter block is accepted. A new chain of words on a file is refused while another open pull request is writing one, as a hole takes one witness at a time (D-25 v3.21).

v3.31 — words by section. A gloss or explainer is read section by section, a section being the words for some steps of the proof's outline and so for some Lean lines (a gloss is one section). A section a model wrote is drafted; one a person wrote is written; one a steward of the target or a curator has signed is verified. A model's version may change only drafted sections. A person's version may change any: over a drafted section the change is shown at once, over a written or verified one it is pending, kept in the record and shown beneath the approved words until a steward or curator signs it. Signing approves the sections it names and verifies them. This replaces v3.30's rule that only a steward or curator may supersede a signed version.

v3.37 — two records outside the node. targets/<id>/registrations/<date>-<n>.yaml records a submission to, or a registration in, a public registry (D-10 v3.37): the registry, its id and version, the wrapper repository and commit, the graph commit exported, the proof and attestation, and a status; appended by a curator or a listed steward of the target, the latest record per registry id is the one read, and a withdrawal record (v3.27) sets one aside. names/<pseudonym>.yaml at the graph root records a display name and an optional link for a pseudonym, written only by the holder of that pseudonym through the service and signed by the approval key; a later record with no name withdraws it. Nothing else reads a name in this version: it reaches a registration's authors (D-19 v3.37) and nothing on the site.

v3.31 — credit on approval. A gloss or explainer version earns on the write-up line (D-19) when a steward of its target or a curator approves it by signature, credited once to its author and never to its signer; an unsigned version, a draft, and a signature on one's own version earn nothing. This replaces "they earn on the write-up line" above, which no merge had ever paid.

v3.32 — one writer per head. A version that supersedes a chain's head is refused while another open pull request supersedes the same head, as a new chain is refused while another is being written (v3.31); a chain has one head, and two versions superseding it are a fork no reader can resolve. The second writer waits, then supersedes the version that merged. A fork already on the record is resolved by withdrawing all but the latest merge (the owner's ruling of 2026-10-06).

v3.33 — approval through the site. An explainer or gloss signature (v3.17, v3.30, v3.31) may be made through the service by a signed-in steward of the target or a curator: the service signs it with the network’s approval key (D-32 v3.33) over the same canonical body, naming the signer’s login, and it means what an SSH signature means and is accountable under D-22 the same way. A version written by a steward of the target or a curator may be signed by its own author, and its sections are then verified: the author answers for the words as writer and as approver. It earns once, on the write-up line, as the author’s work (D-19); the signature earns nothing beyond that, so v3.31’s rule that a signature on one’s own version earns nothing stands. Rationale: the owner’s ruling of 2026-10-07 that a draft “could be rewritten by a steward or curator”; under v3.31 a steward’s own rewrite stayed pending until a second steward signed it, so a problem with one steward could never finalise it.

v3.44 — labels and claims. A gloss of a statement may carry a label: a short name for the statement, at most 60 characters, plain text, no notation. Its body opens with the claim, the statement in mathematical notation as a display ($$…$$), followed by prose. A node’s label and claim are those of the current version (v3.31) of the first statement gloss chain filed on it; a node with none takes as label the name its hole bore in the route that made it, a root the target’s title, and the products say which (D-25 v3.44). A label or a claim is changed exactly as any gloss is: by a superseding version, anyone’s to propose, a steward’s or curator’s to approve, a person’s change over verified words pending until signed (v3.31, v3.33). Nothing is edited; no record but the gloss carries a label. A label is not an explainer and asserts nothing: it is how a statement is named, and a reader checks it against the Lean one click away. A gloss may also describe a merged partial (its file under attempts/): its first sentence is the route’s approach where the partial declares none (D-25 v3.44), so an older route’s intent can be written and corrected the way a label is; it carries no label.

v3.25 — uses. A proof, a partial proof's assembly or an alternate may declare what it draws on beyond its statement's header, in the one place a Lean file can: import lines directly after the statement's imports, each naming a definition module of the same target that is already on the graph, or the merged proof of another node of the same target. With those lines removed the file is the statement with its sorry replaced, as before; Statement.lean, its hash and META.yaml are never changed for a use. The declaration lives in the artifact, under the artifact's hash.

Rationale: makes BlueprintRepair's typed-operation discipline a filesystem property rather than a policy. Shared definitions (defs/). Each graph has a defs/ tier: shared definitions and cross-node helper signatures, content-hashed and immutable like statements, versioned via D-8, carrying fidelity certificates per D-9 (definitions are first-class review objects). No prover creates or edits a shared definition — they file a revision request, adjudicated by a curator (D-29). Context.lean imports from defs/; the path check above extends to reject any submission diff touching it.

Detail evidence75 words

defs/ rationale: a wrong definition yields a true theorem about the wrong object, so definitions need exactly the immutability-plus-review discipline statements already have; an open shared/ directory would be the one mutable surface every node depends on. defs/ overturns if: revision-request latency on definitions blocks proving — then pre-authoring definition coverage at intake (D-6 item 2) is failing and intake hardens, not the tier.

Evidence: research §1–2 — BlueprintRepair typed-operation discipline; LeanMarathon frozen editable regions.

v3.28 — what a proposed statement may hold. A proposed Statement.lean or Context.lean holds its imports, open, namespace and end lines, doc comments and its declarations — the statement's theorem, or the signatures of its dependencies — and nothing else; step 2 refuses any other command. The checks that judge a node import its statement as a module of record (D-4 v3.27), so nothing in it may run code when it is loaded. Every statement on the record when this was written already met it.

D-4 — The gate§

Orientation: in mechanism the gate is ordinary CI — a checklist run on every pull request. What makes it the gate is its role: it is the one component in the network with authority to say a proof counts, and no person's word substitutes for it (that is what "trust artifacts, not parties" means in practice). Steps 1–8 are mechanical and reproducible by anyone (D-5); step 9 is the only human judgment. Detail lists what each step defends against, and how the two rehearsal runs — pregate.sh and precheck_submission — relate to the real one.

Research §3 adopted whole, fail-closed, in order. A PR merges only if:

  1. CI resolves dependencies itself from pinned Lean toolchain + Mathlib SHA. Submitted lake-manifest.json ignored.
  2. Diff touches only permitted paths (D-3); statement hash unchanged.
  3. Build runs network-isolated, secretless, ephemeral, resource-capped. Elaborating a contributor's Lean file executes their code.
  4. Kernel replay from a clean environment (lean4checker --fresh or Comparator). v3.16: on a graph that pins Mathlib, the replay covers every module the graph itself builds — the node, its dependencies (cached or compiled) and defs/ — each replayed into the environment of its imports, and Lean's and the pinned Mathlib's own compiled files, fixed by the gate image's digest, are trusted rather than replayed. A fresh replay of all of Mathlib cannot finish within a graph's step caps.
  5. Axiom allowlist: exactly propext, Classical.choice, Quot.sound.
  6. Static hazard checkers over the statement (ℕ subtraction, division by zero, junk values, Int truncation, unused binders, off-by-one ranges).
  7. Non-vacuity witness present and typechecking.
  8. Declared-dependency check.
  9. Adversarial statement review by a non-author, recorded on the node — v3.11: satisfied by the root's fidelity certificate (D-9, at least screened-and-signed) or its D-10 registry provenance, checked at merge; a per-pull-request approving review by a non-author only where the root has neither. v3.15: registry provenance alone no longer satisfies it — where a statement came from is not by itself evidence that it says what the conjecture says. The second basis is recorded catalog evidence about the statement scoring at least five points (B+), pinned to the root as it stands; below that, a non-author approves the proof's pull request.

v3.25 — uses (steps 2, 4 and 8). Step 2 takes the statement's header with the artifact's use lines and refuses a line that names nothing usable; step 4, where a use is declared by the artifact or by a proof it is built on, first checks that what the artifact proved is the statement as the statement's own header reads it — an import may add names to prove with, never an instance, a notation or a name that changes what the statement's text means; step 8 holds the declared uses to what the kernel term uses: a used node the term does not touch is refused, and one it touches without declaring is refused as before.

v3.27 — what a verdict rests on (steps 3 and 4). Elaborating a contributor's file runs their code, so nothing that code could have written is evidence. Step 4 builds the contributor's modules, then judges them in a separate run that executes none of their code: the kernel replays the compiled modules, and the type of the declaration they hold is compared with the statement as its own admitted files read it. This holds for every artifact that claims a statement (a proof, an alternate, a partial proof's assembly), whatever uses it declares — it widens v3.25's “where a use is declared” to every such artifact, because a dependency's merged proof module carries whatever its file holds after the proof body and step 4 imports it in place of its signature. A metaprogram's verdict is read only as that program printed it. Overturns if: a faster check gives the same guarantee, shown on the real toolchain. Cost: on a Mathlib target the comparison adds about two imports of Mathlib to step 4, against the 600 s cap, measured before the re-pin (F08-T28).

Detail rules · figure · evidence1130 words

Amendment to research §3: native_decide is banned with a waiver path, not flatly — waiver requires recorded justification, reviewer sign-off, and a permanent node flag stating this node's trust base is the compiler, not the kernel. A flat ban produces routing-around rather than compliance. Where each lives: the justification is a file in the submission (nodes/<id>/waivers/native_decide.yaml, the one permitted addition beyond Proof.lean when the proof uses it); the sign-off is a line in the approving review naming the waiver; the flag is on the attestation (D-5), projected into graph.json and the website — never an edit to META.yaml, which stays immutable.

Hazards are admission-time failures with an acknowledgment escape. Step 6 runs over the statement, which cannot change after admission (D-8, D-29); an unacknowledged finding therefore blocks admission, or it would block every proof forever. The author acknowledges an intended construct in META.yaml (acknowledged_hazards: checker, location, one-line justification), which the statement reviewer sees (D-15). At proof time step 6 re-runs and repeats the admission result; it exists so the authoritative run trusts no prior verdict.

The authoritative gate requires an attached passing precheck attestation (precheck_submission, D-28, or pregate.sh, D-27 — structurally identical). Machine-speed submission without a local pass is bounced before CI spends a minute. What counts as attached. The precheck attestation carries a signature of kind service (signed by precheck_submission), contributor (signed with the operator's own SSH key, pregate.sh --sign) or none (unsigned pregate.sh output); each graph's gate-spec.json lists the kinds it accepts and a maximum age, and the gate records the kind it consumed. The precheck attestation keeps garbage out of CI and proves nothing else — the authoritative run re-derives every verdict — so a plain-git contributor with no key and no account is never excluded by it; abuse is answered at the identity layer (D-19).

The gate has a named owner. It composes independently maintained projects pinned to different Lean versions; every Mathlib bump can break the composition.

What each step defends against.

  1. Rebuild from our pins. A submitter who could supply the manifest could point at a doctored Mathlib in which the target is already an axiom.
  2. Paths and hash. The oldest trick: prove an easier theorem by quietly editing the statement.
  3. Isolation. Elaborating a Lean file runs its author's code. An unsandboxed build can read secrets, phone home, or wedge the runner. The isolated build runs on ephemeral hosted CI infrastructure, never on a machine the gate owner administers — a public repository's pull requests can execute code on a self-hosted runner, which is D-24's liability cliff — and its cpu, memory and wall-clock caps are declared per graph in gate-spec.json, not in the workflow. The same rule binds precheck_submission: a contributor's Lean is never elaborated outside the sandbox the gate uses. v3.14: a check that carries no authority may be delegated. check_lean (D-28) forwards a contributor's Lean to a named third-party elaboration service that runs its own sandbox; the network elaborates none of it, the answer is marked non-authoritative and can never attach to a submission, and the gate neither reads nor trusts it (D-1). The service is network configuration, one environment per pinned Mathlib, and replacing or dropping it changes no verdict.
  4. Kernel replay. The elaborator is large and has been fooled (lean4#8231); the kernel is ~5,000 lines. Rechecking from --fresh ignores any cached environment the submission could have poisoned.
  5. Axiom allowlist. sorry compiles — it introduces sorryAx. Any axiom beyond the three standard ones is a hole, whatever it is called.
  6. Hazard checkers. Statements that are true and meaningless: ℕ subtraction truncating at zero, division by zero returning zero, a binder nothing depends on.
  7. Witness. Unsatisfiable hypotheses make every conclusion provable; the witness shows the theorem is about something.
  8. Declared dependencies. A proof that pulls in undeclared nodes makes the graph and the ledger lie about structure.
  9. Non-author review. The one thing no checker can see: whether the statement means what it claims (fidelity). v3.11: this is a property of the statement, reviewed once where it can actually be assessed (D-9 intake, D-10 provenance), not of each artifact submitted against it. Merge is mechanical on steps 1–8 for any node under a root whose fidelity grade is at least screened-and-signed or whose statement is inherited from a D-10 registry with provenance recorded (D-6 item 3), and for the tutorial node (D-27); the attestation records the certificate or provenance it relied on in place of a reviewer. Where the root has neither — a statement the network authored and has not yet put through D-9's pass — an approving pull-request review by an identity other than the author is required, and the post-merge job writes that reviewer into the attestation (D-5). Every kernel-checked artifact of D-12 is treated alike: a counterexample of a certified statement merges as mechanically as a proof of it, since fidelity risk is symmetric and sits on the statement either way. Merge itself is mechanical in both cases: when steps 1–8 are green and step 9 is satisfied, the merge happens with no person pressing a button, so whatever human act stood behind step 9 is always on the record. Reverts (per-artifact review returns for that grade) if a confirmed defect claim (D-15) lands on a statement that merged mechanically. Why the change: the F00 rehearsal (2026-09-08) showed per-artifact approval on an already-certified statement is a click that adds no information, and the kernel has already re-derived the artifact. v3.13: step 9 is not asked of an alternate proof (D-25) — a second or later proof of a node whose Proof.lean has already merged. Steps 1–8 run on it in full; it changes no verdict, status, dependency or credit, and the statement it proves was already put through step 9 when the first proof merged, so a review would again be a click that adds no information. Its attestation records no reviewer. v3.20: step 9 is asked only of an artifact that would settle the target: a closing artifact of D-12 (proof, refutation, vacuity) on the target's root, or a proof of a variant labelled resolves (D-30) while the target is not yet resolved, which is a proof of the root by another road. Nothing else asks it — not a hole, a crux, a skeleton, a reduction, a partial or related variant, nor a resolves variant beneath a root that is already closed — and steps 1–8 alone merge those. Why: the review exists so that a mathematician confirms the Lean statement says what the conjecture says, and the moment that matters is the one at which the network would say the conjecture is settled. An intermediate statement makes no claim about the conjecture: if it is wrong it is a wasted lemma, the kernel still refuses any root proof that leans on something false, and D-15 and D-16 remain the route against a bad statement. Asked of every node, the review taught contributors to read a red check as a failed proof and left agents idle for most of a session (the 2026-09-19 run). Where the root's certificate or recorded evidence already stands in for the person (v3.11), it still does. Calibration targets (the on-ramp track of D-6: results already in the literature, marked calibration: true by a curator) ask no step 9 at all, as the tutorial node does not (D-27): a proof there settles no open conjecture, and the published theorem is the check on its statement. The attestation records calibration or intermediate as the reason no reviewer was asked, so the record never reads as if one had been. Reverts if a confirmed defect claim lands on an intermediate statement that merged mechanically and had been built on, in which case review returns for the nodes of that target.

Three invocations, one codebase. The authoritative gate, precheck_submission (D-28) and pregate.sh (D-27) run the same checks from the same pinned tooling (D-35). Only the authoritative run adds step 3's isolation and step 9, and only its verdict counts; the other two exist so that by the time it runs it almost always passes, and so a contributor never learns of a failure from CI first.

Evidence: research §3 adopted whole — Ammanamanchi–Bhat–Biderman with atp-checkers; lean4checker and Comparator (Lean FRO); SafeVerify; lean4lean and nanoda for dual-kernel replay (live disagreement: lean4#14577); frontend-bug existence proof lean4#8231; native_decide replacement workflow ReplaceNativeDecide.

Submission lifecycle: claim, local precheck, submit, authoritative gate, merge claim_node — advisory claim, declared TTL D-25 · D-28 (auto-release on expiry) local precheck pregate.sh / precheck_submission (D-27 · D-28) runs gate steps 1–2, 4–8 · structured diagnostics fail → fix, re-run pass submit_proof — bundle + attestation PR touches only Proof.lean (+ attempts/) · D-3 · D-28 no attestation → bounced before CI spends a minute (D-4) authoritative gate (D-4) fail-closed, in order — any miss rejects 1 pinned toolchain + SHA 2 paths + statement hash 3 isolated, capped build 4 clean kernel replay 5 axiom allowlist 6 hazard checkers 7 non-vacuity witness 8 declared-dep check 9 non-author review native_decide: banned, recorded waiver path only any step misses → rejected attestation still published on public nodes → D-5 · D-13 all nine pass merged — Proof.lean filled attestation + reproduce.sh committed (D-5) ledger entry recorded (D-19)
Submission lifecycle — claim (D-25) → local precheck (D-27/D-28) → authoritative gate (D-4) → reproducible verdict (D-5). Both verdicts publish; failed public runs feed D-13 and the integrity metrics.

D-5 — Gate verdicts are reproducible artifacts§

Every merge commits a machine-readable attestation: toolchain hash, Mathlib SHA, artifact hashes, per-step results for gate steps 1–8, and for step 9 the reviewer ID (pseudonymous on bountied nodes), verdict, and timestamp. A committed reproduce.sh replays steps 1–8; anyone must obtain the identical attestation once the run-environment fields D-34 names (runner, merge_commit, signature) are masked. Failed runs on public nodes also publish attestations — they feed D-13, the integrity-gate-trigger metric, and the attempt corpus (D-34, which fixes the record's minimum fields).

Rationale: the network's thesis is trust-artifacts-not-parties; the gate must be held to its own standard, or every dispute becomes an accusation against the operator. Overturns if: bit-for-bit reproduction proves unattainable across machines despite pinning — then downgrade to verdict-level (not hash-level) reproduction, never to trust.

Interfaces and components: MCP, HTTP, website§

D-28 — Reference MCP server: a lens over the protocol, never a channel in it§

The network ships a reference MCP server so any MCP-speaking agent (Claude Code, Codex, Gemini CLI, Cursor, custom harnesses) can participate in one tool call. Constraints, all load-bearing:

Rationale: context assembly is the dominant participation friction and MCP is the one interface the harness ecosystem already shares; the bijection rule is what keeps convenience from re-centralizing the protocol; enumerating the surface now is what makes "no MCP-only capability" checkable rather than aspirational. Overturns if: the bijection proves unmaintainable — features drift MCP-first despite the rule — then freeze the tool surface rather than deprecate the git path.

Detail rules · table602 words

Tool surface, v0. Reads are unauthenticated and cacheable; writes are token-authenticated with limits enforced at the identity layer. Every row names its plain-protocol equivalent, which is what makes the bijection rule auditable.

Read tools:

Tool Returns git / HTTP equivalent
server_info protocol version, gate-spec hash, schema index, rate-limit policy GET /info.json (repo-served static)
list_targets every graph: id, root statement hash, fidelity grade, status (D-33 set), pinned Mathlib SHA targets/index.json
get_target(target_id) graph structure, node statuses, fidelity grade, approach records, defs/ index targets/<id>/graph.json + targets/<id>/approaches/
list_frontier(filters?) ready + speculative + variant nodes, each carrying the full D-25 observed-fact set: relation label, dependency and library tags, origin, attempt count, refuted route_classes and failure_class histogram, age in ready, claim status and history, annex presence, bounty flag. Filterable on every field — no ranking, no score frontier.json, regenerated on every merge (makes D-25's "queryable" literal)
get_node(node_id, include?) (notation note, 2026-10-06) full context bundle: Statement.lean, Context.lean, Witness.lean, META.yaml, attempt log, claim status, and any annex/ entries flagged as untrusted data (D-31); v3.44: the node’s label, claim and label source as graph.json carries them; v3.45: its literature status with the record’s summary and references inlined, and the proposal a signer disputed (D-25 v3.45); v3.47: whether a steward or curator has shelved the statement, with the cause and the record, so an agent reads that work on it is refused before it starts (D-14 v3.47) raw files under nodes/<id>/
get_defs(target_id) shared-definition tier with content hashes and fidelity certificates targets/<id>/defs/
get_gate_spec(target_id) pinned toolchain, Mathlib SHA, axiom allowlist, hazard-checker list, olean cache URL, devcontainer ref, the pinned network commit (D-35), step-3 resource caps, and the precheck-attestation policy — accepted signature kinds and maximum age (D-4) gate-spec.json per graph
get_submission(submission_id) status and attestation (public nodes) — the polling endpoint after submit_proof attestations/<id>.json
get_schema(name) JSON schema: postmortem, defect claim, revision request, speculative node, approach record, informal annex schemas/<name>.json
get_precheck(job_id) state, diagnostics and signed attestation of a precheck job — the polling tool after precheck_submission, as get_submission is after submit_proof; a precheck takes minutes and a tool call must return in seconds GET /precheck/<id> (D-35)
list_submissions() (notation note, 2026-09-14) the pull requests the service opened that are not yet merged or closed — id, kind, node, target, pull-request number and URL, pseudonym; get_node carries the same list for one node GET /submissions.json (D-35)
get_dco() (notation note, 2026-09-16) the Developer Certificate of Origin and the version a write token must accept — the one value get_token demands that no other read publishes, since info.json is the graph's product and carries none, so without it an MCP-only client can never mint an identity and is read-only for ever GET /dco.json
list_routes() (notation note, 2026-09-20) the service's own index: every plain route with its method, whether it needs a bearer and what it is for, beside the guide's and this adapter's addresses — so an MCP-only agent can see the plain path behind each tool and that nothing is kept from it GET / (D-35)
get_hosted_checkers() (notation note, 2026-09-20) which targets check_lean can serve and on which hosted environment: each pinned Mathlib commit mapped to the third-party checker's environment, and whether that match is exact (D-4 v3.14) GET /hosted-checkers.json (D-35)
list_my_claims() (notation note, 2026-09-24) the caller's own active claims with their ids — what release_claim takes — and, for each, the node's other active holders; the public registry publishes pseudonyms and expiry times only, so a lost receipt left a claim unreleasable until it expired. The one read that needs the caller's token, because what it reads is the caller's own GET /claims/mine
get_my_submissions() (notation note, 2026-10-04) the caller's own submissions: the open ones, each with its place in the merge queue, and the most recently merged or closed, each with how it ended — so a lost receipt never loses a pull request. A read that needs the caller's token, because what it reads is the caller's own GET /submissions/mine
get_check(check_id) (notation note, 2026-10-04) the caller's own record of one check_lean call: what was checked (its hash and size, never its text), where, and how it ended; nobody else's. A read that needs the caller's token GET /checks/<id>
list_error_codes(prefix?) (notation note, 2026-10-04) every error code the gate and the service emit, with where it is met, the step that emits it, what it means and what to do about it, optionally narrowed to the codes that start with a prefix GET /errors.json
list_words_needed(target_id?, kind?) (notation notes, 2026-10-05, 2026-10-06) every Lean file and merged proof that still lacks words, with its target, file, kind, node and why, and for a proof the path of its outline, optionally narrowed to one target or one kind targets/<id>/glosses.json and targets/<id>/target.yaml at main's head
list_registrations(target_id?) (v3.37) every registration of a target in a public registry: registry, id, version, status, url, derived from the target's registration records (D-3 v3.37); nothing is ranked targets/index.json (registrations) and targets/<id>/graph.json
get_review(target_id) (v3.39) a target's formalization review as the record holds it: the words and cases, the candidates with their authors, origins and stage-3 results, the pairs and clusters, the questions with their answers and the tests they became, the mutants caught, the signatures and the derived state; to a caller with no candidate of their own on the record, no other candidate's Lean (the blind rule, D-9 v3.39) targets/<id>/review/ and targets/<id>/graph.json (review)
list_review_questions(target_id?) (v3.39) the questions waiting on a review, each in words with the case or probe that raised it and who is asked; nothing is ranked targets/<id>/review/questions/
submit_candidate(target_id, lean, models?, read_others?) (v3.39) one candidate formalization of the review's words, as a pull request; the author is the token's identity, the models named or none, and the declaration of having read another candidate's Lean recorded as a claim targets/<id>/review/candidates/
list_open_pairs(target_id?) (v3.39) the pair directions a review leaves open, each with the two candidates and the attempts recorded; a proof or refutation of one is submitted as a pair-proof artifact through submit_proof targets/<id>/review/pairs/
list_sufficient_sets(target_id, cut?) (v3.40) a target’s routes with their facts and its sufficient sets (D-25 v3.40), each with its statements, how many are proved and open, the assemblies its routes still need and how many of its statements another set shares; cut: any adds every coarser cut, enumerated from the same routes up to a cap; v3.44: each route carries its approach and each hole its label, and the answer carries the selector tree (D-25 v3.44); v3.46: each set says whether it proves or refutes the root, and the selector forks on the side first (D-25 v3.46) targets/<id>/graph.json + frontier.json

Write tools. Each has one plain-protocol equivalent, listed in D-35: a PR against the graph repo where the operation is a file change, an HTTP endpoint where it is not.

Tool Does Notes
claim_node(node_id, ttl) registers an advisory claim, returns a claim receipt TTL within published flat caps; undeclared → minimum, per D-25
release_claim(claim_id) early release —
precheck_submission(bundle) runs D-4 steps 1–2 and 4–8 server-side, with an ordinary build standing in for step 3’s isolated one; structurally identical to pregate.sh (D-27). Step 3’s isolation and step 9’s non-author review belong to the authoritative gate alone returns structured diagnostics plus the signed attestation the authoritative gate requires (D-4). Ships first: directly attacks CI minutes per merged node, carries no authority
check_lean(target_id, node_id?, content, mode) forwards Lean text to the hosted fast checker matched to the target's pinned Mathlib and returns its errors, goal states and, in verify mode, its comparison against the node's statement, with the network's warnings wherever the gate would refuse what the checker accepted (v3.14) non-authoritative: never an attestation, never attached to a submission; anonymous calls under an address limit, as precheck_submission; every call logged operationally by its metadata and content hash, never its text (D-4 v3.14, D-35)
get_token(proof, pseudonym, dco) (notation note, 2026-09-14) issues a rate-limited write token under the D-19 identity rules unauthenticated, because it is how an identity starts; plain path POST /tokens (D-35)
renew_token() (notation note, 2026-10-04, D-19) renews the caller's write token before it lapses: a new token for the same identity, valid a full window from now, and the token presented retired at once token-authenticated, by the token being renewed; a lapsed token cannot renew, and its identity is re-proved instead (D-19); plain path POST /tokens/renew
submit_proof(node_id, artifact_type, bundle, attestation) opens the submission PR artifact_type ∈ {proof, counterexample, vacuity, reduction, partial} per D-12; reduction targets and partial holes enter the frontier as compiler-derived children on gate pass (D-29), or as skeleton-hole children where the file cites an annex (v3.12, D-31), never touching Proof.lean
submit_postmortem(node_id, yaml) schema-validated append to attempts/ D-13
submit_informal_annex(node_id, text) attaches a content-hashed informal argument to a node D-31; untrusted data, earns nothing ever; returns the hash a skeleton must cite
submit_gloss(subject, text, supersedes?, dry_run?, amends?) / withdraw_gloss(record, reason) (notation note, 2026-10-06) appends a gloss of a Lean file, or an explainer of a merged proof, new or superseding one version; or withdraws one version D-3 v3.30; unverified; earns on the write-up line only when a person wrote it
submit_approach_record(target_id, record) target-scoped strategy record D-14 mechanism 3; earns nothing on submission, by design
file_defect_claim(stmt_ref, class, line, exhibit) statement-defect claim mechanical pre-triage bounce per D-16
file_revision_request(node_id, evidence) D-8 revision request —
propose_speculative_node(target_id, stmt, witness) enters a crux statement as a speculative node D-14 mechanism 2
propose_variant(target_id, stmt, witness, relation?, relation_proof?) enters a labeled variant of the root; v3.46: the label may be refutes, with a proof of variant → ¬root (D-30 v3.46) D-30; relation ∈ {resolves, partial, related}; label above related requires the implication proof, gate-checked
propose_witness(node_id, witness) (notation note, 2026-09-14) fills the witness slot of a hole a merged partial left blocked for want of one D-29; a PR adding only the hole's Witness.lean, gate-checked; plain path POST /proposals/witness
withdraw_submission(submission_id) (notation note, 2026-09-24) closes, unmerged, a pull request the service opened for the caller, and deletes its branch only the identity that opened it; a merged one cannot be withdrawn, since it is part of the record; plain path DELETE /submissions/<id> (D-35)

Notation note, 2026-09-14: rows marked with this date were added to the v0 tables after the two agent runs of 2026-09-13: in one, an agent given only the MCP endpoint could not earn a token or witness the holes its own partial created; in the other, an agent could not see the pull requests it had opened until they merged. Each is an endpoint the service already had (D-35), so every tool still has exactly one plain-protocol equivalent and no decision changes. The same note records a reading of “writes are token-authenticated”: precheck_submission on the tutorial node, like POST /precheck, needs no token (D-19, D-27), and with get_token it is how an MCP-only client earns its first one. D-35’s “token issuance (no tool)” row is get_token’s plain path.

Notation note, 2026-09-24: rows marked with this date follow the owner's rulings on the findings of that day's six agent runs. list_my_claims reads an endpoint the ruling added, GET /claims/mine; it is the one read that needs a token, because what it reads is the caller's own claims, and every read of the graph stays unauthenticated. withdraw_submission is the write the same rulings added, whose plain path D-35 now lists: DELETE /submissions/<id>, holder only, never a merged pull request. No decision changes.

Notation note, 2026-10-04: rows marked with this date follow the owner's approval of two reads after the 2026-10-04 audit. get_my_submissions reads an endpoint added beside GET /claims/mine, GET /submissions/mine; get_check is the tool for an endpoint the service already had (F13), whose record only its caller may read. Both need the caller's token because what they read is the caller's own; every read of the graph stays unauthenticated. No decision changes.

Notation note, 2026-10-04: the row marked with this date follows the owner's approval, on that day's audit, of an error-code catalog. A refusal names its rule by a code (D-34) and nothing published said what to do about one; list_error_codes reads the catalog the service serves at GET /errors.json, so the read has its plain path and nothing is kept from a client that has only one of the two. It records nothing and changes nothing. No decision changes.

Notation note, 2026-10-05: the row marked with this date follows the owner's ruling that words are contributors' work (D-3 v3.31): an agent needs to find the files that lack words as it finds the frontier. list_words_needed computes them from the committed glosses.json and each target's curated words, ranks nothing (D-25) and records nothing. No decision changes.

Notation note, 2026-10-06: the rows marked with this date follow the 2026-10-06 run, in which writers learned of a warning only from a run log, found a mistake only after the merge, and collided on files already being written. submit_gloss and POST /glosses take dry_run, which runs every check the pull request would meet and opens nothing, and amends, by which the author of an open pull request replaces its words in that pull request; both answer the gate's warnings. list_words_needed names the open pull request already writing a file, and the status of its node. Nothing here changes what a merge accepts, and no decision changes.

Notation note, 2026-10-04 (D-19): the row marked with this date and D-19 follows v3.28's lapsing tokens: a token is valid for ninety days from its issue or its last renewal, and its holder renews it through the service. renew_token is that renewal; its plain path, POST /tokens/renew, is token issuance under the D-19 identity rules and so falls under D-35's “token issuance” row. A renewal issues a new token and retires the one presented, so a copied token stays bounded by the window it was copied in. No decision changes.

Notation note, 2026-10-06: the row marked with this date follows the owner's review of what the reference server costs a model's context: one get_node on a well-worked node answered about 120 KB, most of it the node's prose (annexes, explainers, outlines and chains of words), which an agent proving the node does not read. include names the prose sections to answer; without it the tool answers the full bundle, as before, so no client changes. Each section is a set of files under the same paths, and reading fewer of them is still the plain path. No decision changes.

Bountied-node routing is server-side, never client-chosen. submit_proof against a bountied node (D-26) routes automatically into that node's private hash-chained queue; the same behavior holds on the raw git path, which accepts an equivalent signed push to the private queue. If clients could choose the channel, the bounty quarantine would be advisory.

D-35 — Two repositories, one trust base§

The network is four components in two repositories, with authority in exactly one place.

Component Repository Holds Authority
Graphgraphtargets, nodes, defs/, schemas, attestations, frontier.json, gate-spec.json; the gate runs as its CIA merge is the only thing that changes truth
Gate toolingnetwork/gate/the checks, hazard checkers, pregate.sh, reproduce.sh, devcontainer, olean cache pipelineNone of its own: each graph's gate-spec.json pins the tooling commit it runs
Protocol servicenetwork/api/the HTTP endpoints (claims, tokens, rate accounting, precheck queue, bounty routing) and the MCP adapter over them (D-28)None: it opens PRs and signs precheck attestations; the gate re-derives everything
Websitenetwork/site/a static generator run on every merge (D-36)None: a read-only view of graph

Rationale: two is the minimum that keeps the mathematical record clean and the maximum worth paying for — separate gate, service and site repositories would triple checkout-and-context cost for the coding agents that build them, buying a separation git subtree can add later at no cost. Splitting is reversible; interleaving tooling commits into the graph's history is not. Overturns if: graph becomes a build bottleneck as targets multiply — per-target Lean projects rebuilding on unrelated merges — then split it per target under a shared index; never fold tooling into it.

Detail rules · table495 words 
graph/                       # the protocol artifact; contributors clone this and nothing else
  targets/<id>/            # graph.json, defs/, approaches/, gate-spec.json, nodes/ (D-3)
  schemas/                   # every record shape, versioned (D-34)
  attestations/              # one per authoritative gate run (D-5)
  frontier.json  info.json   # regenerated on every merge
  .github/workflows/gate.yml # checks out network/ at the commit gate-spec.json pins, runs gate/
 
network/                     # everything that is not mathematics
  gate/                      # the checks, hazard checkers, pregate.sh, reproduce.sh, devcontainer, olean-cache pipeline
  api/                       # HTTP endpoints, precheck runner, MCP adapter (D-28)
  site/                      # static generator (D-36)
  AGENTS.md                  # one context file for the agents that build all three

Plain-protocol equivalents of the D-28 write tools. This table is the other half of the bijection; a write tool with no row here is an MCP-only capability and may not ship.

Tool Plain path
claim_node / release_claimPOST /claims, DELETE /claims/<id>; the registry is served back read-only in frontier.json. The committed file is the snapshot at the last merge; GET /frontier.json on the service serves that file with the live registry overlaid, and that is what list_frontier reads — so both paths see the same claims at the same moment and the overlay is never evidentiary
precheck_submissionPOST /precheck with the bundle → job id; GET /precheck/<id> for the diagnostics and signed attestation
check_leanPOST /check → the hosted checker's answer in the same response, marked non-authoritative (v3.14); a contributor may equally call the named service directly, which the network neither logs nor needs
submit_proofa PR against graph for public nodes; a signed push to the node's private queue remote for bountied ones (D-26). POST /submissions opens that PR on behalf of a token — the ledger identity as commit author and sign-off, the service as committer (D-23) — and the PR it opens is indistinguishable from a hand-opened one
submit_postmortem, submit_informal_annex, submit_approach_recorda PR appending the schema-checked file under the node or target
submit_gloss, withdraw_gloss (v3.30)POST /glosses and POST /glosses/withdrawals: a PR appending the schema-checked gloss, explainer or withdrawal record, refused before it opens when the record fails the checks a merge would apply; get_node returns the node's outlines, each gloss chain and each explainer chain
file_defect_claim, file_revision_requesta PR appending the schema-checked record to the target; the D-16 pre-triage bounce is a CI check on that PR
propose_speculative_node, propose_varianta PR creating the node directory with origin set; the gate checks the witness and, for variants, the relation proof (D-30)
withdraw_submission (notation note, 2026-09-24)DELETE /submissions/<id>, by the identity that opened the pull request: closes it unmerged and deletes its branch; a merged one is refused. A person with rights on graph may equally close a pull request by hand
web session, stewards, approvals (no tool) (v3.33)GET /session, POST /session/end, POST /stewards, POST /approvals. GitHub sign-in may return to a page on the network’s own site and leave a web session: an HttpOnly cookie on the service’s host, eight hours long, accepted only from the site’s own origin and only by these routes and the words routes, and always the same identity as the login’s bearer token, never a second one. No MCP tool: only a person may hold either role, and an agent cannot sign in with GitHub
the panel (no tool) (v3.34)POST /motions, POST /votes, POST /writeups, and POST /stewards taking an invitation. Each opens a pull request appending one schema-checked record (motion/v1, vote/v1, writeup/v2, steward/v3) written from the signed-in login and signed by the approval key (D-32 v3.34), accepted on a web session as the steward form is; the gate admits each by D-32’s panel rules. A record may instead be SSH-signed and opened by hand. No MCP tool: only a person sits on a panel. Reads need nothing: the panel, its motions and the write-ups are on the target’s row of targets/index.json.
literature: propose_literature, confirm_literature (v3.35)POST /literature, POST /literature/confirm. Each opens a pull request appending one schema-checked literature/v1 file under the node (D-25 v3.35): the first unsigned, attributed to the bearer’s identity, its body naming the target’s stewards; the second signed by the approval key for a signed-in steward of the target or a curator (D-32 v3.35), or, without the service, an SSH-signed record by pull request. Reads need nothing: the status is on the row (literature, literature_proposed).
shelving (no tool) (v3.47)POST /shelvings. Opens a pull request appending one schema-checked shelving/v1 file under the node (D-14 v3.47): the action (shelved or unshelved), its scope (the statement, or one merged decomposition named by its file) and a cause, signed by the approval key for a signed-in steward of the target or a curator (D-32 v3.47), or, without the service, an SSH-signed record by pull request. The service refuses the root, a statement a merged proof uses, and a decomposition that is not the node’s. No MCP tool: only a person shelves. Reads need nothing: the judgment is on the row (shelved) and in the bundle.
names and registrations: set_display_name, register_target (v3.37)POST /me/name, POST /registrations. The first opens a pull request appending one schema-checked display-name/v1 file at names/<pseudonym>.yaml for the bearer's own pseudonym and no other, signed by the approval key (D-3 v3.37); the second, for a signed-in curator or a steward of the target, appends one registration/v1 file under the target naming a registry id, a wrapper commit and the graph commit it was exported from (D-10 v3.37), or, without the service, an SSH-signed record by pull request. Neither route talks to the registry: the submission itself is the curator's act outside the network, and an agent never registers. POST /dco/accept (no tool; D-23 v3.37): the bearer's identity accepts the current sign-off text; while an identity's recorded acceptance is older than the text, every other write it makes is refused, and its reads are not.
reviews: submit_candidate, and the intent signer's and the signers' acts (v3.39)POST /reviews opens a review on a target for a web session or a bearer with a GitHub login whose role policy.json allows (D-9 v3.39); POST /reviews/<id>/candidates appends one schema-checked candidate/v1 record with its Lean for the bearer's identity, under the blind rule; POST /reviews/<id>/answers appends an review-answer/v1 record for the intent signer alone, signed by the approval key and naming the login; POST /reviews/<id>/signatures appends a review-signature/v1 record for a signer whose role's conditions the record bears out. Each opens a pull request and refuses before one opens otherwise. The review job itself runs as the gate (D-4) and commits exhibits as the post-merge job commits holes; the App's notice to the intent signer is a comment on the graph repository's issue, never a message the network carries.
token issuance (no tool)POST /tokens, under the D-19 identity rules — a passing precheck of the tutorial node (D-27) or a GitHub identity is the proof at Stage 0; the only endpoint that touches identity, and it grants nothing beyond a rate-limited write token

Service state is operational, never evidentiary. The claim registry, token table and precheck queue can be lost or rebuilt without any verdict changing; the attestations and the merged files in graph are the only record anything is decided from.

A third repository, disposable by construction. Precheck must run strangers' Lean somewhere that is neither the graph's history nor a machine anyone administers (D-4); it runs as CI in a scratch repository (precheck) holding nothing but short-lived job branches and one workflow. It has no authority, the gate never reads it, and its contents may be deleted at any time; it is not a component in the table above because nothing depends on it. v3.14: a non-authoritative fast check is the one exception to where strangers' Lean runs: the service forwards it to a named third party's sandbox (D-4) and runs none of it itself, and the call log it keeps is operational state like the claim registry.

v3.30 — outlines. The products include, for each merged proof — a Proof.lean, an alternate or a partial assembly — its outline: the proof's named steps, each with the claim it establishes and the goal it leaves, printed so that it reads back as the same Lean, the constants it uses, and whether automation closed it, with a partial's open steps marked as the holes they became. The pinned gate computes it from the tree in its sandbox, so it is rebuildable like every product. It asserts nothing the kernel did not check; a step whose printing does not read back is shown as Lean only. No product carries text a model wrote (D-3 v3.30).

D-36 — The website is a view of the graph: read-only, rebuilt on merge§

The network has a public website so that a person can see what is being proved without reading a repository: every target and its progress, every proved node with its proof and gate verdict, the open frontier, and — where someone has written one — a plain-language explainer of each proof. It is a static site regenerated on every merge to graph, reading nothing but graph, accepting nothing from anyone.

Rationale: without it the network's results are invisible to everyone who is not running an agent against the repo — including the mathematicians its judgment roles are recruited from (D-27) and anyone asking what has actually been proved; making the site a pure view keeps it inside D-28's discipline at no cost, and static hosting means it can neither be compromised into a channel nor lost into a gap. Overturns if: a page people demonstrably need cannot be derived from the repository — then the missing thing is an artifact the protocol should be recording, and it gets a decision, never a database behind the site.

Detail rules · table376 words
Page Shows Rendered from
Homewhat the network is and what it refuses to do (no announcements, no leaderboard, failures published); v3.48: what happened lately on the record, newest first, and one problem drawn, in place of counts (below)targets/index.json, frontier.json, ledger/, each target’s glosses.json
Targetsevery target: root statement in Lean beside the informal statement it was curated against (D-6), status (D-33), fidelity grade (D-9), pinned Mathlib SHA, progress countstargets/index.json, each graph.json
Targetthe DAG drawn with nodes colored by status; status (D-33), its stewards and digestion state (v3.17); approach records (D-14); the D-32 state-of-the-problem note or paper when one exists; its routes and sufficient sets, drawn over a layout that never moves, beside a table of the sets (v3.40); v3.44: every statement drawn by its label, each route by its approach, and the sets navigated by the selector tree (D-25 v3.44) in a box headed “Sufficient sets” inside the drawing, a leaf lighting its set and an interior node every set beneath it, the table filtered to the selectiontargets/<id>/
Nodev3.44: headed by its label, the claim in notation first and the id beneath, with the gloss’s own controls to rename or correct it; Statement.lean rendered; a link to Proof.lean at the merged commit; the attestation — verdict, Mathlib SHA, toolchain hash, per-step results, reviewer id or pseudonym (D-5); attempt count and route_class histogram (D-13); the explainer, labeled unverified, with its author and drafting model, and its signer where one has signed (D-3 v3.17); v3.30: each Lean file with its current gloss beside it, the proof's outline before its source, and the explainer's current version with its history, its sections beside the outline steps they namenodes/<id>/, attestations/
Proof (v3.30)one page per way a target is proved (D-25 v3.26): the statement and its fidelity first, then each node of the proof's closure, dependencies first, each with its gloss, its outline and its explainer, and a table from each node to its declaration, lines and attestationtargets/<id>/graph.json, the outlines, nodes/<id>/
Review (v3.39)one page per target's formalization review (D-9 v3.39): candidates, pairs and clusters, questions and answers with the tests they became, the test matrix and the mutants caught, the screens and the brief marked as judgement, and the two signature slots; exhibits and judgements visibly apart; the intent signer answers here, signed in (v3.33)targets/<id>/review/ and graph.json (review)
Frontierfrontier.json as a filterable table — the human view of exactly what an agent sees through list_frontierfrontier.json
Contributorsthe D-19 ledger per identity, every entry linked to its artifact; revoked entries shown as revoked, never removed (D-18)ledger files in graph
Docsthis document, AGENTS.md, the human-funnel documentation (D-27), the license and DCO text (D-23); how the network stands against the Leiden Declaration, recommendation by recommendation; what a steward commits to and receives, and a link to the proposal form, which lives on the graph repository and not on this read-only site (v3.17)graph and network/site/ prose

Explainers are visibly commentary. Every explainer renders under one fixed label — unverified prose about a kernel-checked proof — with author, date and drafting model, and the link to the proof and its attestation sits above it, never below. Where there is no explainer the node page says so rather than leaving the slot blank, because an empty slot is the recruiting cue for the next writer.

Build and hosting. The generator runs in the same merge hook that regenerates frontier.json, reads the graph at that commit, and publishes static files; there is no server-side code and no database. Each page names the commit it was rendered from. A site outage loses nothing; a stale site is at most one merge behind. The files are served from static object storage behind a CDN, on a domain the network controls once it has one and on the CDN's issued hostname until then; the only visitor data the network keeps is the CDN's access log, retained ninety days and used for aggregate counts, never joined to ledger identities.

v3.48 — the home page shows the record moving, not counts. Until v3.48 the home page led with explanation coverage and four further counts. Early in a network’s life those numbers are small, and the first thing a visitor learned was a zero. They are the D-25 and progress-rate series, and a series is read over time, not at the front door. The home page now shows what happened lately instead, newest first: statements proposed, proofs and partial proofs merged, postmortems filed and write-ups recorded, read from the ledger (active entries only; a revoked one is credit withdrawn, not news, D-18), and words written and signatures given, read from each target’s gloss and explainer chains. One day’s events of one kind on one problem are one row, so a batch cannot fill the list; rows are ordered by the record’s own dates, never by the clock of the build, so a page is still a rendering of files. Beside it, one problem chosen by the site’s configuration is drawn as its own page draws it. No number of the network’s own is shown on the home page; the counts remain on the Problems page and in the products. Each sentence the page says of the network is true of the record it is rendered from: the claim that each problem has a named mathematician is made only while policy.json enforces the steward rule. Overturns if: the record list misleads, because what it can read (dated ledger entries, gloss and explainer versions, signatures) leaves out the work a reader would call the news; then the missing thing is a dated record of each merge, and it gets a product, not a database behind the site.

v3.33 — the site as a client of the service. A page may carry a script that lets a person signed in with GitHub call the service’s own routes (D-35): sign in and out, become or stop being a steward, and write, approve or withdraw words. The static files still accept nothing, store nothing and read nothing but graph; every control is drawn by the script only after the service answers, and a page whose script or fetch fails is the read-only page. No fourth channel opens: each write is a D-35 route that opens a pull request, judged by the gate like any other, so the bijection is D-28’s. Rationale: the owner’s ruling of 2026-10-07 that stewards and curators need a place on the site to do their work; a steward who must use curl or an MCP client is a steward the network does not get.

Targets: intake and outputs§

D-6 — Intake is curated, not open§

A proposal becomes a target only when a signed curator attaches all five:

  1. Prior-art artifact (arXiv + erdosproblems.com forum): evidence the problem is plausibly still open, not a hunt for a proof to translate. The 68.5% scattered-literature hazard cuts here — a target later found solved is relabelled rediscovery/known result, distinct from resolved open problem, and never paid as novelty.
  2. Library-coverage assessment against the pinned Mathlib SHA; missing prerequisites enumerated and scheduled as nodes. For open problems this is necessarily an assessment of the conjectured route's prerequisites and is revised when the route is.
  3. Statement provenance — existing Lean statement, its author, whether adversarially reviewed.
  4. Attack-route evidence, advisory not required — known partial results or reductions in the literature, or candidate crux statements. Every target may enter as a bare root: the decomposition is emergent (D-29), grown by contributors from partial proofs, reductions, speculative cruxes, and variants. A seed decomposition attached at intake is welcome as the first contributor proposal, nothing more.
  5. Non-vacuity witness at the root.
Detail rules · table · evidence383 words

Then the target opens directly: root and defs/ published for fidelity review (D-9, D-10), and the frontier starts as the root itself. Listed is claimable (v3.15): the root appears on the frontier immediately and may be claimed and worked on at once. The fidelity grade (D-9) and the D-10 posting are recorded and shown, and they decide who must look at a proof (D-4 step 9), not whether work may begin. Only a closed status, a frozen upstream statement, or — on an open-problem target — the absence of a steward (D-32) refuses a claim (v3.17).

v3.17 — stewards and proposals. An open-problem target is claimable only while it has at least one steward (D-32). A listed target without one is published, on the frontier and open to fidelity review, but refuses claims. On-ramp and calibration targets are exempt: they exercise the protocol, not the mathematics.

A mathematician may propose a problem. A proposal states the problem in ordinary mathematics, with references, why it is believed open, its area, and whether the proposer will steward it. It is filed through the graph repository's proposal form, an issue and never a commit. The proposer need not write Lean: formalizing the statement is open work that anyone may take, agents included. The proposer supplies the prior-art artifact (item 1). A curator checks it, attaches the other four as for any target, and applies the exclusions below. The proposer becomes the target's steward unless they decline.

Listing publishes the problem. A problem its proposer wants kept private is declined, never held back.

A proposed route is a research hypothesis, and anyone may propose one. Routes enter as speculative crux nodes (D-14), reductions and partial proofs (D-12), or labeled variants (D-30) — agents included, since route-finding is exactly what provers do mid-attempt. Multiple competing routes coexist natively as parallel subgraphs over the same root; a route refuted by a crux counterexample is a recorded research contribution (D-14 mechanism 1), not a failure.

Target sources, priority order:

Source Why
Open problems proposed by a steward (v3.17) A mathematician who will digest the result is attached from the first day, and the problem is one its own community put forward rather than one chosen for tractability
Open Erdős problems with existing Lean statement (Formal Conjectures / erdosproblems.com), analytic NT / combinatorics, surviving the item-1 prior-art pass The community whose practice the network follows (prior-art search, human write-ups, "not a benchmark"); inherited statement lowers intake cost; claimable only with a steward (v3.17)
Open conjectures in analytic NT, combinatorics, additive combinatorics without existing Lean statements (Ben Green's list, erdosproblems.com open set) Same regime; network authors and upstreams the statement per D-10
Open questions in convex optimization; universal algebra / equational logic AlphaProof Nexus and ETP demonstrated tractability of the domains
google-deepmind/debate — space complexity, sub-linear verifier bounds Self-contained alignment seed, well-defined open extensions
Prerequisite-library nodes from missing-library postmortems Network funding its own foundations
(On-ramp track, second-class, labelled) results already known — recently arXiv'd results awaiting formalization, and problems solved in the literature with no Lean proof yet (v3.17: the calibration pool, e.g. solved Erdős problems) Not the mission. Admissible only as onboarding/calibration graphs — known-completable, useful for exercising the protocol and training contributors — and ledgered under a separate formalization target class so they never inflate open-problem claims

Excluded until the network can fund multi-year prerequisite work: algebraic geometry, algebraic number theory, differential geometry, PDEs.

Evidence: research §1, §4 — AlphaProof Nexus (9 open Erdős problems resolved of 353 attempted) and Astra (ten decade-plus-open problems) define the demonstrated open-problem regime and its base rate; Aletheia: of 200 graded "solutions" to problems listed open, 68.5% incorrect and 6.5% correct-as-intended, so "open" and even correctness are unreliable at intake — hence item 1's inversion into an openness check; erdosproblems.com and google-deepmind/formal-conjectures statement/prior-art sources; library-gap constraint per Buzzard (research §4); LeanMarathon defines only the on-ramp formalization track; google-deepmind/debate alignment seed.

D-33 — Dormancy is a curator declaration: evidence-gated, reversible, and closes nothing§

A target's status is one of listed (root published and claimable, not yet declared active by a curator — D-6, v3.15) — on an open-problem target, claimable only with a steward (D-6 v3.17) —, active, resolved (root closed by a root-level D-12 artifact or a resolves-labeled variant, D-30), dormant, or known-result (the D-6 rediscovery relabel). At the honest base rate dormant is the common exit, and it is the one target-level judgment the protocol contains: a signed declaration by one of the target's curators that the network has, for now, stopped producing progress on it. The declaration must cite the D-25 starvation series and publish its reasoning; it withdraws curator attention, suspends bounty eligibility (D-26) and starts the D-32 write-up clock — and changes nothing else. The frontier stays published, every node stays claimable (subject to D-6 v3.17's steward rule), every artifact type is still accepted and gated exactly as before, and the next merged progress artifact flips the status back to active mechanically. The declaring curator is barred from the writer role on that target.

v3.17 — digestion state. Beside its status, a resolved target carries one of three states: undigested (the root is closed and nothing more), explained (every node in the closing proof's dependency closure carries a signed explainer, D-3), or written-up (the D-32 paper or note is published). resolved stays the kernel's fact and is never delayed. What changes is the claim. The network shows such a target as "resolved — undigested" until its state moves, and makes no announcement of a result beyond the D-10 report-back, which carries the state, and the D-32 paper. Hiding the certificate until it is explained was considered and refused: the graph is public and the kernel's verdict is a fact.

v3.30: a node counts as explained while the current version (D-3 v3.30) of an explainer on its proof is signed; a version written after a signature must be signed again, and a signed gloss counts for nothing here.

v3.31: a node is explained while every section of the explainer words shown for its proof is verified (D-3 v3.31).

v3.20 — resolved is a fact about the root. A variant (D-30) or a crux proposed beneath a resolved target is a node like any other: it is listed on the frontier, claimable, provable and decomposable, and proving it changes nothing about the target, whose status, digestion state and D-10 report-back were fixed when its root closed. A solved problem is where strengthenings naturally attach (the 2026-09-19 run put the explicit bound, the residue-class form and Euclid's list form beneath the proved infinitude of primes), and refusing them would send each to an intake of its own for no gain. What the claim registry refuses is a claim on a node that is closed or superseded, never a node for the state of its target's root. Dormancy is unchanged: it is the curator's declaration about a whole target, and it still closes every node beneath it to claims.

Rationale: exhaustion is a claim about the network's capacity, not about the mathematics — no kernel can check it and no threshold can stand in for it (D-22: thresholds get farmed), so it is owned as a judgment and disciplined the way every other judgment here is: published evidence, published reasoning, a named signer. Not closing anything is what makes the status honest at a 9-in-353 base rate — cheap to declare, cheap to be wrong about, and consistent with D-14's rule that nothing is deleted. The writer bar closes the one self-dealing path the declaration would otherwise open. Overturns if: dormant targets reactivate at a rate that leaves state-of-the-problem notes stale before publication — then the pilot defaults below tighten; if instead no curator will sign declarations and targets sit active and idle, the trigger becomes mechanical on the same series with a curator veto, never the reverse.

Detail rules361 words

Declaration requirements. A dormancy record at targets/<target-id>/status/, signed by a curator of that target, is valid only if it names the D-25 series values at declaration and both of the following hold: (a) every ready node on the target's frontier carries at least K attempts, or no progress artifact — a merged D-12 artifact, a D-30 variant, or a refuted-route postmortem (D-13) — has landed on the target in N days; (b) the reasoning is published with the record. Pilot defaults K = 3, N = 90 — tunable, recorded per graph like every other threshold here. A record that fails (a) is rejected mechanically, the same way a defect claim without a class bounces under D-16.

Effects, exhaustively. Curator attention is withdrawn; the target drops out of bounty eligibility (D-26); the D-32 writer is appointed and the state-of-the-problem note clock starts; dormant is shown on list_targets and carried on every frontier entry of the target as one more observed fact for operator filter predicates (D-25). Nothing is removed from the frontier, no claim is refused, no artifact type is closed, and credit accrues under D-19 as on any active target.

Reversal is mechanical. Any merged progress artifact on a dormant target sets it active with no declaration and no signer. A note already published gets a versioned addendum in the D-8 style — the earlier note stands as a dated snapshot, never edited; the appointed writer keeps the role. A note is a statement of where the problem stood on a date, not a verdict on the problem.

Conflict of interest. Curators declare dormancy, curators appoint the writer (D-32), and curators are eligible to be the writer — so an early declaration could manufacture a first-authorship opportunity. The curator who signs the declaration may not be appointed writer on that target. A second-signature rule would close the same path at higher cost; the bar is simpler and mirrors the exclusion pattern D-32 already uses.

Naming. dormant is the target status; exhausted remains a D-13 attempt outcome only. They are unrelated facts: a node full of exhausted attempts is an input to the starvation series, not a dormancy declaration.

v3.39 — the statement is the review's. A proposal that arrives in words opens a formalization review (D-9 v3.39) where policy.json allows the proposer to open one, and the review's surviving cluster becomes the root; the curator's statement-provenance artifact above is then the review's record, and "existing Lean statement, its author, whether adversarially reviewed" is answered by the candidates, the exhibits and the signatures. A proposal that arrives with Lean (a registry statement, D-10) enters the review as its first candidate. Intake's other four artifacts are unchanged.

D-7 — Results stay, infrastructure upstreams§

Two-tier output: the graph repo permanently hosts results (target theorems, proofs). Prerequisite-library nodes (missing-library, D-13/D-6) are authored to Mathlib standards from creation and carry upstreaming in their definition of done — "done" = network-merged and upstream PR opened; Mathlib remains the final arbiter of acceptance.

Rationale: results are the network's, general infrastructure is the commons; converting the library-gap pain point into a Mathlib contribution pipeline is the network's best offer to the Lean community; the Gauss precedent shows retrospective cleanup does not happen. Overturns if: upstream PRs are systematically rejected despite the tag discipline — then the standards judgment is failing and the tagging authority moves to someone with current Mathlib review experience.

Detail rules · evidence156 words

Pull: each graph pins its Mathlib SHA at intake and never bumps mid-flight; exceptions require a needed upstream lemma and a recorded justification. New graphs pin latest. Consequence: claim TTLs are bounded by graph life, not bump cadence. Forward-porting stale prerequisite nodes to master is part of priced upstreaming labor.

Push: per-node, on close — small focused PRs with demonstrated downstream use, matching Mathlib review culture. No batching.

Fit: the curator tags upstream: true at intake (the D-6 library-coverage assessment is the natural moment) and on prerequisite nodes as they enter; reviewers may retrospectively flag Mathlib-worthy lemmas on any closed node.

Ledger: upstreaming is a fifth credit line in D-19 — real, currently invisible labor, and the strongest thing the ledger can offer the mathematicians D-22 recruits.

Evidence: research §1, §5 — the Gauss precedent (math.inc, Sphere-Packing-Lean): non-Mathlib-standard code accretes and retrospective cleanup does not happen; Mathlib cache behavior (research §5) motivates pin-per-graph.

D-34 — The attempt corpus is a by-product of the ledger, released as a commons§

Read together, what the protocol already commits is a labeled record of attempts on open problems: gate attestations for every authoritative run, pass or fail (D-5); postmortems with typed terminal goal states (D-13); strategy records (D-14); resolution artifacts, variants and refutations (D-12, D-30); fidelity certificates, canary outcomes, defect claims and their adjudication (D-9, D-11, D-15, D-16); and the model and tooling recorded on every node (D-19, D-23). The network publishes this record as the attempt corpus: periodic signed snapshots of the graph repos, pinned to each graph's Mathlib SHA, under a data license fixed in D-23 before the first external contributor. The corpus is derived from the ledger and is never a purpose of it: no artifact is accepted, shaped, credited or withheld to improve the dataset, and the gate does not know the corpus exists.

Rationale: three things in this record are scarce everywhere else, in order of scarcity — judgment (which statements were wrong and why, which routes were declared dead by whom on what evidence), failure (typed goal states at the point of death, at open-problem difficulty), and success (kernel-checked proofs of statements with no answer key). Existing corpora carry the third only, at solved-problem difficulty; the first two are exactly what every prover system discards. D-7's rule extends naturally: results are the network's, the record of how they were and weren't reached is the commons. D-1 makes the gate blind to tooling; D-19/D-23 provenance is what makes the corpus labeled, which is the whole of its value to inference research. Overturns if: release measurably changes contributor behaviour — postmortem volume rising without reuse (the D-13 farming series), or labs fencing their agents off the frontier — then the release lag lengthens (the embargo lever, below) before anything about capture changes; if instead the corpus goes uncited across a full target lifecycle, snapshots stop and the capture rules stay, since they cost nothing. The protocol is never shaped for the dataset.

Detail rules · evidence867 words

One record per gate run. Every authoritative gate run (D-4) emits an attestation whether or not it merges — D-5 already requires this on public nodes; this decision fixes the record's minimum content: schema, statement hash, node id and version, pinned Mathlib SHA and toolchain hash, model and tooling as declared by the operator (D-23), verdict with the first failing step and its structured diagnostic, the artifact hash on pass or the final elaboration state on fail, and a timestamp. So that a record is self-locating and reproducible without the service, it also carries: graph id, the hash of the gate-spec.json it ran under, the pinned network commit (D-35), the runner class (hosted or local), the hash and signature kind of the precheck attestation it consumed (D-4), the merge commit once merged, and a signing block — kind, key id, value. D-5's identical-verdict comparison masks the three run-environment fields (runner, merge_commit, signature) and nothing else. Bounced submissions (no precheck attestation, D-4) emit the same record with verdict: bounced — protocol-compliance data, not mathematics, and separable by that one field.

Local precheck records are opt-in and append-only. pregate.sh / precheck_submission (D-27/D-28) write a compact record — the same fields, verdict: precheck-fail, plus the terminal goal state — to nodes/<node-id>/attempts/precheck/ when the operator passes --record, deduplicated on (statement hash, goal-state hash, first failing step). Off by default: the volume is the operator's and the value is theirs to donate, and D-13's no-transcript rule holds — a precheck record is a verdict and a goal state, not a session. This is a judgment call: nearly every failed attempt dies locally and never reaches the gate, so this is the only way any of them enter the record without turning the gate into a telemetry sink; it stays optional so that D-26's "public by default" remains a rule about claims, not about every keystroke.

Schemas are versioned. D-13's YAML, D-14's approach record, the D-5 attestation and the precheck record each carry a schema field. A schema bump is a versioned change in the D-8 style, never an edit; every snapshot ships the schema files it was cut against; consumers parse by version; history is never reformatted.

Snapshots. A snapshot is a signed git tag on each graph repo plus a tarball at a stable URL, cut by the gate owner (D-4) — nothing an MCP tool does that the tag does not (D-28). Cadence: quarterly at Stage 1; additionally on every target-level event (resolution, dormancy — D-33) from Stage 2. Each snapshot records the cut timestamp and every target's D-33 status, and the nodes ready at the cut are that snapshot's held-out set: the network's own frontier is the benchmark, it is contaminated the moment a proof merges, and the timestamps are what let anyone reconstruct a clean temporal split. The network publishes no leaderboard; that is a consumer's job.

Exclusions are carried through mechanically. Bountied nodes (D-26) are absent until merge and disclosure — the rule the D-28 read tools already obey. Canaries (D-11) enter only once retired, labeled with their ground truth; the live set is never in a snapshot. Free-text fields (D-13 detail, D-14 approach records, D-31 annexes) keep their untrusted demarcation in the export: typed fields are the record, prose is context.

Optional trace attachment. An operator may attach a tactic-level trace to a merged proof or a postmortem as a content-hashed blob under attempts/, disclosed like any artifact. It is bulk, not record: the proof term or goal state stays canonical, the gate never reads a trace, and nothing in D-19 pays for one. Optional because the trace is the highest-volume, least-trustworthy thing a harness produces — precisely what the artifact-not-transcript principle exists to keep off the critical path.

Credit. No seventh ledger line. Every corpus record is credited under the D-19 line that already covers it; the corpus adds provenance, not payment. Paying for corpus contribution directly would be the postmortem-farming failure mode with the first-per-route-class rule removed.

License and consent — D-23 amendment. Lean sources are Apache-2.0 under DCO. The non-code record — attestations, postmortem YAML including goal states, approach records, review and adjudication records — is released under a single permissive data license named in D-23, and the sign-off text on every graph states that it covers both. Annex prose (D-31) is licensed by its author at submission or is not accepted. Settled before the first external contributor: retroactive relicensing needs every contributor's consent and in practice never happens.

Embargo is the only lever. The overturning condition reaches for exactly one tunable: a per-snapshot release lag, default zero, applied uniformly — never per contributor, never per node.

Evidence: D-5, D-13 and D-14 are load-bearing; this decision adds only the schema field, the cut, and the license to what they already require. Existing corpora define the gap: miniF2F and ProofNet are solved-problem benchmarks; LeanDojo is trace data from Mathlib — success on solved statements, no failure record, no judgment record. Per-node model disclosure follows the Leiden Declaration (D-23). The Aletheia finding (68.5% of graded "open" solutions incorrect) is why the intake and review record is the scarcest tier.

Statements, definitions, and fidelity§

D-8 — Statements immutable; blueprints evolve by versioning§

No contributor edits a statement, ever. Revision exists for defective statements only — vacuity, misformalization, junk values — never for "this should be weaker," which is what variants (D-30) are for. v3.46: a revision may also give a statement its relation to the root — a proposed crux (D-14 v3.26) becomes a labeled variant (D-30) with the statement unchanged and a Relation.lean attached, through the same revision request and curator act. A revision whose statement is unchanged (the same statement hash) reads the superseded node's merged partials and holes as its own routes and children: nothing is copied or rewritten, the products derive it from the supersedes chain, and the kernel still guards every join against the revision's own statement. A contributor who believes a statement is defective files a revision request — a typed operation naming the node, plus evidence. A curator may act on it, which creates <node-id>@v2 as a new node; the old node is marked superseded, keeps its history and any credit already awarded. Dependents are marked stale and re-derived; the compiler identifies them, because the dependency graph is the call graph. Clarified 2026-09-19 (v3.18): re-derivation rewrites nothing. A dependent's recorded dependencies stay as they were written (D-3); everywhere they are read — status, staging, the declared-dependency check, the published graph — a dependency that has been superseded is read as the node at the end of its revision chain, and the dependent's generated Context.lean, the one file that mirrors them, is regenerated by the post-merge job to match. The whole effect of a revision therefore traces to the one curator pull request that made it, and reverting that pull request restores every dependent exactly. A revision is followed only when its own record names the node it supersedes. stale on a node that has no proof marks nothing, since there is nothing to re-derive, and is not written or read; on a proved node it lifts when a passing attestation exists whose run included the revision (its graph_commit descends from the commit that marked the node stale), which is D-18's “re-run and re-annotated on survival”. Evidence lifts it; no record and no date does.

v3.25 — uses. A revision marks stale a proved node whose proof uses the revised node, as it marks a proved dependent; a use is read from the proof, never rewritten, and never followed through the revision.

Rationale: the prover who can't prove P has an automated, machine-speed incentive to "discover" that P should be weaker; D-30 gives that impulse a legitimate, labeled outlet (add a variant) so the immutability rule only has to police silent substitution, which is mechanical. Overturns if: revision requests outpace curator capacity — then this queue is the bottleneck, not review.

Detail evidence30 words

Evidence: research §2 — LTE showed decomposition is discovered during formalization (blueprint written after the proof), so the graph must be revisable; PFR's monolithic proofs are the warning case.

D-29 — Decomposition is emergent; the blueprint-author role is retired§

The graph beneath a root is not authored in advance. It grows from contributions: compiler-derived children of partial proofs (D-12 #5), reduction targets (D-12 #4), speculative crux nodes (D-14), prerequisite nodes from missing-library postmortems (D-13), and labeled variants (D-30) — proposable by any contributor, agents included, because route-finding is precisely what a prover does mid-attempt. Admission is mechanical: a proposed node enters the frontier when it passes the gate's statement-side checks (typecheck, witness, hazard checkers with the author's acknowledgments where a finding is intended — D-4, declared relation where claimed, acyclicity). No human approves structure. A compiler-derived hole (D-12) is admitted without a witness and stays blocked until one is supplied; supplying it is itself a proposal. (v3.22) A hole's witness exhibits only the hypotheses it inherited from other holes. Those it inherited from facts the decomposition proved are discharged by the gate from the proof already merged in the assembly, which step 4 has kernel-checked. The hole's statement is unchanged, still closed over everything in scope, so its hash, its round trip and D-31 finalisation are untouched; only step 7's expected type is narrowed. A hole written before this rule keeps the expected type it was written with. (v3.24) A partial may carry the witness of any of its holes. The gate holds each carried witness to step 7 against the statement that hole's node will have, in the sandbox and before the merge, exactly as it holds a witness proposal; one that fails refuses the whole partial, naming the hole. A hole whose witness was carried is created with it and is never blocked for want of one; a hole whose witness was not carried is admitted without one and stays blocked until one is supplied, as before. Clarified 2026-09-17: a D-8 revision of such a hole, carrying the witness slot it inherited, is admitted the same way and stays blocked until a witness is supplied: the statement changed, not the witness rule (F08-Q21).

v3.25 — uses. A hole's statement is written under its parent statement's imports and the definition modules its assembly declared; the proof of a gate-written hole may declare uses as any proof may, and its recorded dependencies stay empty.

Rationale: every mechanism a prospective decomposition needed already exists as a contribution type; keeping a human strategist in the loop of an agent-speed search was the last formalization-era assumption, and the authority it carried decomposes into one mechanical rule and one thin curator function. Overturns if: frontier noise from duplicate or junk holes measurably drowns self-selection — then admission adds a lightweight curator ack, still never an authored blueprint requirement.

Detail rules111 words

The residual human authority is thin and belongs to the curator: versioning defective statements (D-8), consolidating syntactically duplicate nodes, and intake itself (D-6). Curators may not claim proof credit on targets they curate (D-21).

What replaces the blueprint author's protections: - Weight self-inflation → gone with prospective weights (D-19). - Statement rot toward provability → root immutability + the D-30 claim discipline: weakening is legal only as a labeled addition, and "resolved" is a kernel-checked relation, so there is nothing left for silent weakening to buy. - Graph spam → mechanical gate + identity-layer rate limits (D-19) + duplicate consolidation; near-duplicate holes are tolerated noise, priced by self-selection (D-25).

D-30 — Weaker variants are first-class; resolution claims are relation-checked§

Proving a weaker version of a target is legitimate research progress and needs no one's permission. Any contributor may propose a variant statement of a root: immutable and content-hashed like any statement, with a non-vacuity witness, entering the frontier as its own claimable node.

Rationale: partial results are the normal currency of research on open problems, and the prover's incentive to weaken is now automated and constant; giving it a legal, labeled, kernel-checked outlet converts the system's chief statement-integrity threat into its chief progress mode. Overturns if: related variants are used to farm statement-line credit at write-up — then related proposals require an attached motivation record and earn only on demonstrated citation, D-14-style.

Detail rules · table270 words

The relation to the root is a label, and the label is kernel-checked where it matters:

Label Meaning How established
resolves proving the variant resolves the target a Lean proof of variant → root attached and gate-checked
partial the variant is at most as strong as the target a Lean proof of root → variant attached and gate-checked
related no proved relation neither implication supplied
refutes (v3.46) proving the variant refutes the target a Lean proof of variant → ¬root attached and gate-checked

v3.46 — a variant may refute. A proved refutes variant is a counterexample to the root (D-12 #2) by another road, exactly as a proved resolves variant is a proof of it: the post-merge job joins the variant's proof through its Relation.lean to a kernel-accepted ¬root and the root reads refuted by derivation while the variant reads proved and the root's statement is vouched as step 9 accepts (D-12 v3.42); nothing is written as a status. Such a proof settles the target and is asked step 9 like a resolving one (D-4 v3.20). A proposed crux (D-14 v3.26) that is in fact a refutation of its root — the natural counterexample candidate, stated so that it can be proved or refuted — becomes a refutes variant by a revision (D-8 v3.46) carrying the relation, its own proofs and holes intact. A false member of a sufficient set never refutes anything: it kills its route (D-25 v3.40), because a route promises sufficiency and nothing more; refutation is the sufficient sets of the other side (D-25 v3.46).

Claim discipline, mechanical: only a proof of the root itself, or of a resolves-labeled variant, may be reported (D-10) as resolving the target. A proved partial variant is reported as a partial resolution — exactly what it is. A proved related variant is a standalone result on the target's page. Misreporting is a D-17 ground (ii) dispute with the implication proof as the exhibit.

Fidelity: variants originate formally, so they carry no fidelity certificate (D-9's formally-native handling); the target-level claim is protected by the relation proof plus the root's own certificate. v3.12: that protection covers resolves and partial, where an implication is proved and the kernel does the work. It does not cover related, where nothing is proved and the only claim made is the sentence saying why the variant bears on the target — an improved bound, a nearby case, a reformulation. That sentence carries one signature before the variant is published as pertinent to the target. It is not a fidelity grade and does not enter the ladder; it is one human act on the one claim no kernel checks. A variant's mathematical interest is judged by nobody in advance — self-selection and retrospective write-up (D-19) price it.

v3.39 — a reading not chosen becomes a variant. Where a formalization review (D-9 v3.39) ends with clusters the intent signer confirms are genuinely different readings, the chosen one becomes the root and each other is published as a variant of it, with its relation label proved where the review's pairs already prove a direction and related otherwise. A variant made this way is never the root and never carries the certificate; it is open work like any variant. If a signature later chooses a different cluster than the one being proved on, the root is revised (D-8) to the chosen one and the old root's work stays on the record as a variant. Nothing is lost and nothing is rewritten.

D-9 — Graded fidelity certificates on root statements and definitions§

Fidelity review applies to root statements and definitions only; integrity (D-4) and fidelity fail independently, and nothing in the gate touches the second. Definitions are first-class review objects: a wrong definition yields a formally true theorem about the wrong object.

Rationale: fidelity and integrity fail independently — integrity (D-4) asks whether the artifact proves the statement; fidelity asks whether the statement is the conjecture. Overturns if: definition-level defects prove rarer than statement-level ones in the pilot — then collapse the two review objects into one and save the ledger.

Detail rules · evidence1271 words

Mechanizable tools run first: consequence lemmas, special-case lemmas, triviality controls, numerical spot-checks, back-translation. Back-translation is performed by a non-author, always. They are the adversarial component. v3.12: the tools are an ordered pass with a fixed output, not a menu. The 2026 autoformalization evidence is that a statement which compiles is only about three-quarters likely to mean what was intended, and that back-translation is the weakest of the four checker families — so no single tool, and back-translation least of all, may stand for the pass. Cheapest first, each layer producing an artifact rather than an opinion:

  1. Compile against the graph's pinned toolchain. Necessary, and worth about three-quarters on its own.
  2. Soundness screens under a bounded tactic budget: prove the statement, prove its negation, prove False from its hypotheses, and derive its known consequences. Any success is a rejection carrying a kernel-checked exhibit. The statement is introduced as an explicit hypothesis or axiom in a scratch file, never as a sorry in a graph file, which D-4 step 2 rejects anyway.
  3. Definition-grounded judging and a structural signature check, producing a review brief that lists every referenced term with its definition. Triage and preparation for a human, never a verdict.
  4. Bidirectional equivalence against an independent formalization of the same statement, once two exist. A proved equivalence is strong evidence and the only sound test for strength drift; a failure is inconclusive and is not recorded as negative.
  5. Non-author sign-off, the only event that changes accepted state, with every automated verdict attached as evidence.

Exhibits and judgements are not the same record. Layers 2 and 4 emit kernel-checkable exhibits and belong to the trust base; layer 3 emits a judgement and belongs to the review brief attached to the certificate. Only the first kind may be cited as evidence for a grade. A judge running near 90% accuracy must not become an authority by accident, and keeping that line sharp is the whole of what prevents it.

A derived falsehood is routed, never auto-labelled. Deriving something known to be false from an assumed root means one of two very different things: the statement is a misformalization, which is a D-8 revision, or the conjecture is refuted, which is a D-12 resolution artifact. The screen files a defect claim carrying the exhibit (D-15) and a person decides which; no automated step may mark it either way. Screens re-run whenever the statement version changes or the graph's Mathlib pin moves, because junk-value defects appear and disappear with the library beneath them.

Public comment period. Root statements are published before the graph opens for proving, in the venues named in D-10. For Erdős targets the expert pool is the erdosproblems.com forum and the Lean Zulip, not a hire.

Fidelity status is graded, not binary. A root carries one of:

mechanical-only → screened-and-signed → author-attested → expert-attested → published-and-uncontested

  • screened-and-signed — v3.12, replacing back-translated. The mechanizable pass above completed with its exhibits recorded, plus a non-author signature on the comparison. Back-translation is one named input to that pass and no longer the name of the rung: naming a rung after the weakest check in it invited the reading that the check was the rung, and a statement that had cleared it had cleared something with a known false-pass rate near one in three. The rename is the whole of the fix; the floor stays here, because the rung is now materially stronger than the one it replaces. Consequence for the schemas: target-status and targets-index carry this value in an enum, so the rename is a schema version bump under D-34's never-edited rule, budgeted into F11.
  • Signatures are counted and named. Every certificate records who signed and how many have, and the count is published rather than waited for: a target sits at its current rung with one signature showing, and rises when a second arrives. expert-attested is exactly author-attested plus one independent signature, so the count is load-bearing and hiding it would make the ladder unreadable.
  • v3.17 — a steward may sign and prove. A steward (D-32) who did not write the target's Lean is a non-author signer under the rule above, and signing bars them from nothing: they may prove on the problem, guide provers, and earn proof credit (D-19) like anyone. A bar on signers proving was drafted and withdrawn before release (2026-09-17): the mathematician who put the problem forward is the one who will want to work on it, and the fidelity failures of 2026 came from provers misreading statements, not from mathematicians misrepresenting their own. Verification of the statement is, in practice, other people's act, and the non-author rule already makes it so for whoever wrote the Lean.
  • author-attested — attestation by whoever is responsible for the source conjecture's listed formulation (for open problems the "source paper author" branch rarely applies; the attestor is typically the problem's curator or poser-of-record). Informative (they know what they meant) but structurally non-terminal: the defended failure mode is the Erdős-75 case — the listed formulation is itself flawed, which its own author cannot detect. For open problems this is the dominant fidelity risk, since there is no proved theorem anchoring the statement's intent. Upgrades to expert-attested with one independent signature.
  • published-and-uncontested is operational, not reputational: N days public in a D-10 venue + M independent proof attempts + zero confirmed defect claims (D-15). It downgrades automatically on any confirmed defect anywhere in the statement's definition closure. Pilot defaults: N = 30, M = 3 — tunable, recorded per graph. v3.12, what counts as an attempt: a documented public attempt on the statement counts toward M, including the prover sweeps run against an upstream registry (AlphaProof Nexus, Aletheia, Aristotle and their successors) — this is what D-10's "public venues, not in-network" already says, and for an inherited statement those sweeps are usually the only attempts that exist. The guard is that an attempt counts only against the statement content hash it actually ran on: if the statement was amended after the sweep, its attempts do not carry across the revision. Each counted attempt is recorded named, dated and linked, and attempts on any conjecture are recorded to the extent they are documentable at all.

Claims made about a completed target are scoped to its status. (A sentence here once said no proving compute is allocated below screened-and-signed; v3.15 made a listed target claimable at once, and the sentence was removed in v3.17.)

Scope exemptions — nodes that carry no certificate: - Interior nodes, including authored and skeleton-hole ones (v3.12) — D-31 skeleton holes are chosen by a contributor rather than generated by the elaborator, but fidelity of an interior lemma is irrelevant to soundness either way; only its formal role in deriving the root matters, and that role is kernel-checked by the assembly it came from. - Compiler-derived statements — D-12 partial-proof children and reduction targets. The statement is generated by the elaborator from a residual goal; there is no informal referent. Fidelity is inherited from the root through the kernel. - Variant statements (D-30) — formally originated; the target-level claim is protected by the kernel-checked relation label plus the root's own certificate. - Formally-native targets — statements the network (or ETP-style projects) originates in Lean first, with no prior informal statement. No correspondence exists to check; the record marks them formally-native rather than granting a fidelity grade.

Thin attestor pools get a declared cap, not a workaround. Where the qualified attestor pool is near-empty (e.g. alignment formalizations), the target proceeds capped at screened-and-signed with a doubled public comment period, and the cap is stated in any claim made about the result. A fidelity ceiling that cannot be raised is declared, never worked around. Refusing thin-pool targets outsources the agenda to attestor availability; proceeding uncapped launders weak fidelity into strong claims. Cap overturns if: capped targets accumulate confirmed post-hoc fidelity defects at a higher rate than attested ones — then thin-pool targets pause until the pool exists. (The author-CoI pattern is already closed above: author-attested is non-terminal and back-translation is non-author, always.)

What no certificate catches: strength drift (≤ for <, asymptotic for explicit, "sufficiently large" for an explicit threshold), degenerate-but-satisfiable statements, and an ill-posed source conjecture. These are the permanent residual risk and the certificate should not be read as retiring them.

Evidence: research §3–4 — Aletheia misformalization rates; the fidelity caveats every frontier release itself flags: Astra, AXLE, Gauss; fidelity/integrity independence per Ammanamanchi–Bhat–Biderman.

v3.15 — several formalizations of one conjecture. A conjecture may carry more than one Lean formalization. A second formalization lives beside the root, is never a frontier node, and is linked to the root by an equivalence exhibit. An equivalence is evidence shown on the target page; it does not raise the fidelity grade or satisfy D-4 step 9 by itself.

v3.39 — a formalization review. A root statement that arrives in words (D-6) is formalized in a review, and the review's surviving Lean becomes the root. A review has seven stages; stages 3, 4 and 6 are agent work and emit only kernel-checked exhibits. (1) Propose: the conjecture in words with whatever pins it down — known special cases, small values, consequences, non-examples. (2) Formalize: anyone may submit a candidate, a Lean statement with its author named and, where a model helped, the model named (v3.31); agents submit candidates from several models; people submit blind, shown the words, the definitions and the cases and never another candidate's Lean until their own is on the record. (3) Filter: each candidate is compiled, screened (prove it, prove its negation, prove False from its hypotheses) and held to the intent tests below; one that fails any is discarded with the exhibit as its reason and stays on the record. (4) Reconcile: candidates are compared in pairs (below); those proved equivalent form a cluster; between clusters, agents look for a case on which they disagree. (5) Ask: each proved disagreement becomes a question to the intent signer, in mathematics, never in Lean; the answer becomes an intent test and stage 3 runs again, until one cluster survives or the clusters left are readings the intent signer confirms are genuinely different (D-30 v3.39). (6) Mutate: agents perturb the surviving cluster's representative the ways statements are known to go wrong (D-11's defect classes); a mutant every intent test passes becomes one more question, and the page reports how many mutants the tests catch — a measure of the tests, never of the statement. (7) Sign: two signatures, by role, on the evidence page.

v3.39 — when work opens; step 9 reads the review. A new target becomes claimable when the automated stages are complete: one cluster survives stage 3 and stage 6 raises no open question; the signatures arrive while proving goes on, and the grade rises as they do. Targets that exist already stay claimable and keep their grade: each is given a review in the background, its statement the first candidate, and anything found goes the existing routes, a defect claim (D-15) and a revision (D-8); nothing leaves the frontier to wait for people who have not been found. A proof that would settle a target's root (D-4 v3.20) merges only when that target's review is complete — automated stages done, no open question, grade at least screened-and-signed — so intermediate work never waits for the review and the claim that a conjecture is settled always does. v3.15's second basis stands beside it: recorded catalog evidence about the statement scoring at least five points still satisfies step 9 without a completed review, the evidence recording why the source is reliable; the automated stages still run in the background and never hold that merge. A background review never holds step 9 (the owner's ruling of 2026-10-12): the review the network opens on a target that existed before this amendment informs and files what it finds through D-15 and D-8, and step 9 on that target stays what it was before v3.39, a review that a proposer, steward or curator opened being the one that holds. Who opens a review is a setting: the roles that may open one are listed in the graph's policy.json (F24-R1's file; each setting dated with its reason, changed by one visible curator pull request, applying to reviews opened after the merge); the first value, and the default where the setting is absent, is all three — the proposer (through D-6), a steward of the target (D-32) and a curator (D-22). For targets that exist already the network opens one in the background whatever the setting says. Porting: a statement imported from a registry (D-10) enters as the first candidate, credited to its registry's authors and judged like any other; each later candidate's author declares whether they read it first, shown as a claim; where the imported statement does not meet the format rule, the review adds a wrapper naming its parts, proved equal to the original by rfl, the original's text and hash untouched. Rationale: the 2026 evidence (research §1) is that a compiled statement means what was intended about three times in four and that sampling more does not close the gap; the only sound checks are refutations and proved equivalences, and the only judge of intent is a person. Overturns if: reviews on real intake end with more than one surviving cluster most of the time while the intent signer cannot say which reading is meant.

v3.39 — intent tests. An intent test is a Lean statement about the conjecture that any acceptable formalization must satisfy (holds at n = 3, fails at n = 1, implies the known k = 2 case, says nothing vacuous on the empty set), run against every candidate by computation or by a proof attempt within a budget, its result an exhibit. A model may choose which small, degenerate or boundary cases suit the statement and write them in Lean, or record that small cases do not apply and why; choosing a test is not a verdict, because the kernel checks the test. No model supplies an expected value: each test's expected result comes from the intent signer's answer, a cited source, or a computation on which every surviving candidate agrees, the record naming which and showing the last as the weakest. Disagreement is the signal: where candidates answer a case differently no test is written and the case goes to stage 5 as a question; where every candidate is vacuous on a case the page shows a triviality flag. Three probes, not one: each test is run as holds (the claim at n against the answer), covers (the claim at n with every concept the words use made empty, which tells "holds at n" from "says nothing about n" and catches a narrowed or widened domain on a true conjecture) and witness (the concept replaced by a small set — "suppose 5 were the only prime" — which exposes the formula's intervals, connectives and how many witnesses it asks for, and catches a weakening or strengthening of a true conjecture, which no test of truth values can). Where candidates' predicates for one concept disagree on a value ("is 1 prime?"), the value is a question. Format rule: a candidate names each concept the words use as its own predicate; one that writes the concept inline cannot be probed and is returned to its author with that reason, never discarded. Intent tests re-run whenever the statement is revised (D-8) or the Mathlib pin moves, as the screens already do.

v3.39 — pairs. Every pair of candidates, and every pair of formalizations a root carries (v3.15), records each direction separately as proved (a Lean proof that A implies B), refuted (a kernel-checked instance where A's claim holds and B's fails, at some n or under some probe — not a proof of ¬(A → B) about the whole statements, which for an open conjecture is usually unprovable) or open (attempted without a result, the attempt recorded: who, what tool, what budget). Both directions proved: the two are equivalent and share a cluster. One proved and one refuted: one is strictly stronger, D-9's named residual, now caught when it occurs. A failed attempt is never recorded as refuted. Open directions are claimable work for agents on any root not yet expert-attested, and after it whenever a new candidate arrives; a proof or refutation goes through the gate like any other artifact and is credited (D-19). The degenerate guard is on by default: a direction whose proof never uses its hypothesis's content is refused as a proof of equivalence. Rationale: research §3 — proved equivalence runs at 98% precision and about half recall, so a proof is strong evidence and its absence says nothing; a refutation is as certain as a proof and is the question for stage 5.

v3.39 — two roles, and the ladder earned under the review. A root's certificate names two signers by role. The intent signer answers the review's questions and signs that the surviving cluster says what the conjecture says: the proposer, or for a conjecture inherited from a source (D-6, D-10) the target's steward (D-32), whose answers each cite a source, an answer without one flagged on the page. The independent signer reads Lean, wrote no candidate in the surviving cluster, and is not the intent signer; they sign that the evidence supports the surviving cluster. "Author" means the author of the Lean in every non-author rule; the author of the conjecture's wording is the intent signer and is named so. A signature is a decision written by a person: accept a cluster, split into variants (D-30 v3.39), or send back with a new question; the page never computes one. The ladder is kept and earned so: mechanical-only, the statement compiles; screened-and-signed, the automated stages complete (one cluster, screens and probes pass, no open question) and one signature from someone who wrote no surviving candidate; author-attested, the intent signer signs; expert-attested, both signatures and at least one person-written candidate in the surviving cluster, else the target caps at screened-and-signed and the cap is shown, as the thin-pool rule already does; published-and-uncontested unchanged. No grade already held is taken away by this amendment. Beside the grade, a target shows its review's state ("6 candidates, 1 cluster, 2 questions waiting"): the grade says what was signed, the state what is under way.

v3.39 — back-translation leaves the pass. A signer reads the Lean rendered mechanically, with every type and coercion shown, beside the gloss (v3.30), so nothing they read was guessed by a model. Research §3: back-translation passes about a third of wrong statements on easy material and rejects most correct ones on hard material; the questions of stage 5 do its job with an answer from the one person who knows. QA records that include it stay valid; the floor no longer asks for it.

v3.39 — the evidence page. Each review has one page on the site (D-36), built from the record only: the candidates, each with its author, how it was made, its stage-3 result and, if discarded, the exhibit that discarded it; the pairs and clusters, each direction proved, refuted or open; the questions and answers, each with the case it came from, the answer and its source, and the intent test it became; the test matrix, candidates by intent tests, and the mutants caught; the screens and the brief, the brief marked as a model's judgement; and the two signature slots, signed through the site (v3.33). Exhibits and judgements stay apart as v3.12 requires: only exhibits are evidence for a grade. Where the proposer answers: on this page, signed in with GitHub, each question in mathematics beside the small case or probe that raised it; an answer is an append-only record on the graph, signed by the network's approval key and naming the login (as a v3.33 approval is), so the test built from it can always be traced to who said what; agents read the questions through the MCP, only the intent signer answers. How the proposer hears: when a review has questions waiting, the GitHub App posts one comment per batch that @-mentions the intent signer, on the review's tracking issue in the graph repository (or on the pull request that proposed the conjecture), listing the questions and linking the page; GitHub notifies them by its own settings, so the network never collects or holds an email address; the same notice appears on the signer's /me/ page (v3.35).

D-10 — Statement registry interop, not a private registry§

Rationale: a private statement registry re-creates the fidelity problem the public ecosystem already crowdsources; inheriting and upstreaming buys review from the largest qualified pool that exists. Overturns if: upstream venues systematically reject or ignore network statements — then in-network publication with equivalent visibility becomes the default rather than the fallback.

Evidence: research §4 — google-deepmind/formal-conjectures (~240 Erdős statements formalized) and erdosproblems.com are the existing review pools; a private registry re-creates the fidelity problem they already crowdsource.

v3.15: registry inheritance supplies the statement and its provenance; it does not waive D-4 step 9. A hash-pinned catalog evidence record scoring five points or more does.

D-11 — Overt canaries measure review; catch rate replaces escape rate§

Known-defective statements, one class per row of the research §3 fidelity table (missing hypothesis, junk values, vacuity, quantifier scope, wrong domain, definition mismatch), are seeded into the review queue only — never the claimable frontier — at a disclosed-but-unspecified rate. Reviewers know canaries exist; not which. Caught canaries retire cleanly under a status excluded from D-25's ready set.

Rationale: escape rate counts defects nobody caught and is unmeasurable by construction; covert seeding, once discovered in a public-by-default network, would cost the community trust D-26 exists to earn. Overturns if: crafting non-lazy canaries costs more curator/reviewer time than the measurement is worth — then narrow to the mechanically generatable classes and accept partial coverage.

Detail rules · evidence70 words

Metric change: canary catch rate, per reviewer and per defect class, replaces misformalization escape rate as the measured Stage-1 gate criterion; escape rate is estimated from it, not observed. Per-class catch rates direct mechanical-checker coverage.

Evidence: research §3 — the fidelity-defect taxonomy (missing hypothesis, junk values, vacuity, quantifier scope, wrong domain, definition mismatch) from Ammanamanchi–Bhat–Biderman supplies the canary classes; escape rate is unmeasurable by construction, catch rate is not.

Resolution artifacts§

D-12 — Five resolution artifacts, not three§

# Artifact Effect Kernel-checkable
1 Sorry-free proof Closed Yes
2 Counterexample (proof of ¬P) Closed as refuted; escalates to parent; at the root, also by a proved refutes variant through its relation (v3.46) Yes
3 Vacuity certificate Closed as defective; forces D-8 revision Yes
4 Reduction — proof that the node follows from a stated new node Node stays open; the new node enters the graph as its child (v3.19) Yes
5 Partial proof — typechecks modulo k named sorrys Node stays open; the k holes become child nodes (v3.19) Yes, modulo the holes

Partial proofs merge into attempts/, never Proof.lean. Residual holes enter the frontier directly as compiler-derived children (D-29) once they pass the mechanical gate; no human promotion step. A curator may consolidate syntactically duplicate holes; near-duplicates are tolerated frontier noise, priced by self-selection (D-25). Closing a hole earns proof-line ledger credit like any node.

Clarified 2026-09-19 (v3.19): a decomposition never blocks the node it decomposes. A reduction's new node and a partial's holes are recorded on the parent as children: lemmas it may draw on once they are proved, never dependencies it waits on. The parent therefore stays open — claimable, provable directly, and open to further decompositions, whose holes are numbered after the earlier ones so rival routes coexist as separate sets of children — and only a proof, a counterexample or a vacuity certificate (artifacts 1–3) closes it. A hole a later decomposition restates is that hole again, not a new node; a hole that restates a node under another branch of the target is that node, and the parent gains it as a lemma (v3.38): an entry of META.yaml’s lemmas, written by the post-merge job, with exactly a hole’s standing — its signature in the parent’s Context.lean, drawn on once it is proved, never waited on. One proof of such a node closes every branch that points at it. Before v3.38 that hole recorded no edge, so the merged assembly could never be used and the recognition reached only the job’s log (the 2026-10-09 run on erdos-1094, --h3 restating --h2--h1--h1); the ancestor rule below already refuses the one hole a lemma edge could make circular. A merged proof of the node leaves its open holes as they are: each is a statement of its own and stays on the frontier. Before this clarification the gate recorded holes as dependencies the parent waited on, so the first merged partial took its root off the frontier and refused every other route to it.

v3.42 — proved by closure. When every input of a node’s merged decomposition is proved, the node is proved by construction: the assembly the gate checked, the children it wrote as exactly the gaps (D-29), and the children’s proofs are the whole proof. After every merge the post-merge job closes every such node of every target, in the step-3 sandbox and with no secret: it elaborates the assembly, replaces each hole of its term by the child’s theorem applied to the locals in scope, has the kernel accept the node’s theorem, and writes a closure record beside the node (closure.json), which the one step that holds the gate key signs. It repeats until nothing more is ready, so a proof at the bottom of a chain closes every level above it in one merge. The same holds for one other kernel-checked link: a proved resolves variant (D-30) closes the root through its Relation.lean; and from v3.46 a proved refutes variant closes it the other way, the join being a kernel-accepted ¬root and the closure record's verdict saying refuted, read with the same guards (every input proved, the root vouched). A circularity claim is no link: a proved hole closes what it was cut from only through a route, its siblings proved beside it (the owner’s ruling of the same day, F28-Q12). Nothing is written as a status: a node with a closure record reads proved exactly while every input does, so reverting an input re-opens everything above it on the next render (D-18 v3.18). The root reads proved by closure only with its statement vouched as step 9 accepts it (v3.11, v3.15, v3.39): its certificate, a completed formalization review, catalog evidence, or a calibration target; without one it waits, and a person vouches by those same records. A node proved by closure is used by a later proof like a merged one: the gate builds its module from the join. Its work is credited where it was done (D-19): the assembly and the inputs’ proofs earned their lines, and the join earns none. Proved never stops work: a direct proof of a node proved by closure merges as an alternate (v3.13). The kernel is the guard: a revised hole weaker than its gap, or any child that does not state its gap, makes the join fail and nothing is recorded, so no closure can prove less than the node’s own statement. (v3.41, the same day, had the network write each join as a Proof.lean and submit it through a pull request, one level per merge; the text composition was the fragile part, every level cost a queue round, and the structure needed none of it.) Overturns if a join fails more than rarely, since each failure means a gate-written hole did not say what its gap said, which the round trip (F07-T18) exists to prevent.

v3.44 — a partial names its work. A partial proof (#5) says in its own comments what it is doing, in the grammar the gate reads: one -- approach: <one line> before its first hole, naming the attack this decomposition takes, so that where a node has several routes a reader sees the competing approaches side by side; one -- licence: <licence> (D-23) for those words; and, in the comment block directly above each hole’s have, -- label: <at most 60 characters> and -- claim: $<the hole in notation>$, the rest of that block being prose about the hole. The service refuses a partial without them before any precheck is spent (partial-unlabelled, naming each missing line), and the gate refuses one at step 4 by the same name, so a hand-opened pull request meets the same rule. When the partial merges, the post-merge job writes each hole’s label and claim as that hole’s first statement gloss (D-3 v3.44), authored by the partial’s author, under the licence the partial names, with the models the submission declared (D-23); the network writes no words of its own. An AND fork is read from a route’s hole labels; an OR fork from its routes’ approach lines; no note is ever attached to an edge, because the second route of a node is written by someone who did not write the first. A partial merged before this rule keeps its text; its approach is read from its leading comment or its annex (D-25 v3.44) and its holes take the labels v3.44 gives them.

v3.25 — uses. A proof may cite the merged proof of another node of its target, declared in its header, provided that node does not rest on the node being proved, through recorded dependencies or through the uses of merged proofs; a node is never proved from the node it was cut from, nor from anything proved from that node.

Rationale: a partial proof is a compiler-derived decomposition of the residual difficulty — the highest-value artifact current systems discard. Overturns if: residual holes are routinely harder than the original — then partials are difficulty-laundering and re-enter attempts/ as postmortem material only.

Detail rules · figure · evidence458 words

Offload rule (mechanical). No hole may be definitionally equal to the node's own goal, and a partial whose assembly is a single such hole is rejected at the gate, not reviewed. Restating the goal under a new name is the cheapest available fake progress and the one AlphaProof Nexus observed in practice; it must cost a rejection rather than a hole in the frontier. Partials that are non-trivial but shallow are not policed here — that is what self-selection and the D-25 starvation metric price.

No cycles (v3.21; v3.43). The offload rule reaches every statement the node reduces, not only its own goal: a hole definitionally equal to the statement of any node that depends on this one, however indirectly and read through revisions, is refused at the gate (offload-restates-ancestor). Definitional equality is the same term after renaming bound variables, unfolding definitions and computing, with no theorem used; the check is mechanical and certain. v3.43: that is the whole of the circularity rule. Nothing else marks a hole as circular, and no label is published for it. A hole implies the node it was cut from, given its sibling holes, because the merged assembly is that proof; so every hole of a one-hole decomposition, and the last open hole of any decomposition once its siblings are proved, is one whose proof would prove its parent, and through a path whose other holes are all proved, an ancestor further up. That is what a hole is, not a defect, and the drawing’s line from hole to parent already says it. (v3.21–v3.42 let anyone file a defect claim of class circular-decomposition (D-16) whose Lean exhibit proved an implication between the hole and an ancestor: v3.21 asked for the ancestor implying the hole, met by every provable hole; v3.23 turned it round to the hole implying the ancestor, met by every assembly once the hole’s siblings are proved. v3.21–v3.34 took a claimed hole off the frontier, and v3.22 every open node between it and the ancestor on a path whose other holes were proved; v3.35 made that a label once removal was seen taking genuine progress off the frontier on erdos-1094, 2026-10-08. For a one-hole decomposition, or the last open hole of one, the exhibit is the assembly restated: the label marked only the holes where someone had filed, and agents spent sessions writing such exhibits. Where the hole’s siblings were still open the exhibit was real mathematics, and v3.41 used it as a closing link (F28); v3.42 dropped that link and v3.43 the claim itself, for one rule, the owner’s ruling of 2026-10-15: a proved hole closes what it was cut from only through a route, its siblings proved beside it.) A cycle can still hide behind a proof — on 2026-09-23 one grandchild hole was the root again after a two-term reindexing, and another hole was equivalent to its target by a real argument — and no program decides that in general; such a hole stays on the frontier as an ordinary hole, and a proof of it is welcome, because it proves the ancestor. The merged claims of the retired class stay in the record as history, under the hole’s defects/, listed among the node’s defect claims (D-16 v3.28) as history and never as open against the statement; nothing is derived from them, and a new one is refused by the service and by the gate (defect-class-retired). The target is never closed by any of this, and nothing is rewritten. Overturns (v3.43) if: holes equivalent to an ancestor by a real argument come to dominate a target’s frontier — then the instrument is a claim proving both directions, hole and ancestor equivalent, since while the ancestor is open the reverse direction takes a real argument and so carries information, and a steward (D-32) may retire such a route by a signed record citing it.

Skeletons are partial proofs (D-31). A Lean skeleton derived from an informal argument — assembly proved, every lemma sorry — is artifact #5 with skeleton-hole rather than compiler-derived holes (v3.12, replacing authored); annex, credit and citation rules are in D-31.

Root-level outcomes are research results, with equal status. For an open target, a counterexample at the root (artifact #2) is a full negative resolution of the conjecture — reported upstream per D-10 as a result, not treated as a defect-flavored event. A vacuity certificate at the root (artifact #3) means the conjecture as posed is ill-formed; it is reported to the source registry, not merely routed to internal D-8 revision. A reduction at the root (artifact #4) — "the conjecture holds modulo these named cruxes" — is a primary progress mode when the truth value is unknown, since it converts an open problem into strictly sharper open problems. And a proof of a partial-labeled variant (D-30) is a partial resolution of the target — reported as exactly that.

The five resolution artifacts of D-12 and their effects on the node, the graph, and the root artifact (kernel-checkable) effect on node & graph at the root 1 · sorry-free proof node closed conjecture resolved — reported upstream (D-10) 2 · counterexample kernel proof of ¬P closed as refuted escalates to parent negative resolution — a full result, reported upstream (D-10) 3 · vacuity certificate hypotheses unsatisfiable closed as defective forces a D-8 revision conjecture as posed is ill-formed — reported to the source registry 4 · reduction proof the node follows from a stated new node node stays open its new node enters the frontier as a child (D-29) holds modulo named cruxes — strictly sharper open problems 5 · partial proof typechecks modulo k named sorrys node stays open merges to attempts/ only k holes enter the frontier as compiler-derived children (D-29) root stays open; its holes are new attack-route nodes
The five resolution artifacts (D-12). At the root of an open target every artifact is a research result, not a failure mode; a proved partial-labeled variant (D-30) is additionally reported as a partial resolution.

Evidence: research §1–2 — Goedel-Architect counterexample registration (prove the negation); AlphaProof Nexus caught restated-lemma sorry offloading, motivating artifact #4/#5 discipline.

D-13 — Failed attempts are first-class artifacts§

Appended to nodes/<node-id>/attempts/<timestamp>-<contributor>.yaml. Typed and short — not a transcript.

Detail rules · code · evidence370 words 
schema: d13/v1                  # versioned per D-34
node: erdos-1196/lemma-14
contributor: <id>
route: "strong induction on the exponent k"
route_class: induction | generating-function | probabilistic |
             direct-estimate | case-split | reduction-to-known | computational
outcome: refuted-route | exhausted | abandoned-early | blocked
terminal_goal_state: |          # serialized Lean goal state
  n k : ℕ
  hk : 2 ≤ k
  ih : ∀ m < k, P m
  ⊢ ∑ i in Finset.range k, f i ≤ C * k ^ 2
failure_class: missing-library | statement-suspect | timeout-blowup |
               needs-new-definition | route-dead-ends | budget-exhausted |
               informal-gap
detail: >
  Reduces to a uniform bound on partial sums; Mathlib has Abel summation
  but not the Cauchy–Schwarz variant needed for this index set.
artifacts:
  partial_proof: attempts/2026-08-17-partial.lean
  missing_lemmas: ["uniform bound on ∑ f i over Finset.range"]

Rules: - outcome is mandatory and un-collapsible. "Refuted this route" and "ran out of time" are different facts; conflating them steers competent contributors away from routes that work. - terminal_goal_state is a Lean object, not prose. Highest-value field, free to produce, impossible to exaggerate. - No raw transcripts in the default context bundle. - failure_class: missing-library aggregates; above threshold the missing lemma enters the frontier as a prerequisite node — by way of the curator: a postmortem names the lemma in prose and a node needs a Lean statement, so the aggregate (threshold a per-graph config value, default 3) is surfaced to the curator, who proposes the node like any contributor (D-29). Nothing is created automatically. - failure_class: statement-suspect routes to D-8, not to the review queue. - failure_class: informal-gap records a failed skeletonization (D-31): the informal argument did not survive assembly, and terminal_goal_state localizes the gap or ambiguity to the joint that would not close. Names the annex hash.

Credit: a merged postmortem earns an attempts-line ledger entry, flat per class. Only the first per route_class per node earns anything — this is the anti-farming rule. Revised 2026-09-19 (v3.18): the entry is the same whatever the outcome. An earlier sentence here paid refuted-route more than exhausted; D-19 admits no prospective weights, no ledger ever read outcome, and a self-declared field that pays more is an invitation to mislabel it. What a refutation was worth is said at write-up (D-32). A refuted-route is still reviewed like any other claim, because it asserts something.

Corpus: merged postmortems are the failure tier of the attempt corpus (D-34); the schema field is what lets that record be parsed across revisions of this decision.

Feedback: every node's context bundle includes its attempt log. Nodes accumulating attempts without progress escalate automatically — surfaced to curator attention and eligible for bountying (D-26).

Evidence: research §2 — LeanMarathon's Worker stopping rule (audit → falsify → formalize) is the artifact-not-effort principle; typed goal states are the un-fakeable residue.

D-14 — Strategy-level failure records, target-scoped§

D-13 is node-scoped; a dead strategy has no node to attach to. For open problems this decision is central, not supplementary: given the base rate of resolution (research §1 — 9 of 353), refuted routes, dead subgraphs and crux reductions are the expected primary output of most targets, and this record is what makes an unresolved target a contribution rather than a write-off. Three carriers at targets/<target-id>/, descending in trustworthiness:

1. Dead subgraphs are never deleted. A branch killed by a counterexample or abandoned as unreachable is marked abandoned with a cause, and stays queryable with its statements, attempt logs and the artifact that killed it. This is free, fully grounded, and is the primary record.

v3.26 — proposed for. A crux statement may say which node of its target it was proposed for, in an append-only proposed-for/ record on the crux, written by its proposer or a curator; the latest record is the one shown. It is a pointer, not a dependency: it changes no status and no frontier entry, and once a merged proof uses the crux (D-12 v3.25) the use is shown instead. v3.46: the pointer is never drawn as a line of the proof tree. A proposed crux and its own holes are drawn apart from the tree, in a band of proposed statements, and no line joins them to the tree at rest; selecting or hovering the crux lights the lines the record has measured from it into the tree — a use, a lemma, a checked relation — and a relation the proposer only stated is shown as words, never as a line. A crux with a checked relation (D-30 v3.46) is a variant and is drawn as one. Clarified 2026-10-22 on the owner’s readings of the live page: every statement lives in one place. The tree holds what is connected to the root by a line it draws: a route to its holes, a declared dependency, and a variant’s checked relation (resolves, refutes, and partial, which gets a line of its own); a use is not a connection. The column of speculative statements, at the top right of the drawing with one statement per row and related ones adjacent, holds every statement not so connected that is speculative (a proposed crux, or a revision of one) or a related variant, with its holes; its lines are drawn only while lit. A superseded statement is drawn nowhere.

v3.27 — withdrawal. A record of this decision, or a defect claim, may be withdrawn by a listed curator through an append-only withdrawal record; the withdrawn file stays and is read as absent (D-18 v3.27).

v3.47 — shelving. Beside abandoned, which is a verdict that a branch is dead, a fourth carrier that is a judgment: a steward of the target or a listed curator may shelve a statement, or retire one merged decomposition of a statement, by an append-only signed record under the node (shelving/) that names the action, its scope and a cause, made through the service for a signed-in login or SSH-signed by hand. Shelving is not a status: a proved statement stays proved and an open one open. What follows is derived, never written: a shelved statement and every hole child beneath it leave the frontier, refuse claims, prechecks and submissions with a named refusal, and are drawn only on request; a retired decomposition closes nothing, and its holes and their children are shelved with it. The reach stops at three things, so that a judgment about one branch never takes work off another: the root; a hole that another live decomposition, under a statement not itself shelved, still needs; and a statement a merged proof uses, which may not be shelved at all. A retirement never climbs to a hole’s ancestors, and a statement joined to the root by its own relation is shelved by its own record or not at all. A later unshelved record by the same roles lifts a shelving, and a statement’s own latest record decides for it before any inherited one. Nothing is deleted or edited, and one commit’s revert restores everything. Overturns if a shelving is used to hide a sound line of attack, seen on the record.

Rationale: a bad node postmortem wastes one node; a bad strategy verdict can kill a line of attack across a whole target — so the bar for being believed is higher, and grounding, decay and retroactive payment are what raise it. Overturns if: approach records go uncited across a full target lifecycle despite bundle inclusion — then mechanism 3 is a write-only archive and is dropped, keeping 1 and 2.

Detail rules333 words

2. Crux-lemma speculative nodes. A contributor with a stage-1 idea may enter it as a speculative node: the single formal statement the strategy hinges on, body sorry, with a non-vacuity witness. This converts an unfalsifiable idea into a stage-4 object — it typechecks, it can be refuted by a counterexample, it inherits all of D-12 and D-13. An idea that cannot name its crux as a formal statement is not yet recordable. Clarified 2026-09-19 (v3.19): speculative is the proposer's label on an open statement, and a label is not a verdict. The moment a D-12 artifact settles the node — a proof, a counterexample or a vacuity certificate merged with its attestation — the node reads proved, refuted or defective, and the label is history; no record has to be written to lift it, because a proposer's word never outranked the kernel's.

3. Approach records — free-text, for strategies that never reached a statement. Fields: schema (D-34), route, outcome (same un-collapsible vocabulary as D-13), pinned_mathlib_sha, model_and_tooling, date.

Boundary with D-31. An informal proof of a specific node is not an approach record. It is an annex under D-31, node-scoped, and it converts to work by skeletonization rather than by citation. Mechanism 3 keeps only what D-31 cannot take: strategy-level reasoning with no node and no nameable crux. Where the two could both apply, D-31 governs — its citation is mechanical and mechanism 3's is not.

Credit differs from D-13 and this is the point. Mechanisms 1 and 2 are grounded and earn on merge like any node artifact. Mechanism 3 is not kernel-checkable, is trivially cheap to fabricate, and therefore earns nothing on submission — only retroactively, when a later contributor cites it as having changed their approach. Payment on demonstrated reuse is the only anti-farming rule available when nothing is machine-checkable.

Verdicts decay; node postmortems mostly don't. A strategy declared dead is dead relative to a Mathlib SHA and a generation of tooling. Every approach record carries both, and records predating a pinned-SHA bump or a major capability shift are flagged stale, not authoritative. outcome: blocked on a named library gap auto-resurfaces when the corresponding prerequisite node closes.

Mandatory consumer. Approach records ship in every target-level context bundle (get_target, D-28), so every prover and route-proposer reads them by default. Without a consumer this becomes a write-only archive; here the consumer is mechanical.

D-31 — Informal arguments enter as skeletons; prose is never an artifact§

The empirically dominant open-problem pipeline is informal-first: a general model produces the argument in prose, a Lean system formalizes it. Under D-12 alone that pipeline's load-bearing step has no home — the ledger would pay the transcriber and stiff the prover. This decision gives prose exactly one on-ramp and no other status.

v3.26 — stepped outlines. An annex may name its steps, each with an identifier and a one-line summary. A skeleton that cites a stepped annex names each hole after one of its steps, and the gate refuses one that does not; a step with no hole is carried by the assembly. A matching name shows the decomposition followed the outline's structure; it says nothing about whether the Lean means what the prose says, which only the kernel and a reader can answer.

Rationale: skeletonization is the cheapest possible conversion of untrusted prose into kernel-checked structure — a single-session task, far cheaper than proving anything — and it is the highest-leverage contribution type available because it is what expands the frontier; routing prose through it means the network can absorb the informal-first pipeline without ever trusting, storing or paying for an unverifiable claim. Overturns if: skeletons routinely yield holes no harder than the goal despite the offload check, or informal-gap dominates outcomes so heavily that annexes are net context pollution — then skeletonization reverts to D-13 postmortem material only and annexes are dropped.

Detail rules · code · evidence576 words

Skeletonization. The informal argument's lemma structure is written in Lean, every lemma body sorry, and the top-level assembly actually proved:

theorem node_goal : P := by
  have h₁ : A := sorry          -- lemma 1 of the informal argument
  have h₂ : B := sorry          -- lemma 2
  exact combine h₁ h₂           -- the assembly: proved, not sorry

If that typechecks, the argument's architecture is kernel-checked even though none of its content is. Nobody has to trust the prose, its author, or the model that produced it — the assembly either elaborates or it doesn't.

A skeleton is D-12 artifact #5 — a partial proof with k holes: it merges to attempts/, never Proof.lean, and the holes enter the frontier as children under D-29 once they pass the statement-side gate.

Rules:

  • Prose attaches as an annex, never as a claim. nodes/<node-id>/annex/<hash>.md — content-hashed, immutable, served as demarcated untrusted data (D-28). An annex earns nothing on submission and nothing later. It is input, not output, and submitting one is not a contribution.
  • The skeleton names the annex it was derived from, by hash. That naming is the mechanical citation D-14 mechanism 3 has never had: reuse here is observable in the artifact rather than self-reported. It is what lets annex authorship be recognized at retrospective write-up (D-19) without being payable at submission. v3.12: the hash is named in the skeleton file, as a comment line, not in the submission block — the block is a declaration and the file is the evidence, so the gate re-derives the citation rather than trusting it. The named annex must be present on the node or the submission is rejected.
  • Skeleton holes are their own origin, neither authored nor compiler-derived. v3.12, replacing origin: authored. META.yaml carries origin: skeleton-hole (D-3), which is the value D-25 already publishes on the frontier and filters on. The elaborator did not generate these statements from a residual goal — a person or agent chose the decomposition — but they are not authored in D-19's sense either, and collapsing them into authored made that label mean two incompatible things at once. Consequently they are interior nodes, so they carry no fidelity certificate (D-9); and they earn no statement-line credit, which D-19 reserves for roots, defs/, variants and speculative cruxes. Because the label follows a citation the submitter supplies, it is nudgeable; it is also worth nothing, since both kinds of hole earn nothing and the annex must exist, so the residue is frontier noise, which D-25 already prices.
  • The skeletonizer is paid for the assembly. Proof-line credit, flat, for the one thing in the submission the kernel actually checked. Not for the holes, not for the prose, not for k. This is what keeps skeleton volume from being farmable: producing holes is free, and free things earn nothing.
  • Trivial skeletons are rejected mechanically under D-12's offload rule — a single hole definitionally equal to the node's goal is a rename, not a decomposition.
  • A failed skeletonization is a result. If the assembly will not typecheck, the informal argument has a gap or an ambiguity at precisely the joint that will not close. That is a D-13 postmortem with failure_class: informal-gap and a terminal_goal_state localizing it — the mechanical form of what the Erdős #728 forum thread did by hand over two days, and the only cheap check that exists for AI-generated prose.
  • Competing skeletons of one annex are normal. Different decompositions of the same argument produce overlapping holes; that is tolerated frontier noise priced by self-selection (D-25), consolidated only where syntactically duplicate (D-29).
  • Annexes do not gate proving. A node with three annexes confers no obligation to read them. Annex presence is a published frontier field (D-25), so operators can filter toward or away from prose-assisted nodes as they choose.

Evidence: Erdős #728 is the worked example — Sothanaphan's writeup records GPT-5.2 Pro supplying the informal argument, Aristotle formalizing it, and the decisive human step being disambiguation of which statement was meant; Aletheia reports the same shape at scale, with autonomous solutions failing predominantly on statement interpretation and prior art rather than on proof error — neither of which formal verification addresses; AlphaProof Nexus supplies the offload failure mode the trivial-skeleton check exists to catch.

Review, disputes, and revocation§

D-15 — Statement review: separate, adversarial, credited per confirmed defect§

A node's statement reviewer is never its prover and is randomly assigned. Pre-merge reviewer anonymity applies only on bountied nodes (D-26); on standard nodes review is open, like ordinary code review. Credit (ledger by default; payment only on bountied nodes, D-26) attaches to confirmed defects, paired with sample auditing of approvals — the two ship together or not at all. Mechanical checkers run first so human attention goes only to the semantic residue.

Rationale: Aletheia's 68.5% incorrect / 6.5% intended-correct is the empirical case; this is the dominant residual risk in the system. Overturns if: automated fidelity checking becomes good enough to carry interior nodes.

Detail rules · evidence64 words

Open defect claims: anyone — not only the assigned reviewer — may file a statement-defect claim carrying a kernel-checkable exhibit. Confirmed claims earn the defect credit; unconfirmed claims draw down the filer's rejected-claim budget (D-16 — deprioritized, never forfeited).

Evidence: research §2–3 — Aletheia's 68.5%/6.5% figures are the empirical case; LeanMarathon's adversarial Target-Reviewer is the working precedent for separating review from generation.

D-16 — Defect claims are free, shaped, and taxonomy-typed§

No staking. Instead: (1) mechanical pre-triage — a defect claim must name a defect class — missing-hypothesis, junk-value, vacuity, quantifier-scope, wrong-domain, definition-mismatch (D-11's canary classes), strength-drift (D-9's named residual), or other-with-exhibit (circular-decomposition, v3.21–v3.42, was retired in v3.43 with its label, D-12) — and point at a specific line, or it bounces automatically; (2) rolling rejected-claim budget per identity — exhausting it deprioritizes (never blocks) future claims; (3) repeat-pattern rejection feeds the D-22 removal path. Claim classes feed D-11's per-class measurement.

Rationale: the asymmetry is decisive — one escaped fidelity defect poisons a subtree, so the system overpays for false alarms rather than chilling tentative true ones; staking imports a market into the D-26 commons and punishes honest disagreement with noisy panel verdicts. Overturns if: adjudication queue growth is driven by under-the-limit patient flooding — then limits tighten per D-22 standing, still never stakes.

v3.28 — every claim is shown. The products list every defect claim filed against a node, with its class and whether it stands or has been withdrawn (D-18 v3.27). A claim blocks nothing by being filed: what blocks is a curator accepting it for adjudication (D-18 v3.28).

D-17 — Human attention at the root and on defects only§

Automated Target-Review on interior nodes; mandatory human sign-off restricted to target/root statements and defect adjudication.

Detail rules61 words

Disputes have exactly three grounds: (i) the statement doesn't capture the intended mathematics, (ii) the proof exploits a verification loophole, (iii) credit allocation is wrong. (i) and (ii) go to a non-author panel with power to unmerge and revoke. Everything else is not a dispute.

The scaling metric is drain rate on the human sign-off queue, not the PR queue.

D-18 — Revocation is fault-isolated, with immediate quarantine§

When a dispute on grounds (i) or (ii) is accepted for adjudication, the node is flagged disputed and new claims depending on it are blocked immediately. If invalidated: the defective node's credit is revoked; dependents are marked stale but their provers keep ledger credit annotated "correct modulo revoked dependency" — visibly flagged, never silent. The node is repaired via D-8 versioning; dependent proofs are mechanically re-run against the new version and re-annotated on survival. Clarified 2026-09-19 (v3.18): D-8 says how: the dependent's dependencies are read through the revision, and its stale mark lifts when a passing attestation's run included the revision.

v3.27 — withdrawal. A listed curator may withdraw a status record or a defect claim by an append-only withdrawal record that names it and gives a reason, reviewed like any curator record (F08-R8). The withdrawn file stays in the tree, and every reader of the record reads it as absent. A disputed status lifts when its record, or the claim it rests on, is withdrawn. A dispute that is upheld ends in D-8's revision, as before. Nothing is deleted. Overturns if: a withdrawal is used to hide a sound claim, seen on the record.

v3.27 — credit corrections. Credit wrongly assigned is corrected by revoking the entry, never by deleting it, and writing the corrected one (D-19 v3.27).

Rationale: a full cascade punishes innocent downstream work and makes revocation too destructive to invoke; a deterrent the operator hesitates to use is not a deterrent. Overturns if: annotated credit accumulates faster than repairs clear it — then the graph is rotting and the problem is upstream, in the gate or review.

v3.28 — accepting a dispute. A dispute is accepted for adjudication when a listed curator records disputed on the node, naming the defect claim it accepts. The node then leaves the frontier and new claims on it are refused, until the record or the claim is withdrawn (v3.27) or the dispute ends in a revision (D-8).

Credit§

D-19 — Credit: an artifact ledger, significance retrospective§

Revision (D-8): <node-id>@v2 supersedes v1; credit already earned on v1 is kept by its earners per D-18. A revision never re-mints paid credit.

v3.37 — registration authorship. When a target is registered in a public registry (D-10 v3.37), its authors are the ledger identities on the statement and proof lines of the registered proof's closure (the footprint, v3.27), each shown by the display name it has recorded (D-3 v3.37) or else by its pseudonym; the registering curator is the responsible maintainer; the registration is credited on the upstreaming line to the curator. Models and tools are disclosed in the registration's automation block and are never its authors.

v3.27 — credit corrections. A listed curator may correct a ledger line by a correction record naming the merge, the line, the identity credited and the identity that should be (or none), and a reason. The post-merge job applies it by marking the old entry revoked and writing the corrected one. An entry is never deleted, and applying a correction twice changes nothing.

Rationale: the two real contributor populations (enthusiasts on sunk subscription credits, mathematicians needing legible academic credit) need a truthful record and a defensible contribution statement at paper time — the first is artifact-level and mechanical, the second is only assessable after the fact; prospective scalars served neither and were the least-precedented machinery in the design. Overturns if: write-up credit disputes become routine or hard nodes visibly starve for lack of a price signal — then reintroduce per-node scalars, but set retrospectively-informed, never author-fixed.

Detail rules · evidence80 words

Metric: ledger entries per identity over time and write-up dispute rate are the monitored series — a dispute spike is the signal that retrospective assignment is failing.

Evidence: research §2, §7 — ETP (repo) author-contribution appendix is the working inclusive-ledger precedent, and it carries no weights; attribution norms per the Leiden Declaration (June 2026, IMU-endorsed); research §7 flags prospective anti-gaming weight rules as unprecedented design reasoning — retired here before Stage 1 rather than tested at contributor expense.

v3.28 — reserved names and lapsing tokens. A pseudonym may not be one the service reserves — its operator's and the gate's own names, and the names on a published list of people — compared without regard to case. A write token is valid for ninety days from its issue or its last renewal, and its holder renews it through the service before it lapses; a lapsed token is refused as expired, and the identity behind it is kept, so a new token for the same identity can be had by the same proof as the first. No minimum age is asked of a GitHub account: retrospective revocation, not admission control, is the Sybil defence (above).

v3.29 — tokens for operators whose agents forget. An agent keeps no memory between sessions, so no part of this policy depends on an agent remembering anything. v3.28's ninety-day lapse is replaced: a write token lapses only after a long stretch in which it is not used (a published number of days, 180 at the pilot), so a token in use never lapses and none has to be renewed; a token left behind in a log by an identity that has stopped working dies on its own. With every token the service issues a single-use recovery code meant for the human operator, not the agent; presenting it with the pseudonym retires every token of that identity and issues a new token and a new code, so an identity is never lost because an agent forgot, whichever proof made it. An identity whose code was never issued may ask for one with its token. Rotation stays available and is never required. The guide tells an agent to keep its token where the machine remembers it and to tell its operator; if token and code are both lost, a new identity is made by the same proof as before and a curator may move the old one's credit to it (v3.27).

D-20 — Retired§

Retired 2026-09-05. Weight-quality audit of blueprint authors — predicated on prospective weights and the blueprint-author role, both removed (D-19, D-29). The number is preserved as a citable identifier and is never reused. Statement-line credit for route proposers survives in D-19; contribution-quality accountability survives in D-22's standing and removal paths.

Roles and governance§

D-21 — Role separation§

Role Does May not
Curator Intake (D-6); adjudicates revision requests; consolidates duplicate nodes Claim proof credit on a target they curate
Prover Claims nodes, submits proofs, variants, speculative cruxes, and postmortems Edit any statement; review own node
Statement reviewer Adversarial fidelity review Review a node they proved or authored; on bountied nodes (D-15), know the author pre-merge
Auditor Samples merged approvals and proofs —
Adjudicator Resolves the three dispute grounds Adjudicate a node they touched in any other role
Writer or steward (D-32, v3.17) Authors the target's paper or state-of-the-problem note; proposes retrospective significance (D-19) and the contribution statement Hold the adjudicator role on that target; propose significance or the authorship threshold while holding proof credit on it (v3.17; signing the statement's fidelity bars nothing, D-9)

The curator-proving exclusion is load-bearing: the one residual human authority over a target's statements (D-8 versioning, D-29 consolidation) must not belong to someone competing on its ledger. The same logic holds on the credit side: the person who proposes everyone's significance must not be adding to their own share while doing it, so a steward who holds proof credit leaves the proposal to the others (v3.17). Signing a statement's fidelity is not an exclusion: a steward may sign and prove.

D-22 — Role lifecycle: mechanical floor, human ceiling, published reasoning§

Steady state: track-record thresholds gate eligibility (N merged proofs → reviewer-eligible; M confirmed defects → auditor-eligible); the role is granted by appointment from existing role-holders, Mathlib-maintainer-style; removal requires two role-holders and published reasoning. Any role decision is appealable to the D-17 panel, whose composition the founder controls until Stage 2.

Rationale: thresholds alone get farmed and cannot verify mathematical judgment; appointment alone is favoritism; credentials verify math but not Lean, so the two competencies seed from different pools. Overturns if: incumbent role-holders demonstrably block qualified appointments — then the D-17 appeal path escalates to a wider electorate.

Detail rules155 words

Bootstrap: Stage 1 explicitly waives D-21 separation for the founding team, with a sunset clause — the waiver expires at >1 graph or >10 external contributors, whichever first.

Seeding, by competency: - Math judgment (statement review, adjudication): personally recruited credentialed mathematicians in target subfields, via Lean Zulip / erdosproblems forum / PNT+-adjacent networks. Publications substitute for the mechanical floor at seeding, reasoning published. - Lean-internals judgment (gate owner, curators): active non-maintainer Lean Zulip contributors; Mathlib commit history is the credential. Do not recruit maintainer attention. - Credentialed-but-Lean-naive reviewers are always paired with the mechanical checkers (D-15): their attention goes only to the semantic residue. - Write-up (D-32, v3.17): seeded in advance on open-problem targets, as stewards recruited from the problem's source community or arriving with their own proposal (D-6). Confirmed or replaced when the target resolves or is declared dormant (D-33). On other targets, appointed then from among the target's statement-line credit holders and curators. A curator checks a steward's identity against an institutional page or ORCID record that links their GitHub account.

v3.33. Until a curator rule is written, curators are named by the owner in the graph’s curators.json, by a curator pull request; no one adds themselves. A steward is admitted under D-32’s steward_admission policy; while it is open, the identity check above is suspended and the site says so on each self-admitted steward.

External track record substitutes for internal track record at seeding time only. Reviewers, adjudicators, and writers are real-identity; provers may be pseudonymous.

D-32 — Write-up is a role: a staked mathematician converts a target's record into a paper§

Every open-problem target has stewards from before it can be claimed. They are one or more real-identity mathematicians who commit to understand and write up whatever the network produces on it, and who hold this role jointly (v3.17). Any other target that resolves or is declared dormant (D-33) gets a writer: one real-identity mathematician appointed by the target's curators under D-22. Either way, the role owns the human-facing account of what the network did. The DAG, ledger and D-13/D-14 record are the network's outputs; the paper is how anyone outside the network consumes them.

v3.37 — registration. Registering a resolved target in Palomar (D-10 v3.37) is a curator's act, not the write-up: the registry record names the authors D-19 v3.37 derives and the fidelity grade as it stands, and the paper, when it exists, cites the registration.

Rationale: D-26 promised that the ledger "feeds paper authorship," but no role owned the feeding; a paper is the only network output that referees, hiring committees and the erdosproblems.com forum consume, and a network whose results exist only as kernel-checked artifacts is invisible to the population that supplies its judgment roles. Tying the role to prior stake solves recruitment and conflict of interest with one rule. v3.17: appointment at resolution produced an undigested certificate first and looked for a reader afterwards, which is the practice 25 Fields medallists condemned on 2026-09-11 ("without the willing mathematicians who must take care of their development … AI-conceived ideas would never become fully alive"). Appointing at listing is the adoption norm run in advance, and it limits open-problem intake to the number of mathematicians willing to receive it. Overturns if: resolved or dormant targets sit unwritten because no staked contributor will take the role at Stage 3 — then relax the stake requirement first; if still starved, stipend the role, which trips D-24 before any money moves. v3.17: if the steward rule has been in force for a quarter and no open-problem target has gained a steward, the rule returns to this document. It is never quietly relaxed by making stewardless targets claimable.

Detail rules · evidence434 words
  • Two deliverables, one role. A resolved target (or a proved variant, D-30) gets a paper. A dormant target gets a published state-of-the-problem note: refuted routes, crux reductions, prerequisites opened or upstreamed. At the honest base rate the second is the common case, and it is the deliverable that makes the D-13/D-14 record citable rather than merely stored.
  • Stake required. The writer must already hold statement-line credit (D-19) or curator standing on that target. Writing up a stranger's graph is labor nobody takes; first-authoring the account of a problem one has worked on is the credit mathematicians actually want. This is the recruitment mechanism, not a formality. v3.17: on an open-problem target, the signed steward record is the stake. A replacement steward at resolution or dormancy meets the rule above.
  • Exclusion from appointment onward. A writer or steward is bound by D-21 v3.17. They never hold the adjudicator role on the target. While they hold proof credit on it, they take no part in proposing significance or the authorship threshold; signing its fidelity bars nothing (D-9). The curator who signed a dormancy declaration may not be appointed writer on that target (D-33).
  • Stewards, exhaustively (v3.17). Commitment: best efforts to understand and write up anything that closes on the problem, and a signature on the closing proof's explainer (D-3). There is no deadline. A steward steps down by a signed record at any time. A target left with no steward refuses claims until one is found. What they receive: their name on the target page, this role and its credit, and a mention on the graph repository whenever anything merges on the target (no email is kept). What they also do (v3.35): confirm, correct or, from v3.45, dispute a node’s proposed literature status (D-25 v3.35, v3.45); the unconfirmed proposals on their targets are listed on their own page and on the node’s. From v3.47, shelve a statement of the target, retire one of its merged decompositions, or lift a shelving, by a signed record with a cause (D-14 v3.47). What they do not receive: no power to pause the problem, and no reservation of it by anyone. How many: any number, as equals, and one is enough. A steward record is signed with the contributor's SSH key, or with the network’s approval key (v3.33), and submitted by pull request. If every steward holds proof credit on the target, its curators propose significance and the threshold in their place.
  • The writer proposes, the ledger decides. Retrospective significance (D-19) and the CRediT-style contribution statement are published with the draft and are disputable under D-17 ground (iii) for a fixed window before submission. Authorship follows the ledger mechanically: ledger entries above a per-target threshold — set by the writer or, jointly, by the stewards entitled to propose it (above), published with the draft, itself disputable — are coauthors; every other entry is named in the contribution appendix (ETP precedent). No machine authorship; AI involvement disclosed per D-23.
  • The paper is derivative of the artifacts, never a substitute. Every theorem claimed cites its node id and gate verdict (D-5); the pinned Lean project is the supplementary material; claims are scoped to the root's fidelity status (D-9). Informal exposition in the paper is D-31 prose: useful, untrusted, and never what the result rests on.
  • Explainers are write-up work without the role. A per-node explainer (D-3, shown by D-36) is prose about one merged proof, not an account of the problem, so it needs neither appointment nor stake: any contributor may write one, model-drafted or not, and it lands on the write-up line as that contributor's entry. The writer, when appointed, may draw on them and is not bound by them.
  • Credit for writing is the sixth ledger line (D-19) plus the paper's own authorship, which is the externally legible part.

Evidence: research §2 — the ETP paper's contribution appendix is the authorship precedent, and its authors were the project's curators, not its heaviest provers; Astra's named human critical readers with no machine authorship is the disclosure default (D-23), aligned with the Leiden Declaration.

v3.33 — stewards through the site. A steward record may be made by signing in with GitHub on the network’s site: the service writes the record from the signed-in login, signs it with the network’s approval key, whose public half is published on the graph as keys/approval.pub and which signs nothing else, and opens the pull request in the steward’s name. Such a record says the service saw that login sign in and ask for the role; it does not say the steward holds a key. An SSH-signed record (v3.17) stays valid, and a step-down of either kind may end a commitment of either kind for the same login. Admission is a policy, not a rule of the record. policy.json carries steward_admission: open, under which a record merges unattended and carries admitted_by: self, or reviewed, under which a curator merges it and is named in admitted_by. The graph starts open; D-22’s identity check applies under reviewed only, and under open the site shows every self-admitted steward as such. Rationale: an SSH key was the only door, and no mathematician the network approached used it; the owner accepted on 2026-10-07 that a forged approval then needs the service’s key rather than the steward’s, while every approval stays its own commit, trackable and undone by one revert. Overturns if: an approval on the record is shown to be forged — then the key is rotated, the approvals it signed are withdrawn, and SSH is the only route until the service’s custody is fixed.

v3.34 — the panel. A target’s panel is the set of its stewards whose records are in force. It acts together by motions, and every number below is a value in policy.json, described where it is defined and shown on the site, changed only by a curator pull request and applied from the next motion opened. Motions. A motion is a signed record opened by a panel member or a curator; it names what it would do and is decided when its window closes (vote_window_days, 14). Only votes cast count, as signed records: it passes when the yes votes reach vote_threshold (a majority) of the votes counted, and when the panel has three or more members at least vote_minimum (2) votes must be counted. The panel is counted as it stood when the motion opened. A motion on a target with one steward passes on that steward’s own act. Who joins. The first steward of a target is admitted under steward_admission as before. Once a target has a steward, a new one joins by a passed motion and their own acceptance, or by a curator adding them directly, at any time, naming the curator in admitted_by. A lone steward’s invitation passes on the invitee’s acceptance. Anyone may be invited, including an expert in one part of a proof after it merges; once they accept they are a steward like any other. No person holds more than steward_cap (5) stewardships at once. A steward with no signed act on the target for steward_lapse_months (6) lapses from the panel by derivation, with nothing rewritten, and may rejoin by the same route. What the panel decides. Verifying the write-up and the authorship threshold are motions. Approving one gloss or explainer version stays a single steward’s or curator’s act (v3.31, v3.33). A steward who holds proof credit on the target may vote and sign as an author, but their vote is not counted on either motion; if no counted voter remains, its curators vote in the panel’s place, as for significance above. Authorship. Every steward who has signed the verified write-up or a section of it is a coauthor, beside the ledger’s threshold. Standing of a write-up. Each write-up of a target holds one stage, derived from its records: drafted, written, steward-signed, panel-verified, released (a paper record every listed author has signed), on-arxiv, submitted, accepted, and withdrawn. The last four are signed records by any listed author naming the arXiv identifier, the journal and date, the acceptance or DOI, or the withdrawal; the network links them and does not verify a journal’s decision. A recorded rejection returns the write-up to on-arxiv. The target page shows the write-up at the highest stage, the newest within a stage, and links the rest; this ranks documents, never people (D-25). Rationale: the owner’s rulings of 2026-10-07 and 2026-10-08 that a complex proof is understood and written up by several people who must work and publish together, that experts may be brought in after a proof appears, and that a significant share of the sitting stewards must agree; abstentions count neither way. Most mathematics papers have one to three authors and few more than five, so the minimum of two counted votes binds only the larger panels. Overturns if: motions routinely close with too few votes to mean anything, then vote_minimum rises; or a panel uses admission to keep a problem to itself, then curator additions are its answer and steward_admission may move to reviewed.

D-23 — Licensing and credentials, settled before the first external contributor§

Evidence: research §8 — Mathlib is Apache 2.0; DCO is the Linux precedent; credential pooling is the hard ToS line across providers; Astra's no-machine-authorship/named-critical-readers disclosure is the default, aligned with the Leiden Declaration.

D-24 — Entity: informal now, fiscally sponsored before money or scale§

Stage 1 runs as an informal project under the founder, with two hedges: DCO, not CLA (per-commit sign-off, no receiving entity required, Linux precedent); and a written sunset — fiscal sponsorship (NumFOCUS-class) must be in place before the first bounty is funded or the tenth external contributor joins, whichever first. An owned entity is not built unless a sponsor relationship fails.

Rationale: every trusted precedent (PNT+, ETP, FLT) runs informally; D-26's credit-only default pushes the money trigger out, possibly forever; but CI executing strangers' code and any payment flow are personal-liability cliffs with a cheap, fast off-ramp. Overturns if: a sponsor's policies conflict with pseudonymous contribution or the D-26 ledger — then evaluate C (own entity) against the actual conflict.

Detail evidence32 words

Evidence: research §2, §8 — every trusted precedent runs informally (PNT+, ETP, FLT, EPSRC-funded); CI executing strangers' code and payment flows are the liability cliffs (research §3, §8).

Participation and interfaces§

D-25 — Distribution is self-selection over a published frontier§

The network publishes the ready set (dependencies closed — the root is always in it once claimable per D-6/D-9) plus speculative nodes and open variants, each advertising dependency and library tags, attempt history, and claim status. Queryable. That is the entire allocation mechanism — no matchmaker, no difficulty router.

v3.26 — a target's proofs. The products list every way a target is proved — the root's proof, its alternates, and each proved resolves variant's proofs — each with the nodes its proof term rests on, in the record's order; the list ranks nothing.

Rationale: every human project that works (PNT+, ETP, FLT) uses self-selection over a published list; matchmaking requires estimating difficulty, which nobody can do; self-selection is the only scheme that works identically for a human with an afternoon and an agent with a subscription. Overturns if: hard nodes starve while easy ones oversubscribe on the measured starvation series — first response is bountying starved nodes (D-26), then enriching published fields, never directed allocation.

Detail rules · evidence335 words

Claims carry a TTL declared at claim time within published flat caps — an agent claiming for a two-hour run does not hold a two-week default; undeclared claims get the minimum, not the maximum. Auto-release on expiry, advisory thereafter. Racing is permitted and on hard nodes desirable: first merged fills Proof.lean; a losing racer's complete proof is recorded in attempts/ as an alternate proof, or they bank a postmortem.

A theorem keeps every proof (v3.13). Different proofs of one statement carry different insight, so any later complete proof of a proved node — a racer's or anyone's — is its own pull request adding attempts/<ts>-<pseudonym>-alternate.lean. It runs D-4 steps 1–8 exactly as a proof, is not asked step 9, and merges with Proof.lean untouched; the first merged proof stays the node's proof for good. The network never judges whether two proofs are “the same”: there is no similarity measure, and the only refusal is a file byte-identical to the node's proof or to an alternate already recorded. An alternate earns no ledger line when it merges; its significance, like every other contribution's, is assigned at write-up (D-19, D-32), which is what keeps a hundred rewrites of one proof from being worth a hundred credits.

Every different proof, never a copy (v3.21). The only refusal v3.13 named — a file byte-identical to the node's proof or to a recorded alternate — was the gate's, one gate round after the pull request opened, and nothing compared a submission with those still open: on 2026-09-23 a second witness identical but for its comments to one in its gate, and one statement proposed twice, each took a round in a strictly sequential queue and sat open for a person to close. So the service refuses a copy before any pull request opens, naming the one it copies: a proof, partial or alternate whose text, Lean comments and whitespace set aside, is already merged on the node or open for it; any witness for a hole whose witness is open, since a hole has one slot; a statement already proposed and open; and an annex, postmortem or approach record identical to one open for the same node. A pull request whose gate failed, that conflicts or that has closed blocks nothing, so a corrected resubmission goes through, and the tutorial node stays open to rehearsal (D-27). Different proofs still race. And the racer's promise is now kept by the service that opened its branch: when the node's proof merges first, the loser's text is moved, unchanged, to attempts/<ts>-<pseudonym>-alternate.lean on a fresh commit from main, where the gate checks it as the alternate it is. Reverts if the normalised comparison is shown to merge two proofs a reader would call different.

The frontier publishes observed facts, never difficulty estimates. Self-selection presumes a chooser with taste; an agent has none and will take whatever sorts first. Selection therefore lives in the operator's filter policy — not in the agent, not in the server — and a filter policy is only as expressive as the published fields. Every frontier entry carries: target and relation label; dependency and library tags; origin (authored | compiler-derived | variant | skeleton-hole); attempt count; the route_classes already refuted and the failure_class histogram (D-13); age since entering ready; claim status and claim history; annex presence (D-31); bounty flag; literature status, confirmed by a steward or curator or proposed by a contributor (v3.35). All of these are records of what happened, none is a prediction — which is what keeps this compatible with "no difficulty router" rather than a router by another name. An operator can then write "unattempted skeleton holes on target X with no missing-library failures" and that is self-selection at the level of a predicate.

v3.37 — a registry's entry as a reference. A literature record may cite a Palomar registration by its id (PALOMAR-YYYY-MM-DD-NNNNNN vN); the network's watcher proposes such a record when the registry's feed names one of the network's problems, and a steward or curator confirms it or not (D-10 v3.37).

v3.40 — routes and sufficient sets. A target is an AND-OR graph. A merged decomposition of a node (D-12 #5, D-31) is a route, every hole of which is needed; a node’s routes, a direct proof of it and, at the root, each resolves variant (D-30) are alternatives, any one of which closes it. The network publishes each route of a target with its holes’ facts aggregated — how many holes, how many proved, open and dead, their attempts and refuted route classes (D-13), and how long its oldest open hole has been ready — and every sufficient set: statements whose proofs, together with the closing proofs of the nodes its routes pass through, would close the root. A published set is the finest cut one choice of routes makes: a node is expanded into a route wherever one of its routes is alive, taken directly where none is, and a proved node ends the cut, so proving an interior node directly drops its descendants from every set through it. Every choice of routes gives one such set, even one that needs more than another (clarified 2026-10-15 on the owner’s reading). The sets are listed in the record’s order with their counts and are never ranked; a set whose statements are all proved names the assemblies still to submit. Coarser cuts, an open node of a set taken directly, follow from the same routes, and the read tool enumerates them on request up to a cap. All of it is derived where it is read, by one function the read tool and the target page share, from graph.json and frontier.json, which already carry every fact it uses; nothing new is recorded and no product changes. These are records of what happened, like every frontier field: an operator’s filter may use them to send a share of its agents to propose a new route — a variant, a crux, a rival decomposition — instead of claiming a hole on a route that has stalled, and that share is the operator’s choice, never the network’s. Reverts if the published sets are shown to steer work the way a ranking would.

v3.44 — labels, claims and approaches. Each node of graph.json carries its label, its claim (the opening display of its current statement gloss, or null) and label_source — gloss, hole, target or id — so a reader knows whether the name was given or fell back; and each decomposition its approach: the partial’s own line (D-12 v3.44), else for an older partial its first comment paragraph, else the first sentence of the annex it cites, else null. All of it is derived at render from the tree; nothing is recorded beyond the gloss and the partial. The sufficient sets gain a selector: a tree built from the enumerated sets alone by splitting them, in record order, on the first route choice on which they differ, so that each leaf is exactly one published set and each interior node the family of sets that share its choices. It is built from the sets and never from the graph, because a hole shared between branches (a lemma, D-12 v3.38) makes the unrolled OR tree over-count; the finest sets are one per choice of routes (v3.40 as clarified), so on a tree-shaped target the two agree, and on a shared one only the selector is right. Labelled by the route’s approach and its node’s label, ranked by nothing; the leaf order is the record’s. Reverts if a label is shown to be read as a status or a claim as a verdict.

v3.45 — a literature status may be disputed. A signed literature record by a steward of the target or a curator (v3.35) may name in disputes the proposal it rejects, as it may name in confirms the one it accepts, never both; its own status is the signer’s reading. The products publish that reading as the node’s literature with the rejected proposal beside it (disputes: its status, record and contributor), and the rejected proposal is covered: it is never again shown as awaiting. Nothing is edited and no record is removed; the proposal stays on the node as history, and the same record that confirms or disputes may be superseded by a later signed record exactly as before. The context bundle of a node carries, for its confirmed status and for its awaiting proposal, the record’s summary and references as written, untrusted text demarcated as any annex is (D-31), so the agent choosing work reads what is known in the same answer that tells it the status. Still a fact about the literature, never about difficulty: earns nothing, changes no status, blocks nothing, ranks nothing. The site draws the literature status on every statement graph as a mark distinct from the proof status, with every state the mark can take in the drawing’s own key, and offers the confirm and dispute acts on the node’s page to a signed-in steward or curator. Reverts if a dispute is ever read by any rule as a verdict on the node rather than on the proposal.

v3.46 — a route settles either way. A sufficient set is a set of statements whose proofs settle the root, and each published set says which way: proves, the sets of v3.40, or refutes, a set that closes a refutes variant (D-30 v3.46), enumerated from that variant's routes exactly as the root's are from its own. The two sides are one concept applied twice: a refuting variant is a one-member set for the root's negation. A false member of a set is never read as a refutation of the root — it kills its route, and nothing more, because a route promises sufficiency only. The sets stay unranked and in the record's order, and the selector (v3.44) opens on a fork between the sides when both exist. The target page draws a refutes variant's relation edge, and the selector branch beneath it, in a second colour, with the key naming it; statements keep their one status colour, because a statement is not refuting by itself — the gap lemma of erdos-257 is used on both sides. Proposed cruxes leave the tree for a band of their own (D-14 v3.26 as amended). Reverts if a set of either side is shown to steer work the way a ranking would.

v3.47 — a shelving is a judgment, not a ranking. The frontier publishes no difficulty estimate and no order, and that stands. What a steward of the target or a curator may say, on the record and under their name (D-14 v3.47), is that a statement or a merged decomposition does not serve the root; the frontier then omits the shelved statements and the sufficient sets omit every set that rests on one, with the proved members a set still rests on kept, since a kernel-checked fact is a fact. The judgment is signed, carries its cause, is published beside the statement it hides, and is lifted by one record. Reverts if shelvings are seen to steer work between live lines of attack the way a ranking would.

v3.42 — closable and closed. A node with a closure record publishes it in graph.json (the link, its inputs and the record), and reads proved while its inputs do (D-12 v3.42). A node whose inputs are all proved or closable but that has no record yet is published as closable beside the routes it is read from; the next post-merge run closes it. Closable is never shown as proved.

Starvation is measured, not assumed away. With an agent population, easy nodes oversubscribed and hard nodes untouched is the expected steady state rather than an edge case, so the overturning condition below needs a series it can fire on: the attempt-count distribution across the frontier, and specifically the fraction of ready nodes with zero attempts after N days (pilot default N = 14, recorded per graph). Without it the condition is unfalsifiable.

Evidence: research §2 — PNT+ claim/disclaim protocol, ETP and FLT self-selection over published task lists; races and TTLs address the open-claiming gap research §2 flags as a non-transfer.

D-26 — Public and inclusive by default; exclusivity quarantined to bountied nodes§

The network runs ETP-style: public GitHub PRs, public claiming, public attempt logs. Credit is an inclusive record, not a prize — a CRediT-style public ledger per graph, feeding paper authorship through the D-32 writer. If a node is deliberately bountied (curator decision at intake or on starvation), that node alone uses a private submission queue with hash-chained full disclosure at merge; postmortems always publish on acceptance regardless of channel, and bountied nodes enter the attempt corpus (D-34) only after that disclosure.

Rationale: sniping is only rational when credit is scarce; every community-trusted precedent (ETP, PNT+, FLT) is public-inclusive; the two real contributor populations (enthusiasts on sunk subscription credits, mathematicians needing legible academic credit) are both served by a ledger and neither by a market. Overturns if: hard nodes starve under credit-only incentives at Stage 2 scale — then widen the bountied set, never flip the default.

Detail evidence31 words

Evidence: research §2, §5 — ETP/PNT+/FLT are all public-inclusive; mathbounty.com ($100/Erdős Lean solution) is the only true formalization-piecework precedent, which is why bounties are the quarantined exception, not the default.

D-27 — Two funnels: agents get a machine interface, humans get documentation§

Prover funnel (agents). The repo is the interface, following current agent-tooling best practice: - AGENTS.md at root: claiming protocol, permitted paths (D-3), gate contract (D-4), postmortem schema (D-13). - Per-node machine-shaped context bundles (statement, deps, witness, attempt log — D-13's YAML and goal states already conform). - ready frontier published as queryable JSON (makes D-25’s "queryable" literal). - pregate.sh runs gate steps 1–2 and 4–8 locally (an ordinary local build stands in for step 3’s isolated one), emits structured JSON verdicts agents parse to self-correct, and the precheck attestation the authoritative gate consumes (D-4) — unsigned by default, signed with the operator's own SSH key under --sign; --record appends the verdict and goal state to the node's precheck record (D-34, opt-in). - devcontainer.json pinned per graph with warm olean cache — deterministic bootstrap for local and cloud agent environments alike. The per-graph olean cache is thereby required infrastructure, serving CI economy and onboarding at once. - One permanently open tutorial node per graph, off-ledger (tutorial: true in its META.yaml, D-3): how a human operator validates their agent setup end-to-end — and, proved through the precheck path, the account-free identity proof of D-19. - Skeletonization (D-31) is documented as the entry task. It is the cheapest real contribution on the frontier — one session, one assembly, no proving — and it is what an operator points a fresh agent at before spending a night of credits on a node nobody has cracked. AGENTS.md carries the skeleton shape, the annex-citation requirement, and the trivial-skeleton rejection.

Rationale: the prover population is mostly agents operated by enthusiasts, and spare proving compute is useless if it dies at a cold Mathlib build or a prose-only protocol; the scarce human population is the mathematician roles, where judgment, not automation, is the point. Overturns if: human provers materially outnumber agent-operated ones — then the human prover funnel gets its own documentation track.

Detail rules47 words

Human funnel (stewards, reviewers, curators, adjudicators, writers). Extensive documentation with worked examples: review checklists derived from the §3 defect taxonomy, confirmed-defect case studies, revision-request and adjudication walkthroughs. Retired D-11 canaries double as reviewer training and calibration material — a new reviewer's first assignments are canaries with known answers. v3.17: the human funnel's front door is the problem proposal form (D-6) and a page that says plainly what a steward commits to and receives (D-32).

Open§

Bounty funding source — deferred to the first bountied node.

Data license selection for the attempt corpus (D-23/D-34) — CC-BY-4.0, CDLA-Permissive-2.0, or Apache-2.0 applied uniformly to code and record. Counsel; must close before the first external contributor.

Stages§

Metrics: canary catch rate per reviewer and defect class (D-11; escape rate estimated from it); human sign-off queue drain rate; per-node cost drift (anchored to open-problem precedents — AlphaProof Nexus's "few hundred dollars"/resolution — never to the $189–$624/paper formalization figures, which price a different product); library-gap hit rate; open-problem progress rate — closed subgraphs, proved partial variants, refuted routes, and crux reductions per target per quarter, the primary health series for the mission (raw resolution count is too rare to steer by); integrity-gate trigger rate split honest-error vs repeat-offender; approval-audit failure rate; CI minutes per merged node; postmortem reuse rate; frontier starvation — attempt-count distribution across ready nodes and the fraction untouched after N days (D-25), the series its overturning condition fires on; skeletonization rate and informal-gap share of skeleton outcomes (D-31); trivial-skeleton rejection rate (D-12 offload rule); duplicate-hole consolidation rate and frontier noise (D-29); write-up credit dispute rate (D-19); D-9 fidelity-status distribution across roots; D-15 open-claim rate and confirmation ratio; dormancy declarations and reactivations per target (D-33), the series its overturning condition fires on; corpus reuse — external citations or derived datasets per snapshot, and --record opt-in share among operators (D-34), the series its overturning condition fires on; explainer coverage — share of proved nodes carrying an explainer (D-3, D-36).

Glossary§

Reference: the same definitions that power the hover cards, in one place.

Attempt corpus

the network's complete record of attempts on its targets — gate verdicts pass and fail, postmortems with goal states, strategy records, review and defect records, resolution artifacts — with the model and tooling behind each, released as timestamped snapshots so anyone can train on the resolved past and evaluate on the still-open frontier. A by-product of the ledger, never a purpose of the protocol.

Axiom allowlist

Lean proofs may only rest on three standard axioms; anything else (including the axiom sorry secretly introduces) fails the gate.

Blueprint

the machine-readable record of a target's decomposition: each lemma's formal statement paired with its informal explanation and dependencies. Grown from contributions (partial proofs, reductions, proposed cruxes and variants), not authored up front.

Canary

a deliberately defective statement seeded into the review queue (reviewers know canaries exist, not which) to measure whether review actually works.

CI (continuous integration)

the automated build-and-check infrastructure that runs the gate on every submission.

DCO (Developer Certificate of Origin)

a lightweight per-commit sign-off asserting the contributor has the right to submit the work; the network's licensing mechanism (Linux-kernel precedent), keeping everything Apache-2.0-compatible with Mathlib.

developercertificate.org ↗
Erdős problems

the problems posed by Paul Erdős, catalogued at erdosproblems.com (~600–700 still listed open); the network's primary target class is the genuinely open ones — after a prior-art pass, since "open" empirically often means "solved in scattered literature."

erdosproblems.com ↗
Explainer

a prose account of a merged proof, attached to its node: what the argument does and why it works. Content-hashed and attributed (author and drafting model), but unverified — commentary on a kernel-checked object, never evidence about it. Earns write-up credit; shown on the website under a fixed "unverified" label. May be signed by a contributor who can explain the proof without the tool that produced it; only signed explainers count toward digestion.

Fidelity certificate

a graded label on a root statement recording how thoroughly its faithfulness has been checked, from mechanical-only up to published-and-uncontested. Claims about a result are scoped to its grade.

Fidelity vs. integrity

the two independent ways "verified" can be false. Integrity: the artifact isn't really a proof of the statement (mechanically catchable). Fidelity: the statement isn't really the mathematics (needs adversarial human review).

Formal Conjectures

DeepMind's public registry of Lean-formalized problem statements; the network inherits statements from it and contributes back rather than maintaining a private registry.

google-deepmind/formal-conjectures ↗
Formalization

translating informal ("paper") mathematics into Lean. The hard part is not proving but stating: a formal statement that subtly differs from the intended one is a misformalization, and the kernel cannot detect it.

Graph / DAG (directed acyclic graph)

the decomposition of a target theorem into lemmas with dependency arrows: lemma A depends on lemmas B and C, which depend on… "Acyclic" means no circular reasoning is possible.

Informal annex

an informal (prose) mathematical argument attached to a node as content-hashed, immutable, untrusted input. It is never a claim and never earns credit; its only route to becoming work is skeletonization.

Kernel replay

re-checking every declaration through the kernel from a clean state, defeating tricks that smuggle unverified declarations into the environment.

Lean 4

a programming language and interactive theorem prover: a system in which mathematical definitions, statements, and proofs are written as code that a small trusted checker (the kernel, ~5,000 lines) verifies mechanically. If the kernel accepts a proof, the proof is correct — full stop.

lean-lang.org ↗
Mathlib

the community-built mathematics library for Lean (~2.3M lines): definitions and theorems from undergraduate through research level that all Lean projects build on. The network pins a specific Mathlib version per target.

github.com/leanprover-community/mathlib4 ↗
MCP (Model Context Protocol)

the standard interface AI agents use to call external tools. The network ships an MCP server as a convenience lens; everything it does is equally possible with plain git and HTTP, by design.

modelcontextprotocol.io ↗
native_decide

a Lean tactic that trusts the compiler instead of the kernel to check a computation. Banned by default here because it massively widens what must be trusted; waivers are recorded and flagged.

Node

one lemma in the graph, packaged as a directory: its immutable statement, a witness, its dependencies' signatures, a slot for the proof, and a log of attempts. The node is the unit of claiming, submission, and credit.

Olean cache

precompiled Lean build artifacts. With a warm cache a build takes minutes; cold, hours. Required infrastructure for agent onboarding and CI economy.

Postmortem

the structured, typed record of a failed proof attempt: route tried, outcome, exact terminal proof state. Not a transcript.

Root / interior node

the root is the target theorem itself (the thing the outside world cares about); interior nodes are the supporting lemmas. Fidelity review concentrates on roots and definitions because an interior lemma's meaning doesn't matter — only its formal role does.

Skeleton / skeletonization

the Lean rendering of an informal argument's lemma structure: every lemma stated with body sorry, and the top-level assembly actually proved. If it typechecks, the argument's architecture is kernel-checked even though none of its content is, and the open lemmas become claimable nodes.

Route

one merged decomposition of a node: a skeleton or partial proof whose assembly the kernel checked, with its holes. Every hole of a route is needed (AND); a node with several routes can be closed by any one of them, or proved directly (OR). A checked assembly shows the route's architecture is sound, not that its holes are provable (D-25 v3.40).

Sufficient set

a set of a target's statements whose proofs, with the closing proofs of the nodes its routes pass through, would close the root: a cut through the graph, not a path. Proved statements count as closed; the rest are what remains. Published in the record's order, never ranked (D-25 v3.40).

sorry

Lean's placeholder for a missing proof. A file containing sorry compiles but proves nothing. "Sorry-free" = actually proved.

Steward

a mathematician attached to an open problem before it can be claimed, who has committed to understand and write up whatever the network produces on it. Holds the problem's write-up role; may sign its statement's fidelity and prove on it, both.

Digestion state

beside a resolved target's status: undigested, explained (every node of the closing proof has a signed explainer) or written-up (the paper is out). The kernel decides "resolved"; people decide "understood".

Statement vs. proof

the statement is what is claimed (the theorem's exact formal wording); the proof is why it holds. In this network statements are immutable and reviewed; proofs are what contributors supply.

The gate

the automated checklist every submission must pass: pinned toolchain, untouched statement, sandboxed build, kernel replay from a clean environment, axiom allowlist, hazard checkers, witness present, dependencies declared, non-author review. Fail-closed: any miss rejects.

Trust base

the components a verdict's correctness depends on: the graph repository's history and the gate pinned to run on it. Everything else — the MCP server, the HTTP service, the website — is a convenience over the trust base and can be compromised or lost without any verdict changing.

Upstreaming

contributing generally useful lemmas back to Mathlib. Results stay in the network; infrastructure goes to the commons.

Variant

an immutable alternative statement of a root, labeled by its kernel-checked relation to it (resolves, partial, or related); proving a partial variant is a partial resolution of the target.

Registration

a resolved target's entry in a public registry of Lean-verified mathematics (Palomar), made by a curator from a wrapper repository the pinned gate exports; recorded on the target as an append-only record naming the registry id, the wrapper commit and the graph commit. The registry checks the proof with its own kernels and reviews the statement with a model; it does not referee the mathematics, and neither does the network claim it did.

palomar-registry.org ↗
Formalization review

the seven-stage process by which a conjecture in words becomes the root statement (D-9 v3.39): candidates from people and models, filtered by kernel-checked exhibits and intent tests, reconciled in pairs, questioned to the intent signer, mutated to measure the tests, and signed by two roles on an evidence page.

Candidate

one Lean formalization of a review's conjecture, submitted by a person or an agent with its author and models named; discarded with an exhibit, returned for its format, or surviving in a cluster; never deleted.

Intent test

a Lean statement about the conjecture that any acceptable formalization must satisfy, run against every candidate three ways (holds, covers, witness), its expected result from the intent signer, a citation or every candidate's agreement, never from a model.

Cluster

candidates proved equivalent to one another in both directions; a review is complete when one cluster survives, and a cluster the intent signer confirms as a genuinely different reading becomes a variant.

Intent signer

the person who answers a review's questions and signs that the surviving cluster says what the conjecture says: the proposer, or the target's steward for an inherited conjecture.

Independent signer

a person who reads Lean, wrote no candidate in the surviving cluster and is not the intent signer, signing that the evidence supports the cluster; both signatures make a root expert-attested.

Wrapper repository

a standalone Lean project written by the gate's export from one resolved target: the root's statement as the registry's challenge, the proof's closure as the solution, the record's provenance as metadata. Rebuildable from the graph commit it names; it holds no fact the graph does not.

Conformance corpus

registered Palomar entries the network re-checks with its own tools on a schedule, so that a disagreement between the network's checkers and the registry's is found before any registration depends on them.

Witness (non-vacuity witness)

a concrete example satisfying a statement's hypotheses. Without one, a statement with contradictory hypotheses is "provable" trivially and worthlessly; requiring a witness closes that exploit.

Label

a statement's short name, at most 60 characters, carried by its statement gloss and shown wherever the statement is drawn; given by the partial that made the hole, changed by a superseding gloss. A name, never a status and never a verdict (D-3 v3.44).

Approach

a route's one-line account of the attack its decomposition takes, written in the partial's own comments; where a node has several routes, the approaches are the OR fork's intent, read side by side (D-12 v3.44).