Component · spec & evidence

Tactic Portfolio Availability Probe

Maps which Lean proof tactics a recorded run marked usable before any code relies on one.

Contract

Does It turns one captured Lean run's results into an inspectable list of which proof shortcuts ("tactics" like `rfl`, `simp`, `omega`, `aesop`) were recorded as compiling, showing at a glance which are usable and which are off before anything treats a tactic as available. In this fixture seven tactics are marked usable and `aesop` is marked failed (its recorded run hit a missing-Mathlib error). The tool reads pre-recorded status rows and checks them for honesty; it does not run Lean itself.

Scope limit It only projects and validates which tactics were recorded as compiling in one captured environment; it does not run Lean/Lake at all, prove any goal, certify domain-level conclusions, use external model services, claim benchmark performance, or include launch operations.

Run

PYTHONPATH=src python3 -m microcosm_core.organs.tactic_portfolio_availability_probe run --input fixtures/first_wave/tactic_portfolio_availability_probe/input --out /tmp/plectis-public-runs/tactic_portfolio_availability_probe

PYTHONPATH=src python3 -m microcosm_core.organs.tactic_portfolio_availability_probe run --input fixtures/first_wave/tactic_portfolio_availability_probe/input --out receipts/first_wave/tactic_portfolio_availability_probe --acceptance-out receipts/acceptance/first_wave/tactic_portfolio_availability_probe_fixture_acceptance.json

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Corpus Readiness Mathlib Absence Gate, Formal Math Verifier Trace Repair Loop, Target Shape Tactic Routing Gate, Undeclared Library Prior Symbol Classifier, Verifier Lab Kernel

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module