Fermat's Last Theorem (FLT)

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

265

Declarations

3684

Contain sorry

50

Axioms

3

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

3684 declarations, 50 contain sorry, 3 declared as axioms; 265 files