From a Cold Clone to a Proof Receipt

The cold-clone problem

The first interaction with a large Lean repository is usually a filesystem. The reader sees source files, generated files, scripts, papers, and build configuration, but not the shape of the mathematics. A language model can search filenames and text, yet those operations do not answer the questions that matter: Which programmes exist? Which propositions are established, conditional, finite, or open? Where does a declaration sit in the formal dependency graph? Which surface is exhaustive, and which is a human selection? What may be trusted without compiling anything?

This is not only a convenience problem. When an agent cannot see a library’s option surface, it tends to rediscover existing lemmas, confuse a finite result with its open unbounded neighbour, or build a new local index because the existing one was not discoverable. Conversely, loading every declaration, paper, and proof edge into one prompt destroys the distinctions the extra context was meant to reveal. A useful first-contact surface must therefore be small, expandable, and honest about what it omits.

The development studied here indexes eight open Erdős problems. Problems 249 and 257 are the two principal reviewed programmes; Problems 68, 243, 251, 269, 1041, and 1049 are problem-owned expansion lanes with their own notes and explicit nonclaims. The corpus concentrates its depth around a small number of hard frontiers: exact separation equivalences for Problem 249, a machine-checked rational countermodel agreeing with the totient’s parity at every index, and quotient-greedy classifications for Problem 257, with obstruction theorems recorded beside the routes they close. The generated certificate shards named in the abstract sit underneath these results as checked finite evidence, not beside them as further claims. The design goal is not to replace reasoning with a fixed pipeline. It is to let a capable reader see enough structure to reason well, while reserving mathematical authority for the pinned proof kernel.

A layered mathematical option surface

No single graph can serve all readers without hiding an important distinction. The repository therefore commits four related layers (Figure ). They are projections with different coverage contracts, not successive claims of understanding.

A bounded tour over an unbounded drilldown

The first command returns a six-line card rather than a database dump. It derives corpus scale, formal-graph scale and misses, the authority boundary, the eight-problem map, the open frontier, and the available intent classes from the committed projections. The full packet uses a registry-scaled budget: 18 kB of base context plus 2 kB per indexed problem, hence 34 kB for the present eight-problem registry. It expands the card into a mathematical map, status counts, reader-specific contracts, and typed follow-up commands.

Five intent lenses cover the main transitions:

1. understand the mathematics through a selected programme and its claims;

2. locate any formal object through ordinary-language search followed by exhaustive inventory;

3. inspect exact formal dependencies through proof cones and paths;

4. begin a checked change through the session notary and focused builder;

5. audit the agent and release system through the publication architecture and release gate.

The route logic names no specimen theorem or module. Repository-specific mathematics enters through data: programme rows, claims, declaration records, and frontier propositions. This distinction matters. The mechanism is generic over the repository’s projection schemas, while the current projection content is intentionally specific to the mathematics it describes.

Ordinary-language entry is likewise not an undocumented trigger list. The --vocabulary packet is an executable Rosetta surface: it publishes question operators, aliases, transparent expansions, typed route hints, an all-problem registry projected from docs/problems.json, and a route-discovery lexicon projected from docs/claims.json::machine_readable_paper.entrypoints. A unique exact authored term may take a constant-time fast path; ambiguous or unseen language falls through to visible vocabulary interpretation and ranked corpus search. Every search response records that interpretation, so an agent can inspect how its wording was translated instead of depending on phrase luck.

The packet also answers four different cold readers. A research mathematician gets programmes, claim statuses, and surviving open propositions. A formalisation engineer gets declaration coordinates, exact value references, and a route into a checked change. An AI-lab researcher gets coverage and authority distinctions. An independent contributor gets the no-build orientation, changed-cone build route, and public handoff check. Each reader sees the same facts through a different question contract rather than a separate hard-coded example.

Crossing from navigation to authority

The architecture treats navigation and proof as separate capabilities (Figure ). A static query may nominate a theorem or dependency path. It cannot establish that a proposed application typechecks, that a proof closes a goal, or that an English interpretation is mathematically faithful.

