Formal Math Lean Proof Witness

Component checks whether

This component checks whether the installed Lean toolchain actually compiles a tiny purpose-built project end to end and whether that run can be recorded without copying the proof into the record. This component answers one narrow question and refuses the larger ones. The question is whether the installed Lean toolchain will actually compile a tiny, purpose-built Lean project end to end, and whether that run can be recorded without copying the proof into the record. It is not a theorem prover, a benchmark, a Mathlib check, or an import of any private proof. It runs lake build over a synthetic fixture and writes down what happened.

Emits metadata-only record

It emits a metadata-only record of tool availability, build return code, output line counts, source hashes, declaration names, and per-file counts, while the proof text and raw tool output never reach it. What it emits is a metadata-only result record: whether Lean and Lake were found, the build return code, line counts for standard output and standard error, source file hashes, the theorem and definition names it parsed out, and per-file line counts. The proof text and the raw tool output never reach that record. A reader gets evidence that the build ran and what it contained, not a copy of the proof.

Point is discipline

The point is the discipline around the run: a real subprocess ran, a deliberately broken proof was rejected, and no answer was smuggled in through the inputs. The point of the component is the discipline around the run. Anyone can print "Lean says it compiles." The harder claim is that a real subprocess ran, that a deliberately broken proof was rejected, and that no answer was smuggled in through the inputs.

Purpose

Guarding against a checker-free pass

The first failure mode is an integration that reports success without invoking the checker, so the witness runs a real lake build subprocess and separately compiles an invalid file it must reject. Two failure modes shape the design. The first is an integration that reports success without ever invoking the checker. The witness guards against that by running a real lake build subprocess, recording its exit status, and separately compiling an intentionally invalid Lean file to confirm the toolchain rejects it. A green result that never touched Lean is not reachable through this path.

Rejecting the circular pass

The second failure mode is a circular pass where the manifest carries the answer, so the component rejects any manifest embedding a proof body, ground truth, provider output, oracle ids, or private body. The second failure mode is a circular pass, where the input manifest quietly carries the answer. The component rejects manifests that embed a proof_body, a ground_truth_proof, provider output, oracle premise ids, or a private source body. Each of those has a named negative case. A loose witness would accept a manifest that already states the conclusion; this one does not.

The scope is small on purpose

The scope is deliberately small: Mathlib, Aesop, and Batteries imports are rejected before anything runs, so this witnesses a toy theorem under a local toolchain, not library-dependent proof work. The scope is small on purpose. Imports of Mathlib, Aesop, and Batteries are rejected before anything runs. This is a witness for a toy theorem under a local toolchain, not a claim about library-dependent proof work. That boundary is the deliverable: it shows the record-keeping a larger formal-math component would need, without borrowing authority it has not earned.

How it works

Two entry points, one builder

run drives the first-wave fixture with negative cases on and run_witness_bundle drives the exported bundle with them off, both delegating to _build_result, which runs in a fixed order. The runtime lives in src/microcosm_core/organs/formal_math_lean_proof_witness.py. Two entry points exist. run drives the first-wave fixture with include_negative=True. run_witness_bundle drives the exported public bundle with include_negative=False, and reuses a fresh prior result record through _fresh_bundle_receipt when the inputs have not changed. Both delegate the real work to _build_result, which executes in this order.

Validating copied source modules

In bundle mode validate_source_module_imports recomputes each copied module's SHA-256 against its live source, checks the declared exact-copy or replacement relation, material class, and anchors, and blocks on any mismatch. First it collects the input file set with _input_paths and, for the bundle mode, validates copied source modules with validate_source_module_imports. That function reads source_module_manifest.json, and for each declared module it recomputes the SHA-256 of the copied target, recomputes the SHA-256 of the live source it was copied from, and checks that the declared source_to_target_relation is exact_copy (matching digests, sha256_match: true) or public_replacement_source_body (distinct digests, sha256_match: false). It also checks the material class is one of the four public classes, that body_in_receipt is false, that the source ref sits under an allowed public prefix, and that every declared anchor string is present in the target. Any mismatch becomes a finding, and any finding blocks the module.

Scanning inputs and the witness manifest

It scans every input and copied artifact for forbidden material, then _validate_manifest rejects forbidden keys and non-public refs and requires the positive witness rows, Lean files, and source pattern ids. Next it scans every input and copied artifact for forbidden material with scan_paths against the public forbidden-class policy, then validates the main witness_manifest.json with _validate_manifest. That check walks the manifest for the forbidden keys, rejects non-public source refs, and requires the positive witness rows, declared Lean files, source refs, public replacement refs, projection result record refs, and source pattern ids to all be present.

Probing the toolchain and running the build

_tool_versions records whether lean and lake are on the path, then _run_command runs lake build in a temporary copy, keeping only the return code, output line counts, and timeout flag. Then it probes the toolchain. _tool_versions uses shutil.which to record whether lean and lake are on the path, and caches the answer. For the live path, _copy_project_to_temp copies the Lake project into a temporary workspace and _run_command runs lake build MicrocosmProofWitness with a 90-second timeout. _run_command captures the subprocess but keeps only the return code, the standard-output and standard-error line counts, and the timeout flag. It never keeps the output body.

Redacted per-file source metadata

