Corpus Readiness Mathlib Absence Gate

From recorded lean

From a recorded Lean readiness report it answers, per corpus, whether the library is present and whether the Mathlib import lane resolves, pairing copied rows with a live probe. corpus_readiness_mathlib_absence_gate reads a recorded readiness report from a Lean math toolchain run and turns one question into an inspectable answer: for each math corpus, is it actually present on this host, and is the Mathlib import lane actually available, or not? It carries copied corpus and toolchain rows from a 2026-05-11 proof-state curriculum smoke run and pairs them with a live import check.

Emits metadata-only readiness

It emits a metadata-only readiness board and consumer verdicts: which corpora are absent, which are smoke-test only, and which tasks stay blocked until a Mathlib probe passes. The output is a readiness board and a set of consumer verdicts. It records which corpora are absent, which are usable only for translation smoke tests, and which downstream tasks stay blocked until a passing Mathlib probe exists. Everything it emits is metadata-only: no proof text, no provider output, no non-public paths.

Is not prover

It is not a prover or Lake build but a gate that forces a formal-math route to expose corpus readiness before any proof route counts as usable. It is not a theorem prover, a Lake build, or a Mathlib availability claim. It is a gate that forces a formal-math route to expose corpus readiness before any proof route is treated as usable.

Purpose

Roster presence mistaken for usability

Formal-math agents conflate a corpus appearing on a roster with it being usable for their proof route, so a missing library surfaces only later as a broken import. Formal-math agents fail in one specific way. They treat "there is a corpus" as if it meant "this corpus is usable for the proof route I am about to take". A roster lists miniF2F, PutnamBench, ProofNet, LeanDojo and Mathlib, the agent assumes the libraries are present, and the failure only surfaces later as a broken import or a tactic that needs a premise the host cannot resolve.

Alias field must agree with a live probe

The loose check trusts a mathlib_available field or PASS status; this gate refuses that drift, flagging any row whose alias claim a live probe does not confirm. The loose version of this check trusts the roster. It reads a mathlib_available field, or a PASS lean status, and marks the corpus ready. That is the drift the gate is built to stop. A stale alias field cannot turn the gate green on its own. It has to agree with a live probe or the row is flagged.

How it works

Two entrypoints funnel into _build_result

run and run_projection_bundle both call _build_result, which loads two inputs, scans paths against the exclusion policy, then folds four ordered checks into one result and board. The two entrypoints run and run_projection_bundle both call _build_result. run handles the first-wave fixture with its negative cases. run_projection_bundle handles an exported bundle without negative cases and requires a source-module manifest. _build_result loads the two input files, scans every input path against the non-public-state exclusion policy, then runs four checks in order and folds them into one result and a readiness board.

flowchart TD input["Fixture or exported bundle input corpus rows plus consumer gate cases"] artifacts["validate_runtime_source_artifacts four source digests, parse JSON, run probe"] probe["runtime_lean_import_probe Std compiles, Mathlib import rejected"] corpus["validate_corpus_readiness seven corpus rows checked against the probe"] gates["validate_consumer_gate_cases verdicts derived from readiness facts"] imports["validate_source_module_imports copied source digests for the bundle"] result["_build_result one metadata-only result and board"] input --> artifacts artifacts --> probe probe --> corpus corpus --> gates input --> imports gates --> result imports --> result

The live import probe: Std compiles, Mathlib rejected

validate_runtime_source_artifacts digest-checks four source refs and runs a probe that expects Std to compile and Mathlib to be rejected, setting mathlib_lake_project_import_available false when the lane fails. validate_runtime_source_artifacts anchors the run to four source refs: the corpus readiness rows, a tactic-affordance probe, the Mathlib import probe Lean file, and a tactic portfolio availability file. It checks each file's SHA-256 against a recorded digest, parses the JSON ones, and calls runtime_lean_import_probe. That probe writes two small Lean files into a temporary directory. One imports Std and is expected to compile. One imports Mathlib and is expected to be rejected with the toolchain's own unknown module prefix 'Mathlib' error. The probe also confirms lake is on the path. It never runs lake build and never exports any Lean body. Its result sets mathlib_lake_project_import_available, which stays false whenever the Mathlib lane does not resolve.

Corpus rows normalised against probe evidence

validate_corpus_readiness marks a corpus usable only when it exists, carries a Lake file, and the probe agrees; contradicting alias claims are flagged and every unavailable lane is blocked. validate_corpus_readiness normalises the seven corpus rows against that runtime evidence. A corpus is marked usable for Mathlib-dependent work only when the runtime row says it exists, carries a Lake file, and the Mathlib import lane is available. If a row claims mathlib_lake_project_import_available or any present alias in MATHLIB_PRESENT_ALIAS_FIELDS while the probe disagrees, the row is flagged with CORPUS_READINESS_RUNTIME_PROBE_CONTRADICTION. Absent corpora and every unavailable Mathlib lane land in blocked_capabilities. In the current fixture the probe stays false, so all seven Mathlib lanes are blocked.

