Polynomial Freiman-Ruzsa (PFR)
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
- 76
- Declarations
- 1083
- Contain sorry
- 6
- Axioms
- 0
Lean4 Domain Explanation Language (L4DEL): 494 annotated, 0 flagged (errors or placeholders), 533 without an L4DEL annotation. Run lean4-explainer annotate --file <path> for templates. Lean run with Lean (version 4.35.0-rc4, x86_64-w64-windows-gnu, commit c29b6dda4f7c20e3eeaa717c4e565663c5cfa364, Release) (cache-only rendering).
1083 declarations, 6 contain sorry, 0 declared as axioms; 76 files
Folders
- PFR/ 73 files, 1067 declarations
- PFRPalomar/ 2 files, 16 declarations
Files
- PFR.lean 73 imports, no declarations