The session notary records a typed move grammar in an append-only ledger: observations, conjectures, plans, interpretations, abandonments, probes, claims, and closure. Conjectures may declare a falsifier. Dead ends remain in the record instead of being rewritten into a linear success story.

A probe is different. The notary stores the exact Lean input bytes, runs the pinned Lean process, and computes one of three verdicts from the process result: accepted, accepted with an admitted placeholder, or rejected. The agent cannot type a verdict into the ledger. A claim must cite an accepted probe receipt; the notary rejects weaker citations. Replay reruns every stored probe and compares the current result with the recorded verdict.

This design deliberately leaves search policy open. LeanDojo couples an open programmatic Lean environment with extracted proof data, premise annotations, retrieval, and a theorem-proving benchmark . Pantograph exposes tactic execution, proof states, metavariables, and data extraction through machine interfaces [5]. Those systems make machine-to-Lean interaction richer. The notary here addresses a complementary question: after an agent chooses its own policy, which parts of the resulting reasoning record are advisory, and which exact claims are grounded by replayable kernel acceptance?

Compilation after comprehension

A committed navigation projection is portable text; an .olean file is a toolchain- and platform-specific build product. A cold clone can therefore orient immediately but must either compile the selected formal target or restore a compatible cache before editing.

The focused build wrapper accepts an exact target, modules changed since a Git reference, or the stale cone derived from Lake traces. It orders the selected modules into dependency waves, limits parallel jobs, and finishes with a serialized Lake authority check. Restored caches use Lake’s content traces rather than checkout timestamps. In one historical four-file addition, the planner selected 26 modules in four waves rather than both complete roots; in a warm two-root dogfood plan it selected no stale modules. The test suite covers trace freshness, changed-file selection, dependency ordering, bounded parallelism, failure propagation, and the final authority check.

The exhaustive dependency-index validator is expensive for a different reason: it traverses the elaborated environment and exports direct references. After a full export matches the committed index, the validator writes an exact receipt below the ignored Lake cache. Its key includes every supported Lean source file, the toolchain and Lake locks, the exporter and builder inputs, the declaration atlas and generated manifest, the formal-source release slice of the claim registry, the dependency-extraction helper definitions, and the committed index bytes. An ordinary check reuses the receipt only while all inputs and output remain byte-identical; an explicit full-check mode bypasses it. A changed formal or exporter input therefore forces a fresh incremental build and full export, while documentation-only revisions and exact cache restores do not.

This is intentionally conservative. The receipt does not claim that the environment export itself has become incremental. It prevents unnecessary repetition when its entire input surface is unchanged. When Lean source changes, Lake still recompiles only stale dependencies, but the graph exporter currently scans the supported environment again.

Dogfood receipt

The committed prospective session is a naturalistic use of the workbench, not a synthetic benchmark. The ledger contains six reasoning notes, one kernel-accepted probe, and two claims bound to that probe. It produced a binary carry-pivot normal form for numeral-adjacent boundary words and an exact divisor-incidence identity that sharpens a previously landed one-sided coefficient bound to equality. At the audited revision, replay reruns the stored probe and returns the same accepted verdict.

The receipt supports a narrow statement: the stored input is accepted by the pinned Lean environment, the cited claims point to that accepted probe, and the result survives replay at this revision. It does not establish that the agent’s route was optimal, that every candidate was searched, that a bounded failure is impossible, or that the mathematics is new outside the repository history.

The navigation surface was dogfooded separately as four audiences. The research-mathematics route reaches the programme map and explicit frontier; the formalisation route reaches a source coordinate and exact proof cone; the AI-lab route exposes exhaustive-versus-selective coverage and receipt authority; the contributor route reaches a focused build and release check. Adversarial tests remove or distort each protected transition and require the cold-clone validator to reject the mutation. This evaluates the declared first-contact contract, not subjective comprehension.

Relation to prior work

