Formal Conjectures
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
- 1725
- Declarations
- 9845
- Contain sorry
- 3790
- Axioms
- 1
Lean4 Domain Explanation Language (L4DEL): 7200 annotated, 0 flagged (errors or placeholders), 2419 without an L4DEL annotation. Run lean4-explainer annotate --file <path> for templates. Lean run with Lean (version 4.33.1, x86_64-w64-windows-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release) (cache-only rendering).
9845 declarations, 3790 contain sorry, 1 declared as axioms; 1725 files
Folders
- FormalConjectures/ 1468 files, 8236 declarations
- FormalConjecturesForMathlib/ 221 files, 1430 declarations
- FormalConjecturesTest/ 12 files, 80 declarations
- FormalConjecturesUtil/ 22 files, 99 declarations
Files
- FormalConjecturesForMathlib.lean 221 imports, no declarations
- FormalConjecturesUtil.lean 18 imports, no declarations