Corpus Readiness Mathlib Absence Gate
Runs the real Lean toolchain to confirm the math library is absent, then gates proof tasks.
Contract
Does It reads a recorded readiness report from a Lean math toolchain run and makes one fact inspectable: when the report was captured, the Mathlib library was not importable (its import probe failed). From that, it lists which math corpora are absent or usable only for translation smoke tests, and which downstream tasks must be blocked before any Mathlib-dependent proof work is attempted. It also re-checks that the recorded source files match their recorded SHA-256 digests and that no proof bodies, provider outputs, or non-public paths leaked into the public output. The result shows exactly where the proof pipeline draws a hard "not ready, do not proceed" line, with provenance, instead of quietly assuming the environment is fine.
Scope limit It only projects and gate-checks recorded corpus/toolchain readiness accounting, re-verifies recorded source digests and leakage guards, and runs a bounded Lean/Lake import probe when a toolchain is present. It does not run a full Lake build, prove formal-result correctness, claim Mathlib is available beyond the probe result, benchmark corpora, score model performance, use external model services, or include launch operations or public sharing.
Run
PYTHONPATH=src python3 -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run --input fixtures/first_wave/corpus_readiness_mathlib_absence_gate/input --out receipts/first_wave/corpus_readiness_mathlib_absence_gateEvidence
ClassExternal tool runevidence 4/5Real runtime resultRuns real tools
Links to Verifier Lab Kernel, Tactic Portfolio Availability Probe, Undeclared Library Prior Symbol Classifier, Formal Math Lean Proof Witness
Source
Paper module
Paper module Corpus Readiness Mathlib Absence Gate