Theorem Proving in Lean 4
Generated by a source-level scanner, plus a Lean run where it succeeded: see the Trust page. Trust is UNKNOWN wherever Lean did not run. Indented declarations and macro-generated declarations are not listed.
- Lean files
- 35
- Declarations
- 1258
- Contain sorry
- 64
- Axioms
- 14
Lean4 Domain Explanation Language (L4DEL): 34 annotated, 0 flagged (errors or placeholders), 781 without an L4DEL annotation. Run lean4-explainer annotate --file <path> for templates. Lean run with Lean (version 4.34.0-rc1, x86_64-w64-windows-gnu, commit 3447a668783dbce1a8fdb97101dd067687b2b418, Release) (cache-only rendering).
1258 declarations, 64 contain sorry, 14 declared as axioms; 35 files