Mathematics in Lean

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

88

Declarations

1646

Contain sorry

246

Axioms

0

Lean4 Domain Explanation Language (L4DEL): 16 annotated, 0 flagged (errors or placeholders), 583 without an L4DEL annotation. Run lean4-explainer annotate --file <path> for templates. Lean run with Lean (version 4.30.0, x86_64-w64-windows-gnu, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release) (cache-only rendering).

1646 declarations, 246 contain sorry, 0 declared as axioms; 88 files