Formal Math Readiness Gate
Reads declared math setups and lists which proof tactics may be attempted versus blocked.
Contract
Does Before anyone tries to prove a math theorem with the Lean prover, this gate reads simple description files that declare what a math setup is supposed to have — which math library is claimed to be present, which proof tactics are reported as already probed, which lemmas may be looked up, and which limits apply to the text budgets handed to AI providers — and writes a plain checklist of what is allowed to be attempted versus blocked. It works only from those declared description files; it does not inspect the real toolchain or run anything. Its guards keep the claims honest and checkable: it refuses to let a library be marked available unless a probe result backs that up, blocks routing a proof tactic that was not probed, and refuses to let any real proof text sneak into the lemma-lookup tables or provider budgets.
Scope limit It only validates and projects declared readiness metadata; it does not run Lean/Lake, inspect the real toolchain, use external model services, prove any theorem correct, produce benchmark claims, or authorize Mathlib-dependent proof attempts.
Run
microcosm formal-math-readiness-gate run --input fixtures/first_wave/formal_math_readiness_gate/input --out receipts/first_wave/formal_math_readiness_gateEvidence
ClassComputed projectionevidence 3/5Source-faithful refactor
Links to Formal Math Lean Proof Witness, Source Projection Import Protocol, Proof / Control / Runtime Import Bundle, Provider Context Recipe Budget Policy, Tactic Portfolio Availability Probe, Target Shape Tactic Routing Gate
Source
Paper module
Paper module Formal Math Readiness Gate