diff --git a/Challenge.lean b/Challenge.lean index 8b13789179..4deed19ae2 100644 --- a/Challenge.lean +++ b/Challenge.lean @@ -1 +1,2 @@ - +import Challenge.Mazur +import Challenge.Odlyzko diff --git a/Challenge/Mazur.lean b/Challenge/Mazur.lean new file mode 100644 index 0000000000..34cfe9ea34 --- /dev/null +++ b/Challenge/Mazur.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2025 Kevin Buzzard. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Buzzard +-/ + +import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point +import Mathlib.GroupTheory.Torsion + +/-! +# Mazur's bound on the torsion of an elliptic curve over the rationals + +Source: doi:10.1007/BF02684339, url:https://www.numdam.org/item/?id=PMIHES_1977__47__33_0 +Proposed by: Kevin Buzzard, Vasily Ilin +Status: open +Open declarations: `Challenge.Mazur.torsion_ncard_le` +Tags: elliptic-curves, torsion, modular-curves, flt-assumption +MSC: 11G05, 11G18 +Estimated size: ~50000 lines of Lean + +Informal statement: +* `Challenge.Mazur.torsion_ncard_le` — For every elliptic curve E over the rationals, the torsion + subgroup of the group of rational points of E, viewed as a set, has at most 16 elements. Set.ncard + returns 0 on an infinite set, so the statement reads "at most 16, or infinite"; that is the form + the FLT project assumes, since finiteness of the torsion subgroup is classical and far easier. +-/ + +namespace Challenge.Mazur + +open scoped WeierstrassCurve.Affine + +/-- **Mazur's torsion theorem**, in the form the Fermat's Last Theorem project assumes it as +`FLT.Assumptions.Mazur_statement`: the torsion subgroup of the group of rational points of an +elliptic curve over `ℚ` has at most 16 elements. Mazur classified the possible torsion +subgroups — cyclic of order `n ≤ 10` or `n = 12`, or `ℤ/2ℤ × ℤ/nℤ` for `n = 2, 4, 6, 8` — and +16 is the largest resulting size. + +`Set.ncard` returns `0` on an infinite set, so this says "at most 16, or infinite". That is +enough for the application, because finiteness of the torsion subgroup is a much easier +classical fact (Mordell--Weil); a solution is welcome to prove finiteness as well. -/ +theorem torsion_ncard_le (E : WeierstrassCurve ℚ) [E.IsElliptic] : + (AddCommGroup.torsion (E⁄ℚ).Point : Set (E⁄ℚ).Point).ncard ≤ 16 := sorry + +end Challenge.Mazur diff --git a/Challenge/Odlyzko.lean b/Challenge/Odlyzko.lean new file mode 100644 index 0000000000..a8f6991e7d --- /dev/null +++ b/Challenge/Odlyzko.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2025 Kevin Buzzard. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Buzzard +-/ + +import Mathlib.NumberTheory.NumberField.Discriminant.Defs +import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex + +/-! +# Odlyzko bound for root discriminants + +Source: url:https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/ +Proposed by: Kevin Buzzard, Vasily Ilin +Status: open +Open declarations: `Challenge.Odlyzko.abs_discr_ge` +Tags: number-theory, discriminants, number-fields, flt-assumption +MSC: 11R29, 11R42 +Estimated size: ~5000 lines of Lean + +Informal statement: +* `Challenge.Odlyzko.abs_discr_ge` — For a totally complex number field K whose degree over the + rationals is at least 18, the absolute value of the discriminant of K is at least 8.25 raised to + the power of that degree. +-/ + +namespace Challenge.Odlyzko + +open Module NumberField + +/-- An **Odlyzko bound** for the root discriminant of a totally complex number field of degree +18 and above: such a field has root discriminant at least `8.25`. Minkowski's elementary +argument is not strong enough; the bound comes from analysing the zeros of the Dedekind zeta +function of `K`. Stated verbatim as the Fermat's Last Theorem project needs it, where it is +assumed as `FLT.Assumptions.Odlyzko_statement`. -/ +theorem abs_discr_ge (K : Type*) [Field K] [NumberField K] [IsTotallyComplex K] + (hdim : finrank ℚ K ≥ 18) : |(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K := sorry + +end Challenge.Odlyzko diff --git a/Challenge/challenges.yml b/Challenge/challenges.yml new file mode 100644 index 0000000000..ebee52d3ab --- /dev/null +++ b/Challenge/challenges.yml @@ -0,0 +1,103 @@ +# Registry of Lean Pool challenges: open statements awaiting a proof. +# +# One entry per challenge. `statements` (and the optional `definitions`) name +# the declarations that may be left as `sorry` in the entry module; every other +# declaration in that file must be closed. `informal` is the natural-language +# statement the Lean is judged against — keep the two saying the same thing. +# +# Regenerate the cards after editing: +# cd python && uv run python -m lean_pool.quality --repo .. --write-challenge-cards +challenges: + - slug: odlyzko-root-discriminant-bound + title: Odlyzko bound for root discriminants + summary: >- + Prove that a totally complex number field of degree at least 18 has + absolute discriminant at least 8.25 raised to the degree — equivalently, + root discriminant at least 8.25. Minkowski's elementary bound is too weak; + the result comes from analysing the zeros of the Dedekind zeta function of + the field, and follows from equation 26 and the table on p17 of Poitou's + 1977 "Sur les petits discriminants". The Fermat's Last Theorem project + assumes it as FLT.Assumptions.Odlyzko_statement (tracking issue #458, + which also links Thomas Browning's notes on an approach); Kevin Buzzard + calls it one of the easiest of the results it assumes, and it is not on + the project's own formalization plan. The line estimate is a guess at the + analytic machinery needed — an explicit formula for the Dedekind zeta + function and the resulting inequality — not at the write-up of the + finished argument. + branch: algebraic number theory + entry_module: Challenge.Odlyzko + proposers: + - Kevin Buzzard + - Vasily Ilin + source: + title: Sur les petits discriminants + authors: + - Georges Poitou + url: https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/ + license: Apache-2.0 + provenance: human + status: open + estimated_lines: 5000 + statements: + - declaration: Challenge.Odlyzko.abs_discr_ge + informal: >- + For a totally complex number field K whose degree over the rationals + is at least 18, the absolute value of the discriminant of K is at + least 8.25 raised to the power of that degree. + tags: + - number-theory + - discriminants + - number-fields + - flt-assumption + msc: + - "11R29" + - "11R42" + - slug: mazur-torsion-bound + title: Mazur's bound on the torsion of an elliptic curve over the rationals + summary: >- + Prove that the torsion subgroup of the group of rational points of an + elliptic curve over the rationals has at most 16 elements. This is the + numerical consequence of Mazur's 1977 classification of the possible + torsion subgroups — cyclic of order at most 10 or of order 12, and + Z/2Z x Z/nZ for n = 2, 4, 6, 8 — proved in "Modular curves and the + Eisenstein ideal" by descent on the Eisenstein quotient of the Jacobian + of a modular curve of prime level. Every known proof of Fermat's Last + Theorem uses it, and the FLT project assumes it as + FLT.Assumptions.Mazur_statement (tracking issue #477); it is not on the + project's own formalization plan. The line estimate reflects that Mathlib + has none of the modular-curve machinery a proof needs, so it is an + estimate of a programme rather than of a single development; a solution + via the winding quotient and known partial results towards + Birch-Swinnerton-Dyer may be shorter than Mazur's own route. + branch: arithmetic geometry + entry_module: Challenge.Mazur + proposers: + - Kevin Buzzard + - Vasily Ilin + source: + title: Modular curves and the Eisenstein ideal + authors: + - Barry Mazur + doi: "10.1007/BF02684339" + url: https://www.numdam.org/item/?id=PMIHES_1977__47__33_0 + license: Apache-2.0 + provenance: human + status: open + estimated_lines: 50000 + statements: + - declaration: Challenge.Mazur.torsion_ncard_le + informal: >- + For every elliptic curve E over the rationals, the torsion subgroup of + the group of rational points of E, viewed as a set, has at most 16 + elements. Set.ncard returns 0 on an infinite set, so the statement + reads "at most 16, or infinite"; that is the form the FLT project + assumes, since finiteness of the torsion subgroup is classical and far + easier. + tags: + - elliptic-curves + - torsion + - modular-curves + - flt-assumption + msc: + - "11G05" + - "11G18"