_source_metadata records each positive Lean file's ref, hash, line count, declaration names, and imports with body_redacted: True, and sums the compiled declaration count across files. For each positive Lean file, _source_metadata reads the text and records its public-relative ref, its hash, its line count, the declaration names found by a theorem|lemma|def regular expression, and its imports, with body_redacted: True. The compiled declaration count is the sum across those files.

Running the rejection checks

With negatives enabled, _build_result compiles the invalid proof and forbidden-import files for real and runs _validate_negative_manifest over four tampered manifests, recording the expected code for each. When negative cases are enabled, _build_result runs the rejection checks. It copies invalid_proof.lean into the built project and runs lake env lean on it; a non-zero exit records LEAN_WITNESS_INVALID_PROOF_REJECTED. It scans mathlib_import_forbidden.lean with _forbidden_imports and records LEAN_WITNESS_FORBIDDEN_IMPORT when a blocked import is present. It then runs _validate_negative_manifest over four tampered manifests for the private-source-ref, proof-body, provider-output, and oracle-premise-id cases.

Computing the final status

A result is pass only when Lean and Lake are present, the build returned 0, the manifest and bundle modules validated, no forbidden import appeared, no negative case is missing, and the scan is clean. Finally the status is computed. A result is pass only when Lean and Lake are available, the Lake build returned 0, the manifest validated, bundle source modules validated when in bundle mode, no forbidden imports appeared in the positive files, no expected negative case is missing, and the non-public-state scan found zero blocking hits. Otherwise the status is blocked. _build_result returns the record with the scope limit, the compiled declaration count, the redacted tool metadata, and the source file metadata attached.

flowchart TD A["Fixture input witness_manifest.json + lake_project"] --> B["run() include_negative=true"] C["Exported bundle source_module_manifest.json"] --> D["run_witness_bundle() include_negative=false"] B --> E["_build_result"] D --> E E --> F["_validate_manifest reject proof bodies, non-public source refs"] E --> G["validate_source_module_imports recompute copied digests, check exact_copy vs replacement"] E --> H["_tool_versions lean/lake on path?"] H --> I["_run_command lake build MicrocosmProofWitness"] I --> J["Negative cases: invalid proof rejected, forbidden import blocked"] F --> K["metadata-only result record: return code, line counts, hashes, declaration names"] G --> K I --> K J --> K

Negative cases

Fixture ships six

The fixture ships six named negative cases, each with an expected error code, defined in EXPECTED_NEGATIVE_CASES. The fixture ships six named negative cases, each with an expected error code, defined in EXPECTED_NEGATIVE_CASES.

Six refusals, each with a code

A real invalid proof, a blocked import, and four tampered manifests each raise their named error code, and if any expected case is not observed the run is blocked. An invalid Lean proof (invalid_proof.lean) is compiled for real and must fail: LEAN_WITNESS_INVALID_PROOF_REJECTED. A file importing a blocked library (mathlib_import_forbidden.lean) is caught before execution: LEAN_WITNESS_FORBIDDEN_IMPORT. A manifest citing a non-public source refs is refused: LEAN_WITNESS_PRIVATE_SOURCE_REF_FORBIDDEN. A manifest embedding a proof body is refused: LEAN_WITNESS_PROOF_BODY_IN_MANIFEST_FORBIDDEN. A manifest carrying provider output is refused: LEAN_WITNESS_PROVIDER_OUTPUT_IN_MANIFEST_FORBIDDEN. A manifest carrying oracle premise ids is refused: LEAN_WITNESS_ORACLE_PREMISE_IDS_IN_MANIFEST_FORBIDDEN. If any expected case is not observed, the run is blocked.

Prior Art Grounding

The Lean proof-assistant lineage

The component sits in the Lean small-kernel lineage, borrowing the discipline of a local toolchain run with source hashes, declaration names, negative cases, and metadata-only records, not Mathlib-dependent authority. This component sits in the Lean proof-assistant lineage and the small-kernel theorem-proving tradition it belongs to. The Lean theorem prover system description describes the toolchain this witness invokes, and the Lean mathematical library shows why real proof authority depends on explicit imports, declarations, and a checked environment. The witness borrows the discipline, a local toolchain run with source hashes, declaration names, negative cases, and metadata-only records, before any Lean-witness language is allowed. It does not borrow Mathlib-dependent proof authority.

Validation Result record Path

./repo-pytest tests/test_formal_math_lean_proof_witness.py -q --basetemp=/tmp/microcosm_formal_math_lean_proof_witness_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus
jq '{edge_count:(.relationships.edges|length), mermaid_status:.paper_module_payload.generated_projections.mermaid.status, atlas_status:.paper_module_payload.generated_projections.atlas_card.status, source_authority:.relationships.source_authority, unresolved_selective_relation_count:(.relationships.unpopulated_selective_relations|length)}' paper_modules/formal_math_lean_proof_witness.json

What a pass means here

A pass means the focused test saw a real Lake build for the toy witness, the six negative cases, redacted records, and a generated row reporting edge_count: 8 and source_authority: json_capsule. A pass means the focused test saw a successful Lake build for the toy witness when Lean and Lake were available, saw the six negative cases, saw public-relative redacted records, and the generated row reports edge_count: 8, mermaid_status: available_from_capsule_edges, source_authority: json_capsule, and zero unresolved selective relations.

To run the component directly:

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