Consumer verdicts derived from readiness facts

validate_consumer_gate_cases recomputes each verdict from readiness facts, not the case's own label, blocking cases needing an unavailable Mathlib lane or an absent corpus; only the miniF2F smoke passes. validate_consumer_gate_cases derives each verdict from the readiness facts instead of trusting a case's own expected-decision label. A case is blocked if it requires the Mathlib lake project import while that lane is unavailable, or if its target corpus is absent. Of the seven cases, one passes: the miniF2F Lean3 translation smoke, which does not require a Mathlib project. The other six stay blocked. A case that never set readiness_gate_checked is flagged with CONSUMER_READINESS_GATE_UNCHECKED.

Exported-bundle source floor and final status

validate_source_module_imports enforces copied-body digests and byte equality, and _build_result passes only when no negative case is missing, the secret scan is clean, and the source floor holds. validate_source_module_imports adds the exported-bundle floor. It requires the manifest to declare copied_non_secret_macro_body, each row to use a body material class, each copied file to match its recorded source and target digest, and no row to carry a body inside a result record. Exact-copy rows must preserve byte equality; rewrite rows must match the declared private-absolute-path rewrite recipe exactly. _build_result then computes one status: it passes only when no expected negative case is missing, the secret scan has no blocking hit, the source-module floor holds, and no unexpected finding appears.

Negative cases

Fixture carries five

The fixture carries five named negative inputs, declared in EXPECTED_NEGATIVE_CASES. Each one must be observed with its error code or the run is blocked:

• mathlib_available_without_probe must raise MATHLIB_AVAILABILITY_OVERCLAIM when Mathlib is claimed available with no passing probe.
• consumer_skips_readiness_gate must raise CONSUMER_SKIPS_CORPUS_READINESS_GATE when a consumer attempts Mathlib-dependent work without checking readiness.
• private_corpus_source_ref must raise PRIVATE_CORPUS_SOURCE_REF_FORBIDDEN when a source ref points at a non-public paths.
• proof_body_leakage must raise CORPUS_READINESS_PROOF_BODY_FORBIDDEN when a corpus row carries a proof or provider body field.
• release_overclaim must raise CORPUS_READINESS_RELEASE_OVERCLAIM when the metadata tries to include launch operations or proof authority.

Prior Art Grounding

Grounded in Lean corpus and theorem-proving work

The design draws on Lean corpus and neural theorem-proving work where library availability and benchmark splits are part of the claim, requiring probes and digests before tactic-routing language is allowed. This component sits in Lean corpus and neural theorem-proving work where library availability, premise access, and benchmark splits are part of the claim. The Lean mathematical library establishes Mathlib as a large community-maintained formal mathematics corpus, miniF2F gives a cross-system benchmark for formal Olympiad statements, and LeanDojo shows why reproducible corpus extraction and accessible-premise metadata matter for theorem-proving agents. The gate borrows the discipline: corpus rows, Mathlib probes, blocked consumer cases, and copied-source digests must be visible before retrieval or tactic-routing language is allowed. It does not claim Mathlib is present or that any theorem was proved.

Validation Result record Path

Reader-verifiable commands, run from the microcosm-substrate/ public root:

PYTHONPATH=src python3 -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run \
  --input fixtures/first_wave/corpus_readiness_mathlib_absence_gate/input \
  --out /tmp/microcosm-corpus-readiness-mathlib-absence-vrp
PYTHONPATH=src python3 -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run-projection-bundle \
  --input examples/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle \
  --out /tmp/microcosm-corpus-readiness-mathlib-absence-bundle-vrp
PYTHONPATH=src python3 scripts/build_doctrine_projection.py --check-paper-module-corpus
PYTHONPATH=src .venv/bin/python -m pytest -p no:cacheprovider --basetemp=/tmp/microcosm-corpus-readiness-mathlib-absence-tests -q tests/test_corpus_readiness_mathlib_absence_gate.py

What a pass certifies and excludes

A pass means fixture and exported bundle agree on readiness, Mathlib absence, blocked consumers, digests, and the five negative cases; it reruns no Lean, proves nothing, and installs no Mathlib. A pass means the fixture and the exported bundle agree about corpus readiness, Mathlib absence, blocked consumers, copied source digests, metadata-only result files, and the five negative cases. It does not rerun Lean or Lake, prove any theorem, or install Mathlib.