Undeclared Library Prior Symbol Classifier

Detects when a checked Lean proof cites a library result outside its approved set.

Contract

Does It checks whether a Lean proof cites a library result (a lemma or definition) that was never on its approved list. Even after a prover accepts a proof, that proof can still quietly use a library symbol it wasn't allowed to, and this component surfaces those out-of-bounds uses as an inspectable record that names each symbol and where the rule came from. It matters because "the proof checked" does not mean "the proof stayed within the allowed set of building blocks," and this makes that gap visible without ever reading the proof's own steps.

Scope limit It only projects the symbol-boundary classification mechanic over copied Lean/Std premise rows and pre-extracted symbol observations; it does not read proof source, run Lean or Lake, prove formal-result correctness, treat the whole standard library as an implicit allowlist, claim Mathlib availability, use external model services, or include launch operations.

Run

Command

PYTHONPATH=src python3 -m microcosm_core.organs.undeclared_library_prior_symbol_classifier run --input fixtures/first_wave/undeclared_library_prior_symbol_classifier/input --out receipts/first_wave/undeclared_library_prior_symbol_classifier

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Corpus Readiness Mathlib Absence Gate, Tactic Portfolio Availability Probe, Provider Context Recipe Budget Policy

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module

Paper module Undeclared Library Prior Classifier

Undeclared Library Prior Classifier scores extracted Lean symbol observations against an allowed premise set without running Lean or treating libraries as implicit allowlists.

Read the full write-up

Back to Components index → Reference roster →