Component · spec & evidence

Formal Math Premise Retrieval

Shows which lemmas a plain search surfaces per query, and never leaks proof text or answer keys.

Contract

Does Given a small copied set of Lean/Std math-lemma descriptions plus some search queries, this component shows which lemmas a plain term-matching search would surface for each query, how it keeps each assembled context within a fixed size budget, and that it never exposes proof text or "answer-key" hints (the premise ids a solver would only get to see after the fact). On the bundled first-wave fixture, the result record shows the retrieval mechanism working in miniature alongside deliberate bad inputs (a leaked proof body, leaked answer-key ids, a budget overflow, an attempt to peek at test answers, and an unknown strategy) that the component catches; the leak and budget guards actually fire.

Scope limit It only checks that public retrieval metadata is internally coherent, term-scored over a copied index, budget-bounded, and leakage-clean; it does not run Lean/Lake, use external model services, prove any theorem or its own correctness, claim benchmark performance, or include launch operations.

Run

PYTHONPATH=src python -m microcosm_core.organs.formal_math_premise_retrieval run --input fixtures/first_wave/formal_math_premise_retrieval/input --out receipts/first_wave/formal_math_premise_retrieval

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Formal Math Lean Proof Witness, Formal Math Verifier Trace Repair Loop, Lean Std Premise Index, Verifier Lab Kernel, Mathematical Strategy Atlas Hypothesis Scorer, Ring2 Premise Retrieval Precision Recall Harness

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module