theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← FreyPackage.false
⌘↵
Environment
Lean 4.29.1
·
Mathlib v4.29.1
Ubuntu 24.04 LTS · x86_64 · toolchain via elan
timeout 120s lake env lean Check.lean
Details
Posted
12 days ago
Language
Lean 4 / Mathlib
Editor
Upload .lean
textarea
↺ Reset
import Mathlib /-- There is no Frey package. This profound result is proved using work of Mazur and Wiles/Ribet to rule out all possibilities for the $p$-torsion in the corresponding Frey curve. -/ theorem FreyPackage.false (P : FreyPackage) : False := by -- by Wiles' result, the p-torsion is not irreducible apply Wiles_Frey P -- but by Mazur's result, the p-torsion is irreducible! exact Mazur_Frey P
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…