The Regula Standard🔗

This standard specifies requirements for mathematical proofs and verified functional programs in Lean.

Public review draft; not affiliated with the Lean FRO or Mathlib.

1. Introduction
2. 0. Precise Claims and Kernel-Checked Evidence
3. 1. Core Principles
4. 2. Type Design Patterns
5. 3. Logic and Proof Patterns
6. 4. Mathematical Foundations
7. 5. Documentation Standards
8. 6. Code Organization
9. 7. Tooling and Machine Audit
10. 8. Compliance and Quality Audit
11. Critical Violations to Check First