Proof blueprints pair informal plans with named Lean declarations and author-supplied dependency links. leanblueprint stores a blueprint in TeX and its checker only confirms that each named declaration exists [1]; it neither infers those links nor checks that the informal and formal statements agree. LeanArchitect infers formal dependencies and proof-hole status and exports synchronised blueprint material [2]. The Carleson project shows a blueprint used as a large collaboration surface. Its public blueprint split the formalisation into about 180 claimable tasks, most corresponding to one blueprint lemma; formalisation feedback produced localized corrections, modifications, and extensions to the mathematical guide, including a few changes to the general setup and main theorems [3]. The present tour has a different first-contact role. It begins after the repository already contains a large corpus, distinguishes exhaustive inventory from authored interpretation, and routes a reader into exact dependency and proof-receipt tools.

LeanDojo and Pantograph provide stronger interaction substrates for learned or scripted theorem proving [4][5]. This work does not propose a new proof-search policy. It makes the policy slot explicit and records enough of an agent-chosen trajectory to separate notes, nominations, rejected probes, and accepted claims.

Nor is its declaration graph or retrieval route novel in isolation. LeanGraph extracts typed elaborator-level edges across Lean projects, while a separate network study analyses Mathlib’s multilayer declaration graph [6][7]. LeanExplore combines semantic, lexical, and graph ranking behind Python and MCP interfaces, and LeanSearch v2 targets global premise sets through iterative sketch–retrieve–reflect [8][9]. The narrower claim here is that one cold-clone contract composes source addresses, selective semantics, dependency cones, incremental validation, and authority receipts without requiring a hosted service or an initial Lean build.

Large-library maintenance supplies the relevant compilation lesson. describes performance-aware library design, deprecation, semantic linters, benchmarks, review tooling, and explicit technical-debt management [10]. The changed-cone planner and receipt cache apply a smaller-scale version of that maintenance posture. The local measurements do not transfer Mathlib’s scale or social evidence.

Lean Atlas narrows the declarations whose meaning can affect selected theorem statements and leaves semantic verification to people . That is close to the authority distinction here: formal dependency can focus human inspection without deciding intended meaning. The cold-clone tour adds a front-door contract across exhaustive inventory, selective semantics, public claims, and agent receipts.

Limits and transfer conditions

This is a case study of one repository at one audited revision. Its projection schemas and routing engine are reusable mechanisms, but another project must supply its own source roots, programme map, claim vocabulary, frontier statements, and authority owners. The paper gives no evidence that a new project can adopt the architecture cheaply or that agents using it outperform agents with an ordinary README.

Counts describe artifact coverage, not mathematical understanding. Direct dependency edges are not proof explanations. Authored semantic nodes may be wrong or incomplete. Maintainer-reviewed claims may also be wrong; automation preserves recorded relationships but does not judge unrestricted prose.

Receipted reasoning is auditable rather than necessarily good. A model may choose unproductive probes, omit a relevant source, or rationalise a dead end. Replay detects environment drift in stored probes but not every flaw in the surrounding interpretation. Context-blind historical experiments also cannot establish training-data blindness.

Finally, the first full project build and the first elaborated graph export remain material costs. The architecture moves them after comprehension, supports compatible cache restoration, and avoids repeating an exact export when nothing relevant changed. It does not eliminate the cost of validating a genuinely changed formal environment.

Authority-preserving agent entry

An agent-native formal repository should not merely contain many proofs. It should reveal, from a cold clone, what mathematics exists, what each navigation layer knows, what remains open, and which next action crosses into proof authority. The architecture here realises that sequence with committed projections, a bounded intent tour, exact loaded-root dependency data, a session notary, focused builds, and cache-bound validation receipts.

The central design choice is separation. Comprehension comes before compilation; nomination comes before application; reasoning notes remain distinct from kernel verdicts; exhaustive routing remains distinct from selective interpretation; and a public claim remains distinct from the formal statement it describes. Those boundaries let a capable agent move quickly without making speed look like authority.

Reproduction routes