Formal Math Premise Retrieval

Public premise retrieval after source import

This is the first source-available formal-math import slice after the source projection protocol, turning the source prover lab's premise-index, term-scoring, context-budget, and strategy-selection patterns into a runnable component. formal_math_premise_retrieval is the source-available first real formal-math import slice after the source projection protocol. It turns the source prover lab's premise-index, term-scoring, context-budget, and strategy-selection patterns into a runnable Microcosm component.

It is still deliberately below proof authority. It validates:

• Lean/Std premise metadata;
• query term scoring across public premise ids, namespaces, declaration names, statement excerpts, and retrieval terms;
• split eligibility;
• context recipe budgets;
• public strategy ids;
• redacted result records;
• negative cases.

It stays deliberately below proof authority, refusing Lean or Lake execution, external model access, proof-body or oracle-id exposure, test-split tuning, correctness claims, and launch. It does not run Lean or Lake, use external model services, expose proof bodies, expose oracle-needed premise ids, tune on test split truth, claim formal-result correctness, or include launch operations.

Purpose

Premise selection narrows the library

Before a model can attempt a proof it must find the right lemmas, and this component is the smallest honest premise-selection step: score every public premise against a query and return a ranked shortlist. Before a model can attempt a formal proof, it has to find the right lemmas. A Lean library holds thousands of theorems and definitions, and the useful ones for a given goal are a handful. Premise selection is the step that narrows that library down to candidates worth putting in front of a prover. This component is the smallest honest version of that step: it takes a query, scores every public premise against it, and returns a ranked shortlist.

Retrieval must work and the boundary must hold

The narrow question is whether transparent term-scoring over copied public Lean/Std metadata returns the premises a query should find without touching a proof, so retrieval must work and the boundary must hold. The single question it answers is narrow and checkable: given a copied catalogue of public Lean/Std premise metadata, does a transparent term-scoring retrieval return the premises a query should find, without ever touching a proof? Both halves matter. The retrieval has to actually work, so each fixture query carries the premise ids it is expected to surface and the run fails if the shortlist misses them. And the boundary has to hold, so the same run refuses any input that smuggles in a proof body, an oracle answer, or test-split truth.

The restraint is the point

The index is plain inspectable term overlap, not a learned embedding or benchmark claims, so the claim is that retrieval runs over real copied Lean metadata and forbids the shortcuts that would flatter it. What is unusual is the restraint. The retrieval index is not a learned embedding model and the scoring is not a benchmark claims. It is plain term overlap over fields that a reader can inspect: premise ids, namespaces, declaration names, statement excerpts, and retrieval terms. The interesting claim is therefore not "this retrieves well" but "this retrieves over real, copied Lean metadata and can be audited end to end, and the design forbids the shortcuts that would make a premise-selection result look better than it is".

Shape

flowchart TD bundle["JSON source record paper_module.formal_math_premise_retrieval"] --> instance["Generated paper-module instance 15 relationship edges"] instance --> component["Runtime component formal_math_premise_retrieval.py"] subgraph Inputs["Public inputs"] index["Premise index copied Lean/Std metadata"] queries["Retrieval queries terms, split, strategy, top_k"] recipes["Context recipes byte budgets"] negatives["Negative-case inputs proof body, oracle ids, test-split tuning, budget, strategy"] end component --> index component --> queries component --> recipes component --> negatives index --> split["Split gate skip premises not in allowed_for_split"] queries --> split split --> score["Term-overlap scoring shared tokens + strategy bonus"] score --> shortlist["Ranked top_k shortlist"] shortlist --> recall["Recall check vs expected premise ids"] negatives --> reject["Required rejections five leakage/overclaim guards"] recipes --> reject recall --> result records["metadata-only result records board, validation, sign-off"] reject --> result records result records --> ceiling["Scope limit metadata coherence, no Lean/Lake, no proof"]

Evidence/accounting:

• Bundle authority: core/paper_module_capsules.json::paper_modules[25:paper_module.formal_math_premise_retrieval] has source_authority: json_capsule, three subjects, one resolved code_loci[0].path, depends_on naming paper_module.formal_math_lean_proof_witness, and generated projection statuses for Markdown, Mermaid, and Atlas.
• Generated instance: paper_modules/formal_math_premise_retrieval.json::paper_module_payload repeats the bundle authority_ceiling, reports Mermaid status available_from_capsule_edges, and derives 15 relationships.edges with relationships.unpopulated_selective_relations: [].
• Component atlas: core/organ_atlas.json::organs[9:formal_math_premise_retrieval] classifies the component in family: formal_math_and_proof, cites the runtime locus, and restates that retrieval metadata coherence is not Lean/Lake, provider, theorem-correctness, benchmark, or launch-scope decision.
• Mechanism rows: core/mechanism_sources.json::mechanisms[27:mechanism.formal_math_premise_retrieval.validates_public_premise_retrieval_slice] and core/mechanism_sources.json::mechanisms[37:mechanism.formal_math_premise_retrieval.validates_public_premise_retrieval_projection] point at src/microcosm_core/organs/formal_math_premise_retrieval.py and name first-wave, sign-off, and runtime-shell result record refs.
• Runtime and tests: src/microcosm_core/organs/formal_math_premise_retrieval.py exposes run, run_retrieval_bundle, EXPECTED_NEGATIVE_CASES, and AUTHORITY_CEILING; tests/test_formal_math_premise_retrieval.py checks 11 premises, 4 queries, 44 considered candidates, five negative cases, metadata-only result records, and compact runtime-shell cards.
• Result records: receipts/first_wave/formal_math_premise_retrieval/formal_math_premise_retrieval_result.json records status: pass, 11 premises, 4 queries, 44 considered candidates, five observed negative cases, missing_negative_cases: [], and a secret-exclusion scan with blocking_hit_count: 0; the exported runtime result record at receipts/runtime_shell/demo_project/organs/formal_math_premise_retrieval/exported_premise_retrieval_bundle_validation_result.json records status: pass, the same premise/query/candidate counts, no negative cases, and secret_exclusion_scan.scanned_path_count: 11.
• Standard ceiling: standards/std_microcosm_formal_math_premise_retrieval.json::authority_ceiling has status: pass while keeping formal_proof_authority, lean_lake_authority, provider_authority, and release_authority false.

