Lean evidence profile
mathgraph.lean-evidence-profile.draft-1 describes how a future record may separate proof validity, statement fidelity, execution, provenance, and generalization. No qualified Lean record currently implements this profile.
formalization.yaml metadata
The profile can carry authorship, source status, maintainers, declared automation or AI use, license status, limitations, and classifications. These fields describe provenance; they do not prove fidelity or correctness.
Statement and proof remain separate.
| Field | Purpose |
|---|---|
| Declaration names | Exact Lean names covered by the receipt. |
| Permitted axioms | Declared trusted assumptions, distinct from observed axiom output. |
| Statement SHA-256 | Identity of the statement bytes or canonical statement object. |
| Proof SHA-256 | Identity of the proof source, separate from the statement. |
| Statement fidelity | A separate axis; never inferred from kernel acceptance. |
Pin the environment that checked it.
| Field | Boundary |
|---|---|
| Lean commit | Exact compiler or verifier revision. |
| Mathlib commit | Exact library revision when used. |
| Workflow SHA-256 | Identity of the executed workflow definition. |
| Report SHA-256 | Identity of the resulting verification report. |
| Verifier versions | Named tools and exact versions, without collapsing their trust boundaries. |
Optional receipts require actual evidence.
A future record may attach a Comparator receipt, an Independent-kernel receipt, or a review Policy digest. Each receipt must name its URI, digest, and maturity. Absence remains visible.
Source links and “Open in Lean Playground” links appear only when a future qualified receipt establishes a reproducible environment. Playground convenience is not proof authority.
The current L4YAML public consequence record does not carry this Lean profile, Comparator, Playground, review-policy, or independent-kernel receipts.
Draft means unstable.
PROPOSED specifies an intended contract with no qualified adopter. EXPERIMENTAL would require an implemented research artifact and bounded evidence, but still would not be a stable production contract. This profile stays PROPOSED until a real Lean record tests and reshapes it.