Lean Std Premise Index

Lists a fixed catalog of public Lean building blocks and confirms none hides proof text or test answers.

Contract

Does Presents a small, fixed catalog of Lean standard-library "premises" (named building blocks like facts about numbers, booleans, lists, and basic logic) along with the labels and source references that say where each one comes from. It shows what proof ingredients are on the table and that they were copied from public Lean sources, with no hidden proof text, no Mathlib, and nothing that secretly gives away test answers. It only checks and displays this catalog; it does not run Lean or prove anything.

Scope limit It only validates the projection of premise metadata and copied source bodies; it does not run Lean or Lake, prove any theorem correct, expose proof bodies or oracle-needed ids, use external model services, produce benchmark claims, or include launch operations.

Run

Quick probe

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

Validator command

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

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Formal Math Verifier Trace Repair Loop, Verifier Lab Kernel, Mathematical Strategy Atlas Hypothesis Scorer, Undeclared Library Prior Symbol Classifier

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module

Paper module Lean/Std Premise Index

The Lean/Std premise index validates a copied public Lean/Std descriptor catalog plus Ring2 premise-retrieval source bodies without claiming proof, Mathlib, Lean/Lake, provider, launch, or theorem-correctness authority.

Read the full write-up

Back to Components index → Reference roster →