Generate a LeanEval workspace for a Formal Conjectures declaration - #4951
Open
williamjblair wants to merge 72 commits into
Open
Generate a LeanEval workspace for a Formal Conjectures declaration#4951williamjblair wants to merge 72 commits into
williamjblair wants to merge 72 commits into
Conversation
github-actions
Bot
added
documentation
This was referenced Aug 15, 2026
Draft
rdivyanshu
pushed a commit
to rdivyanshu/formal-conjectures
that referenced
this pull request
Aug 16, 2026
… one (google-deepmind#4894) **Program lane:** Foundation ## What this establishes `extract_names` currently reports one `formal_proof` per declaration even though a declaration can carry several annotations and assumptions belong to a proof, not to the conjecture. This change introduces the canonical versioned representation: `schemaVersion: 2` with a `formalProofs` list whose entries carry `kind`, `link`, and proof-specific `conditions`. The list is deterministic despite attribute storage in a `HashSet`, `site/build.js` renders every proof with its own conditions, and `FormalConjecturesUtil.Metadata` becomes the shared home for `FormalProofInfo` rather than leaving each tool to infer a shape. ## Dependency and sequence This is the first dependency in the [review, verification, and preservation loop](google-deepmind#4394). google-deepmind#4884 supplies the first real conditional-proof datum. google-deepmind#4828, google-deepmind#4749, google-deepmind#4951, and google-deepmind#4962 must converge on the list-aware schema after this lands; they should not collapse schema 2 back to one proof per declaration. ## Review question Does schema 2 correctly model every proof annotation and its conditions, with deterministic export and correct site rendering, and is `FormalConjecturesUtil.Metadata` the right shared boundary for current consumers? ## Explicit boundary This PR does not update or accept every downstream consumer, does not decide Comparator or preservation policy, and does not imply maintainer acceptance. It introduces no Vela authority or dependency.
williamjblair
force-pushed
the
comparator-workspaces
branch
from
August 17, 2026 03:08
3d838fb to
c8fb28a
Compare
williamjblair
changed the title
williamjblair
force-pushed
the
comparator-workspaces
branch
from
August 17, 2026 17:34
c8fb28a to
aeafd32
Compare
The generated workspace required this repository so Challenge.lean could import the problem's own module. lean-eval vendors its problems and cannot fetch Formal Conjectures at evaluation time, so the statement's dependencies have to travel with the workspace. The hand-built pilot in this branch already had the right shape, `import ChallengeDeps` against Mathlib alone; the generator did not, and the two disagreeing was this branch's main gap. comparator_facts now reports the FC-local closure of a statement in dependency order, and the generator copies it into ChallengeDeps.lean, each declaration inside its own section carrying the open, variable, universe, set_option and local notation in force where it was written. Copying is a construction and its failure modes are ones Lean sees and a reader does not, so --verify elaborates the generated Challenge against this checkout's Mathlib, which is the revision the workspace pins. It found four defects that no amount of reading would have: - Elaborator artifacts. _proof_N and .match_N have no source range because they have no source; copying the parent regenerates them. They are reported separately so a generated constant with no copied ancestor is an error rather than a silent omission. The heaviest FC100 closure is 10 real declarations, not 19. - Constructors and where-auxiliaries carry ranges inside their parent's. EdgeN.mk covers line 88 of a structure spanning 83 to 93, and pmSumListAux._sparseCasesOn_1 has exactly its parent's range, so copying either duplicated a declaration or sliced a fragment of one. - An inductive's fields live in its constructor, so the closure ordered EdgeN before the V it uses and the copy did not elaborate. - answer(False) reached Challenge.lean verbatim. answer is this repository's elaborator, and a statement that already carries its answer has no sorry slot for hoist_answers to remove. Unwrapping to the bare term is faithful: in the default postpone mode the elaborator elaborates the term and attaches an annotation. Copied dependencies keep every attribute except this repository's own, since dropping simp or reducible changes how the declarations after them elaborate. provenance.json is now generated rather than only hand-written for the pilot. The lakefile's requirement was the only record of which commit a statement came from, and removing it would otherwise have left the workspace untraceable. Verified on the ten declarations covering every FC100 dependency pattern and both hole kinds: all ten generate and elaborate. 35 adapter tests pass, 58 across scripts/, ruff no worse than before, lake --wfail build comparator_facts clean.
lean-eval#536 divides this integration in two: lean-eval's generator core
is extracted into leanprover/lean-eval-generator and consumed as a pinned
dependency, and the Formal Conjectures side owns an importer that maps FC
declarations and metadata to LeanEval modules and manifests. The FC
importer does not fork the generation logic.
make_comparator_workspace.py did both halves in one 1,164-line module, so
the extraction would have been a rewrite. Split it along that line:
fc_leaneval_importer.py resolves a declaration against an exact FC
commit, reads the elaborated environment, copies
the FC-local closure, types each answer(sorry)
slot, records the provenance
leaneval_interface.py the two values that cross: one marked-up
Mathlib-only Lean module in labelled regions,
and one problem manifest
leaneval_generator.py the workspace: layout, import graph, scope
placement, lakefile, Solution adapter, config
make_comparator_workspace.py the command that runs one then the other
The generator imports the interface and never the importer, so it can be
replaced by a pinned package without touching the FC side.
comparator/OWNERSHIP.md gives the line counts either side of that deletion,
and the five things lean-eval has to settle before the interface is real.
The manifest now records the FC source commit and declaration id, as
lean-eval#536 requires, and travels into the workspace as manifest.json;
it subsumes the previous provenance.json and holes.json. Every other
generated file is byte-identical to what the pre-split script produced.
--emit-import writes only the pair this repository owns. A new CI step
feeds those bytes back through the generator and requires them to
reproduce the workspace exactly, which is what says the pair is the whole
interface. --verify now elaborates the marked-up module before anything is
written, so a copying defect fails here rather than in lean-eval CI.
Python tests: 91, up from 58.
comparator/pilots/fc_sum_of_three_cubes/ was eleven hand-written files: a copy of generator output, checked in. A copy drifts from the generator, and it says nothing about the importer because a human wrote it. Its workflow was the only thing that referenced it, and the only end-to-end evidence that the Comparator path works at LeanEval's toolchain. So redirect the workflow rather than delete the evidence. It now imports two declarations from FormalConjectures/Wikipedia/SumOfThreeCubes.lean, generates their workspaces, builds them at LeanEval's Lean 4.33 and Mathlib, and takes three Comparator verdicts: the workspace as generated must be rejected, because its Submission is sorry; the same workspace with the statement proved must be accepted; and the answer(sorry) workspace with its hole filled by the proposition on the other side of the iff and the bridge closed by Iff.rfl is accepted, which is the demonstration that a definition hole needs a human reading the answer. That is importer -> generator -> Comparator, end to end, with nothing vendored. For the workspace to build where it is going, it has to be pinned there. comparator/tools.toml gains a [target] table holding LeanEval's toolchain, Mathlib, Comparator and lean4export pins, preserved from the deleted pilot's provenance record. The generator writes lean-toolchain and the lakefile Mathlib revision from it, and every manifest now records both pin sets: source.lean_toolchain, where the answer-slot types were read, and target.lean_toolchain, where they will be used. That gap was open question 4 in OWNERSHIP.md as an assertion; the new job observes it. The Solution adapter marks its delegated hole @[reducible], matching the one workspace known to have built at 4.33. comparator/README.md drops what OWNERSHIP.md already says about ownership and the seam, and three claims that the target pins made false: that generated workspaces carry this repository's toolchain, that they pin Mathlib from lake-manifest.json, and that target pins are not yet recorded. Prose is 268 lines against 313. Python tests: 94.
williamjblair
force-pushed
the
comparator-workspaces
branch
from
August 20, 2026 00:31
a7affe9 to
fc450fa
Compare
`answer_spans` carried its comment-and-string scanner twice; whenever the scan is at code the lexical state is empty, so one `_next_code` helper serves both loops. `closure_region` read and parsed every dependency twice; one pass computes the tuple both consumers share. The seam is one `_seam` helper: the emit path assembles its file map from it, and the generate path stages the context files directly through the same `_write_files` loop `write_tree` uses, instead of filtering the emit map back apart by path prefix. `find_declaration` rglobbed and read every source file per lookup; a cached one-pass index of declared name tokens answers the same question with the same matching rule. The Mathlib revision and the FC merge-base are read once per run; the per-path dirty check stays per call. Shared-library notations with ASCII-only tokens (J(, L(, e) are now copy candidates; the existing gates do the filtering the removed non-ASCII heuristic approximated.
`pins()` refuses to generate from a source file that differs from the merge-base with upstream main, so a pull request editing SumOfThreeCubes.lean could never pass the job its own edit triggered. The trigger now covers comparator/** and the workflow itself; the whole-set audit covers statement drift once an edit lands. The four paths comparator/** already covered are gone. tools.toml now names the comparator repository beside its revision, the workflow clones what the TOML says instead of a hardcoded URL, and the build asserts the bundled lean4export is the revision [target] declares rather than printing it into an output nothing read.
Four fixes the review's finders confirmed against the tree: - `omit` and `include` are file-scoped context; the keyword list did not know them, so a statement written under `omit [...]` was copied with the omitted instances silently restored — an elaborating module stating a different theorem, which no gate could see. Corpus witnesses in ErdosProblems/80, Wikipedia/Kaplansky and two Arxiv files. - `answerTypes` was read off the conclusion after the telescope, so a slot inside a hypothesis binder was invisible and mistyped Prop; the binder types come from the same telescope and now contribute (witness: erdos_975.variants.quadratic, whose slot is ℝ). - An ascribed slot retired its environment entry only when the source spelling string-equalled ppExpr output, so `Set <| Triangle ℝ ℝ²` produced the refusal "-1 Prop slot(s) ... cannot be matched" (witness: erdos_633, which now imports). A statement whose every slot is ascribed is fully typed; leftover entries are respellings. - The proof cut and the block-comment depth count were textual in ways Lean is not: the cut now happens at the first bracket-depth-zero `:= by` (an autoParam default or a structure literal is statement text), and `/-` inside a string, after `--`, or as part of `/--` no longer moves the comment depth. Also: strip_fc_attributes removes the one blank line an emptied attribute leaves, not every blank line in the block.
`comparator_facts` gains a `--batch` arm: `module declaration` pairs on stdin, one environment importing every module in the batch, one JSON object per line in input order. `resolveIn` already filters candidates by module, so the shared environment answers each pair exactly as a per-module import does; the heartbeat budget scales with the batch so each pair keeps its single-run allowance. `import_set` prefetches the whole set through it into a cache that `elaborator_facts` consults first. A pair the batch reports an error for is not cached: the per-declaration run remains the arbiter of what fails and with what message. A hundred-declaration audit run drops from a hundred Mathlib imports to one.
Dropping the non-ASCII rule wholesale let a bare ")" literal qualify a command against every text. Delimiter-only literals are out; tokens with letters or non-ASCII stay, which is what admits J(, L( and e from the shared library.
The adapter's other three JSON boundaries refuse keys nothing reads; the extractor payload was the one consumed as a raw dict. FactsRecord validates the payload's keys, binder and dependency shapes at the seam, so a drift between comparator_facts and this side fails there instead of surfacing as a missing default downstream. `_resolve` is the one statement of problem-file-to-declaration resolution, shared by statement_pair and locate_target. OWNERSHIP and the README now describe the batch arm and the prefetch.
`compile_fc100_target.py` read the known-failures ledger by importing the other command, which dragged the whole importer graph into the target gate. The format's loader now lives in `known_failures.py`, imported by both. The test file covered two modules; `test_fc_source.py` now holds the source-reading cases, the wire-format cases join `test_leaneval_interface.py`, and `test_fc_leaneval_importer.py` keeps the assembly cases. No test changed, only its file.
… what The source pin checked only the statement's own file, while the closure copier read dependency and notation files straight from the working tree: a workspace could mix a pinned statement with branch-local copied text and record one commit for all of it. `pins` now takes every path whose text reached the workspace — statement, dependencies, notation commands, and the pin files the record quotes — refusing a change or an untracked file in any of them. The sidecar's provenance closes the same chain: each copied dependency is recorded as the slice actually emitted (declaration, module, path, range, digest), the statement travels as range plus digest instead of its full text — a trusted-statement record has no business carrying the source's proof body — and a `producer` section names the importer commit, the pinned generator with its contract version, and the target pins the artifact was generated for.
The emitted artifact claimed to be "the exact bytes crossing the seam" while generation piped a different serialisation with an absolute machine-local context root swapped in. The request is now serialised once — relative `context` root, resolved by running the binary with the staging directory as its working directory — and that one string is what the binary reads, what `--emit-import` writes, and what the sidecar digests as `digests.request`. The seam test feeds the emitted file back byte-for-byte instead of reparsing it.
`parse_response` now refuses what it previously let through: unknown fields at either level, a missing field (a refusal, not a KeyError), paths that are absolute, traverse upward, or carry dot/empty/backslash components — which also makes each path its own normal form, so two spellings of one file cannot dodge the duplicate check — a response naming this side's `fc-provenance.json`, and, given the requested ids, any workspace missing or extra. `_write_files` re-checks containment at the write. A `--set` batch validates everything, sidecars and target collisions included, before the first workspace lands, so a refused batch writes nothing rather than a prefix of itself.
Destination group, lifecycle status, visibility, statement revision and submitter are LeanEval's decisions, but they lived as constants inside the wire-format module. They now arrive as an explicit `ImportPolicy` the command constructs — the draft-intake instantiation in one place, a real LeanEval intake free to build its own. The Mathlib repository URL moves to `tools.toml [target]` with the pins it belongs beside. The sidecar's `permitted_axioms` was an assertion nothing checked: the generator owns the Comparator config. Generation now compares the config actually produced against the recorded tuple, so the two cannot drift silently. `slug` and `DefinitionHole` move to `fc_source`, the domain module, so the dependency runs wire-on-source rather than the reverse and fc_source's own "knows nothing of requests" claim is true.
…hey wait The batch protocol's space-delimited lines could not carry every legal Lean name — a guillemet component may contain anything — so both sides now speak JSON lines. The Python side refuses an answer for a pair nothing asked about instead of caching whatever echoes back, and both extractor invocations carry timeouts, so a hang ends the run instead of the day. The ledger loader refuses unknown keys and duplicate declarations: a typo'd field rode along invisibly, and last-one-wins would shadow an entry and quietly defeat the exact match the gates promise.
`[tools]` (comparator, landrun, lean4export) and `[target]`'s repository and commit had no consumer anywhere in the adapter or CI — the CI landrun is the cloned comparator repo's own stub, and the lean-eval commit predates the standalone-generator consolidation. The resolved component pins are now stated to be authoritative, the lean4export local-build note moves to the README beside the local-run instructions, and the file's header commits to the rule: every key has a consumer, or it goes.
… result The whole-set audit's pull-request trigger watched only its own file and the ledger, so an adapter, pin, template, action or toolchain change could bypass the gate it exists to be. It now triggers on everything its outcome depends on, with ordinary statement edits still excluded — the weekly run is their backstop. The artifact grows from two reports into the review evidence: the exact request bytes the set run piped to the generator, every workspace with its provenance sidecar, and a manifest digesting each file. The Comparator job's third-verdict fixture edits gain the same fired-or-fail asserts the second verdict already had.
README: the snapshot check covers every read file, not just the selected source; "exact bytes" is now literal and says why; the 92/8 paragraph caught up with the frozen-set policy google-deepmind#5075 settled. OWNERSHIP records the two boundaries this series drew — catalog policy arrives as an explicit ImportPolicy, and the import header is faithful for this corpus because every problem file already elaborates under all of Mathlib via FormalConjecturesUtil's public import, with the Mathlib revision as the one recorded source-versus-target gap. The same fact sits on MODULE_PREAMBLE itself, where the next reader will look first.
Collaborator
Author
|
Since the ledger retirement, two passes landed on this branch: a code-review pass (commits What the series changes:
The refuted claim was that Evidence of no behaviour change: the FC100 sweep after the series is byte-identical to the one before it in every workspace file; the only diffs are the new sidecar schema and the newly emitted Two follow-ups are filed rather than folded in: leanprover/lean-eval-generator#4 (in-process SHA-256, response path validation, |
Collaborator
Author
|
I think this LeanEval integration is now in a good place with all upstream changes now merged (and no blockers I can see) so I will set to ready for review. Thanks @kim-em for all the support! @mo271 @Paul-Lez it would be great for you both to review when you have time. Paul, specifically, I know you also have a comparator integration so perhaps we can compare both and converge on the best design/engineering direction. In the process of working on this PR, I did a deeper dive into the surrounding architecture and ecosystem around FC and potential directions/future work (perhaps for the upcoming workshop too + related to recent discussions in Zulip) in #5158 |
williamjblair
marked this pull request as ready for review
August 25, 2026 17:10
Adding every read file to the snapshot check swept in `lean-toolchain` and `lake-manifest.json`, which made a toolchain bump the one change that could not pass it: a bump edits exactly those two files, so `pins()` would refuse every declaration and the comparator jobs would fail on the pull request that most needs them to run. They were never source text. The record states them as the environment the facts were read in, which is an observation, not a claim that they came from the pinned commit. The statement, its copied dependencies and its copied notation stay held to one revision.
The generation smoke test and the seam round-trip ran inside the corpus build, on every pull request. A statement pull request paid for building the pinned generator and importing eight declarations it had nothing to do with, a failure in either reported as the corpus build failing at minute eighty, and a pull request editing one of those eight source files could not pass: `pins()` refuses a source file that differs from the merge base, which is exactly what such a pull request changes. The Comparator job already had the right triggers, the extractor and the generator, and the comment explaining why it excludes statement files. Both checks move there, and its module list grows to cover the smoke set. The corpus build goes back to building the corpus.
Three provenance and timeout defects, each the same shape: the failure path produced the answer a reader wants rather than the one that is true. `blob_sha` took an unchecked `git rev-parse` and stored `""` beside a real commit, so a record that had lost its anchor looked like a record that had one. `importer_dirty` took an unchecked `git status`, whose empty output means both "clean tree" and "command failed", and reported clean for both. Both now refuse. The generator is the only call crossing into an external binary and the only one with no timeout, while the extractor's two are bounded and say why; it gets the same bound. A collapsed batch prefetch stays a fallback, not a failure, but it now says so on stderr: re-running a hundred declarations one at a time was otherwise visible only as a job that took hours. Two documentation claims were false. The README credited a job that no longer runs those steps and miscounted the declarations. OWNERSHIP said a test asserts the CLI plumbing never imports the importer; no such test existed, so this adds it rather than softening the claim.
The known-failures gate was written twice, once per stage, differing in the key field and one word; it now lives beside the loader it reads, so the two stages cannot drift about what the ledger means. "Which trees are ours" was spelled three incompatible ways — the copy-dependency allowlist excluded `FormalConjecturesUtil` while Lean's `isFCLocal` included it — and is now one tuple, with the notation scan's ordering kept explicit because it decides output. Every subprocess is bounded. The generator was the last unbounded crossing into an external binary, and the git and lake calls had no bound at all. The limits live in their own module: four callers need them and none of them needs another, which the new seam test noticed when a timeout import created exactly that edge. Three defaults pointed the wrong way and now refuse: a missing `endColumn` silently sliced to the end of the line, a producer record missing whole sections loaded as empty strings, and the ledger gate's own guard defaulted to green. A `--set` run with no ledger says that it gated nothing. A target build that fails without an `error:` line keeps its output instead of recording the words "build failed". In Lean, the heartbeat budget is named once and the batch scales it. A constant whose module the environment cannot name now answers "copy it" rather than "Mathlib has it", and one the environment cannot find at all is kept rather than dropped: both then reach the generated-dependency check, which asks about them, instead of leaving ChallengeDeps quietly short.
Twenty lines of YAML spelled workspace ids the code derives, so three rules — the slug character class, the qualified-name join, and the default id — were encoded in a second place that could not be checked against the first. The command already prints the directory it wrote, so the jobs capture it. A change to how an id is built now fails in the code that owns it. The same for the sidecar: the seam step globs the file the command named rather than composing the name again, and it passes the expected id through, so the response-identity check runs where it matters most. Three smaller duplications go with them. The elan release was installed by two jobs from two copies of the same four lines and is now one composite action, which is what the extractor action already existed to be. The audit's bundle manifest hand-rolled JSON and hashing that differed from the adapter's in encoding, so its digests could not be compared with the ones inside the artifacts it lists; it uses the adapter's now. The Comparator workflow was the only file here without a licence header.
Three modules each held their own copy of the root, so patching one patched a third of the adapter, and the tests only worked because they also mocked whatever the other two would have reached. Every module now reads `fc_source.ROOT`, and the directories derived from it are derived on each read rather than snapshotted at import. The caches were the reason that mattered. `_declared_names`, `fc_notation_commands` and `_base_pins` each cached a value computed from the root while keyed on nothing, and the notation cache stored root-relative paths that reach `pins`. They take the root as an argument now, so a moved root cannot collide with an entry from the old one, and the `cache_clear` calls the tests needed — one of them present, two missing — are gone with the reason for them. The two leaky helpers go too: a `setUp` that assigned before it could register cleanup, and a root assigned outside the `try` that undid it.
The whole-set audit was one job doing two things that fail for different reasons and cost differently. Importing, verifying and generating the set is one Mathlib, this repository's, and it is where an FC-side defect shows: that half stays on every pull request touching the adapter. Compiling the result at LeanEval's pins is a second Mathlib at a second toolchain, most of the runtime, and what it catches is the other repository bumping rather than anything a pull request here did: that half runs weekly and on demand, against the set the first half generated rather than regenerating it. `merge_group` stays off deliberately. It does not support path filters, so adding it would put a two-Mathlib job on every merge in a repository with three hundred open pull requests.
Collaborator
|
Hey @williamjblair thanks for working on this! @williamjblair Re the comparator integration I've been working on, this is intended to be somewhat minimal (i.e. generate the bare minimum needed to run comparator on a given declaration, e.g. this would be useful as a check for people who want to submit solutions to problems that are too large to fit in the repo). Since Lean-Eval may have different constraints, so it's not clear that my implementation would be the right fit there. |
Collaborator
Author
|
I agree on your complexity/brittleness points (the closure copying and the notation copying are the brittle part which exist only because a workspace cannot depend on this repository) There are two main design decisions to fix this however 1. Let the workspace depend on this repository. This removes the copying:
These would be calls for @kim-em. 2. Make this repository export its facts. Nothing here emits ranges, notation or namespaces, so the adapter rebuilds them from source text. #5158 proposes the Neither decision changes the rest: the proof still becomes Sounds good on the comparator work too! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Tracking: #4394 · Integration: #4930 · Architecture RFC: #5158
Upstream plan: lean-eval#536 workstream 9 · coordination lean-eval#533
This PR adds the FC-side importer from §10 of the LeanEval plan. It turns one FC declaration into one evaluation workspace, through a versioned contract with a pinned external generator.
1. The system
flowchart TB subgraph FC["Formal Conjectures — this PR"] A["Declaration<br/>erdos_730, @[category ...]"] B["Elaborated facts<br/>ranges · binders · slot types"] C["Marked-up module<br/>statement + copied closure"] A --> B --> C end C --> R["Request JSON<br/>schema version 1"] R --> G subgraph G["lean-eval-generator — pinned 77373a53"] GG["Render workspace"] end GG --> WS["Workspace file map<br/>+ FC provenance sidecar"] WS --> LE subgraph LE["LeanEval"] LL["Catalog · target pins · scoring"] end LL --> SOL["Solver writes Submission.lean"] SOL --> CMP subgraph CMP["Comparator"] CC["Sandbox · export · identity<br/>+ axiom check · kernel replay"] end CC --> V(["Verdict"])Each stage owns one thing, and the artifact between stages is checkable.
This PR is the first box. It does not generate workspaces, score submissions, or judge proofs. The placeholder generator it once carried is deleted, not forked.
2. Why the module is Mathlib-only
LeanEval vendors its problems. A Challenge cannot fetch this repository when a solver builds it. So the statement cannot import its own FC module, and every FC declaration it depends on must travel with it.
The importer therefore copies the declaration's FC-local closure into the module, each copied declaration carrying the
open,variable,universe,set_optionandlocal notationin force where it was written. Copying is a construction, so it can be wrong in ways only Lean sees.--verifyelaborates the assembled module before anything is written.3. The generated workspace
flowchart LR CD["ChallengeDeps.lean<br/>copied FC closure"] --> CH["Challenge.lean<br/>trusted statement + hole"] CH --> SO["Solution.lean<br/>fixed adapter"] SU["Submission.lean<br/>the solver works here"] --> SO SO --> WT["WorkspaceTest.lean"] CF["config.json<br/>targets + permitted axioms"] --> WT WT --> CMP(["Comparator"])Solution.leanis fixed. It fails to build if a submission changes the statement.config.jsonnames the permitted axioms, so a submission that leavessorryreportssorryAxand is rejected. The FC provenance sidecar rides beside these files and records where the statement came from.4. Two toolchains, on purpose
The importer reads facts from an environment elaborated at this repository's Lean 4.33.1. The workspace builds at LeanEval's Lean 4.33.0. The gap is one Mathlib patch release, and CI builds across it, so the gap is observed rather than assumed.
An FC-side copying defect fails at
--verify, on this side. A genuine target incompatibility fails at the target build. The two gates tell those apart.The
import Mathlibheader is faithful, not convenient: every problem file importsFormalConjecturesUtil, whichpublic imports all of Mathlib. Each statement already elaborates under the full library. The header drops only the FC-local layer, which travels as the copied closure.5. Result at this head
100/100 declarations import, verify, classify (92 open + 8 solved), generate, and compile at target pins.
comparator/known_failures.tomlis empty, and the audit asserts exactly that.6. Guarantees at the boundary
Each row is a check, not a convention.
pins()holds every source file read to one revision: the statement, its copied dependencies, its copied notation. An untracked file refuses. The toolchain and manifest are recorded as the environment observed, not held to the pin, so a toolchain bump can still run these jobs--emit-import, and recorded asdigests.request. The seam test replays it byte for byte--setbatch validates fully before the first writeconfig.jsonis compared against the manifest at generationImportPolicy7. CI
comparator/**The adapter's checks live with the adapter, not beside the corpus build. A pull request that only edits a statement should not pay for them, and could not pass them:
pins()refuses a source file that differs from the merge base, which is exactly what such a pull request changes.The three verdicts exist because a gate that only ever accepts proves nothing:
sorry, which addssorryAx, which the config does not permit.answer(sorry)hole filled with the proposition from the other side of the iff, closed byIff.rfl, is accepted and resolves nothing. A definition hole is where a machine check cannot stand in for a human reading the answer. The generated README says so; this asserts it.The audit is split because its halves cost differently. The source half is one Mathlib, this repository's, and it is where an FC-side defect shows, so it gates every pull request that touches the adapter. The target half is a second Mathlib at LeanEval's toolchain, and it catches drift in the other repository rather than a defect here, so it runs weekly against the set the source half generated.
The bundle is the evidence, not a summary: the exact request bytes, every workspace with its sidecar, the report, and a manifest digesting each file.
make_comparator_workspace.py --setis the same run locally.8. Audit response
All findings from the whole-set audit are closed.
conjecturedeclarations shared one idnoncomputable sectioncarried with the preamble; FC notation copied only where it was in force; namespaces created before any copiedopen; statement-rootedmatchauxiliaries accepted; ascribed slots read at their own positionirrational_e_to_efailed at target pinslocal notation "e" => exp 1was masked at FC pins by auto-bound implicits. The preamble fix closed itErdos1092failed at target pinsDotted names surfaced during migration. The generator anchors on a declaration's last component, so
erdos_1038.parts.iwould generatetheorem i. Dotted names are restated under their slug, and the provenance records the FC name.9. Files to review
fc_source.pyfc_leaneval_importer.pycomparator_facts.leanleaneval_interface.pyleaneval_generator_cli.pyknown_failures.pytemplates/WorkspaceTest.lean10. Open questions
sourceis one free-text line. The FC commit, blob and declaration id that §10 requires have no home, so they travel as a sidecar. Should a future contract carry a passthrough provenance object? Theformalization.yamloverlap belongs here: the question is which object owns which fields.definition_namesis checkable only against the comparator commit pinned intools.toml.lean-eval-generator#4 proposes three upstream hardening items. None changes contract v1. Nothing here waits on them.
11. Not in scope
Disproof support (Wave 4). Opening problem PRs to lean-eval, which waits on the launch gates and on consolidation with @Paul-Lez's prototype. Editing
FC100OpenSet1.lean, resolved by #5075.The source-reconstruction half of the adapter is a compatibility boundary, not a design. It recovers facts the elaborated environment already knows, because this repository has no export boundary yet. #5158 proposes the manifest that would let it be deleted. Nothing in that RFC blocks this PR.