Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tidy up FLT.lean #188

Merged
merged 1 commit into from
Oct 31, 2024
Merged

Tidy up FLT.lean #188

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 16 additions & 2 deletions FLT.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import FLT.FLT_files -- **FIXME** need this hack to make check_decls work in leanblueprint
import FLT.Basic.Reductions
import FLT.FLT_files -- import the project files

/-!

Expand All @@ -12,6 +11,13 @@ a proof of Mathlib's version `FermatLastTheorem`
of the statement (which is a statement about the
nonnegative integers `ℕ`.)

Note that many of the files imported by this file contain
"sorried" theorems, that is, theorems whose proofs
are not yet complete. So whilst the below looks
like a complete proof of Fermat's Last Theorem, it
currently relies on many incomplete proofs along the way,
and is likely to do so for several years.

-/

/-- Fermat's Last Theorem for positive naturals. -/
Expand All @@ -20,3 +26,11 @@ theorem PNat.pow_add_pow_ne_pow
(n : ℕ) (hn : n > 2) :
x^n + y^n ≠ z^n :=
PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn

#print axioms PNat.pow_add_pow_ne_pow
/-
'PNat.pow_add_pow_ne_pow' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
-/

-- The project will be complete when `sorryAx` is no longer
-- mentioned in the output of this last command.