Overview🔗

The numbered modules define requirements for Lean types, definitions, proofs, and the claims made about them. Module 0 states the fundamental requirement and what kernel-checked evidence establishes; module 8 is the single audit checklist, whose rows link to the modules that define each requirement and its rationale. The adoption guide sets up and runs the checker.

Scope🔗

The standard covers dependent types, theorem statements, proofs, axioms, elaboration, modules, namespaces, and Lean computation. It also covers mathematical models, executable definitions, monadic and effectful programs, and metaprograms. Each claimed surface must satisfy the applicable declaration, foundation, and computation rules; the claim kinds in module 1 §1.3 distinguish what the evidence concerns.

A complete executable component has explicit behavioral proof requirements tied to its actual Lean definitions. Types, proof-bearing constructions, and existing theorems may discharge those requirements. Semantic review must still confirm that the requirements express the intended behavior and cover the actual call paths. A logical foundation label alone does not establish execution correctness. To transfer a result to another formal representation, provide checked correspondence sufficient for that transfer. Applying a result to native execution or an external system retains the stated compiler, runtime, and external assumptions (module 3 §3.6, module 7 §7.5–§7.6).

These Lean requirements are intended for systems where correctness is critical. The standard does not certify or guarantee any external system. It does not address development lifecycles, organizational processes, traceability frameworks, CI/CD platforms, supply-chain provenance, releases, risk waivers, or certification schemes.

Document Structure🔗

Critical Violations lists issues for initial triage. The absence of a listed issue does not establish that a component conforms to the standard.

Lean Example Convention🔗

Every lean block of this standard is one complete Lean module with its own imports. When the standard is built, each block is elaborated where it is written, in a fresh environment containing exactly those imports, with autoImplicit and relaxedAutoImplicit off (module 7 §7.1) and Lean's linter.missingDocs on (module 6 §6.7). Every line of every code block is at most 100 characters, the community's line limit; a longer line fails the build of the standard. The documentation audit (module 7 §7.7) checks each block by its kind:

• Unmarked lean block: a positive elaboration example. It must first elaborate exactly as printed, with its own imports and no checker imports or wrappers inserted. The resulting module and its owned logical dependencies first pass completed kernel admission (§7.3); the module is then checked under the declaration policy with the Standard-Logical axiom allowance. Emitted warnings, proof holes, project or unknown axioms, compiler-trusting proof axioms, and forbidden declarations fail this check. The narrowly authenticated recursive-helper exception remains as specified in §7.4. A narrower foundation claim or an execution-correspondence claim requires separate evidence.

• lean (fails := "PATTERN") block: an expected elaboration failure. The nonempty pattern must be valid, the frontend must complete with source rejection and no warning, and one effective-error message must match the entire pattern under the restricted grammar of §7.7 (| alternatives and .* between ordered literal fragments, not general regular-expression syntax). The page shows such a block under the verdict Rejected by Lean, as intended, followed by the error message that matched its pattern.

• lean +trustedCompiler block: an example of a compiler-trusting proof mechanism, such as native_decide, decide +native, or bv_decide. The example must elaborate warning-free and receive the required compiler-trusting classification. Such examples are not included in conforming positive proof surfaces or in the three logical foundation labels.

• leanSketch, text or another non-Lean block: pseudocode, a multi-file sketch, or tool output. It carries no claim that the displayed text elaborates as Lean; a leanSketch block says so where it is shown.

Any other code-block spelling (an unnamed block, or an unknown name or argument), an invalid diagnostic pattern, a Lean block that does not open and close in the first column, a line with a fence run and the block name lean at any other place (in a quotation, in a list item or inside another block), a carriage return, the character U+0000, and an unclosed block fail the audit. §7.7 specifies the same three kinds as a Markdown fence protocol.

A positive example establishes the specified elaboration and declaration checks. It does not prove that the example satisfies its intended specification or every other rule: a valid Lean program may illustrate a semantic defect, which the explanation must identify. Use a negative example to claim that Lean rejects the printed code.

Requirement Keywords🔗

Throughout this standard, uppercase requirement keywords carry the meanings defined in RFC 2119:

• MUST / REQUIRED / SHALL: a condition that conformance requires.

• MUST NOT / SHALL NOT: a prohibited condition or action.

• SHOULD / RECOMMENDED: the expected choice; departing from it needs a valid technical reason and consideration of the consequences.

• SHOULD NOT / NOT RECOMMENDED: a choice to avoid unless a valid technical reason and consideration of the consequences support it.

• MAY / OPTIONAL: a choice the standard permits. When an optional claim is made, its applicable requirements must still be met.

Formal Lean statements claimed as conforming SHALL elaborate on the declared toolchain. Their explanations SHALL preserve the quantifiers, assumptions, conclusions, and relevant definitions without strengthening the result (module 5 §5.2). Kernel acceptance and fidelity to the intended claim are distinct obligations. Elaborating a Prop-valued definition establishes its statement, not a proof of that proposition. Every material result presented as established requires the checked evidence specified in module 0.