Runtime Surfaces

• Component runner: 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
• Exported bundle runner: python -m microcosm_core.organs.formal_math_premise_retrieval run-retrieval-bundle --input examples/formal_math_premise_retrieval/exported_premise_retrieval_bundle --out receipts/runtime_shell/demo_project/organs/formal_math_premise_retrieval
• CLI route: microcosm formal-math-premise-retrieval run-retrieval-bundle
• Standard: standards/std_microcosm_formal_math_premise_retrieval.json
• Fixture manifest: core/fixture_manifests/formal_math_premise_retrieval.fixture_manifest.json

Public Claim

Microcosm can show a real formal-math retrieval mechanism in miniature:

• a source-available Lean/Std premise index;
• public field-haystack term-scored queries;
• split-aware eligibility;
• context recipe ceilings;
• strategy gates;
• redacted validation result records.

How retrieval scoring works

Five inspectable fields per premise

Each premise contributes five inspectable fields, premise id, namespace, declaration name, statement excerpt, and retrieval terms, while a query carries its own terms, split, optional strategy, recipe, and expected ids. Each premise row contributes five inspectable fields to the haystack: its premise id, namespace, declaration name, statement excerpt, and a list of retrieval terms. A query carries its own terms, a data split, an optional strategy id, a context recipe, and the public premise ids it is expected to return.

Term-overlap scoring with a split gate

Scoring is per-query term overlap over the five fields, with a split gate that structurally excludes premises whose allowed_for_split omits the query split and a single-point bonus for a matching strategy tag. Scoring is term overlap, computed per query. Both the query and each premise are tokenised into lowercase word counts. A premise is only considered if the query's split appears in that premise's allowed_for_split list, which is how test-split leakage is kept out at the structural level rather than by trust. For each eligible premise the score is the summed minimum count of every shared token across the five fields, so a term that appears in both the query and the premise contributes as many points as the smaller of the two counts. A premise that also carries the query's strategy id as a tag gets a single extra point. The ranked list is sorted by score descending, ties broken by premise id, and the top of that list up to the query's top_k is taken as the retrieval.

Grading recall against expected ids

The retrieval is graded against itself: each query declares the ids it should surface, recall is the fraction that landed in the shortlist, and any miss blocks the run. The retrieval is then graded against itself. Each query declares the public premise ids it should surface, and the component computes recall as the fraction of those expected ids that actually landed in the shortlist. A query that declares expectations but misses any of them blocks the run. In the first-wave fixture this is eleven premises and four queries, scoring forty-four considered candidates in total, and every query is expected to reach full recall.

Five refusals keep the signal honest

The five negative-case inputs each encode a shortcut, a shipped proof body, oracle ids, test-split tuning, a budget overflow, and an unknown strategy, and all five rejections must be observed or the fixture blocks. The failure mode this guards against is a premise-selection result that looks good because it cheated. The five negative-case inputs each encode one such shortcut: a premise index that ships a proof body, a query that lists the oracle premise ids it is "meant" to find, a query that tunes on test-split truth, a context recipe that blows past the byte budget, and a query naming a strategy id outside the allowed set. The run is required to observe all five rejections; if any expected rejection is missing, the whole fixture is blocked rather than passed. Recall over copied real metadata is the positive signal; the refusals are what keep that signal honest.

Prior Art Grounding

Premise-selection and retrieval-augmented proving

The component is grounded in premise-selection and retrieval-augmented theorem proving, closest to LeanDojo and motivated by earlier environments like HOList and GamePad that extract premise metadata for learning-assisted proving. This component is grounded in premise-selection and retrieval-augmented theorem proving work. LeanDojo is the closest modern anchor because it couples Lean interaction with retrieval-augmented premise selection. Earlier theorem-proving environments such as HOList and GamePad also motivate extracting proof-state or premise metadata for learning-assisted theorem proving.

Borrowing the retrieval accounting pattern

Microcosm borrows the retrieval accounting pattern, requiring premise ids, excerpts, terms, split eligibility, budgets, and strategy gates to be inspectable before any retrieval claim, without running Lean/Lake or exposing proof bodies. Microcosm borrows the retrieval accounting pattern: premise ids, namespaces, statement excerpts, retrieval terms, split eligibility, context budgets, and strategy gates must be inspectable before premise-retrieval claims are admitted. It does not run Lean/Lake or expose proof bodies.

Negative Cases

• premise_index_proof_body_forbidden
• query_oracle_ids_forbidden
• test_split_tuning_attempt
• context_recipe_budget_overflow
• unknown_strategy_id

Reader Evidence Routing

• Start with the JSON Bundle Binding to identify the source record, generated instance, proof boundary, and scope limit.
• Use Structured Lattice Bindings for navigation; the generated JSON row is the authority for relationship counts and dependency state.
• Use Runtime Surfaces and Result record Expectations when checking metadata coherence, redaction, leakage checks, and source-available bundle behavior.
• Use Negative Cases, Scope limit, and Scope limit together before admitting any formal-math public claim.

Validation Result record Path

Reader validation without durable writes

./repo-pytest tests/test_formal_math_premise_retrieval.py -q --basetemp=/tmp/microcosm_formal_math_premise_retrieval_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus