Challenges: Odlyzko root-discriminant bound and Mazur's torsion bound

[Vilin97]

The first two entries on the challenge board, and the first real exercise of the machinery in #288 (stacked on it; retarget to main once that merges).

Both are results the FLT project assumes and does not plan to prove itself — FLT/Assumptions/ states each as an axiom with a literature reference. They are stated here verbatim as FLT needs them, Apache-2.0 with the upstream headers retained.

Challenge.Odlyzko.abs_discr_ge

A totally complex number field of degree ≥ 18 has |discr K| ≥ 8.25 ^ finrank ℚ K — root discriminant at least 8.25. Minkowski's elementary bound is too weak; this comes from Poitou's simplification of Odlyzko's analysis of the zeros of the Dedekind zeta function (equation 26 and the table on p17 of "Sur les petits discriminants").

FLT tracking issue #458 links Thomas Browning's notes on an approach. Buzzard calls it one of the easiest of the results FLT assumes.

Challenge.Mazur.torsion_ncard_le

The torsion subgroup of E(ℚ) has at most 16 elements — the numerical consequence of Mazur's 1977 classification (cyclic of order ≤ 10 or 12, and ℤ/2ℤ × ℤ/nℤ for n = 2, 4, 6, 8). Every known proof of FLT uses it. FLT tracking issue #477.

Note Set.ncard returns 0 on an infinite set, so the statement reads "at most 16, or infinite". That is the form FLT assumes — finiteness of the torsion subgroup is classical and far easier — and both the card and the registry's informal statement say so.

What this exercises in #288

The statement gates (Mathlib-only imports, sorry restricted to the registered declarations, #print axioms confirming each registered statement is open and nothing else in the file rests on sorryAx), the generated cards, mk_all on the Challenge library, and the challenge review path. challenge-verify.yml has nothing to verify yet — both are open.

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

This PR adds the first two entries to the Lean Pool challenge board: an Odlyzko root-discriminant bound for totally complex number fields and Mazur's torsion bound for elliptic curves over ℚ, both stated verbatim as the FLT project assumes them.

• Challenge.Odlyzko.abs_discr_ge: States that a totally complex number field of degree ≥ 18 has |disc K| ≥ 8.25^(finrank ℚ K), correctly importing IsTotallyComplex and the discriminant definitions from Mathlib; the 8.25 decimal literal elaborates to 33/4 in ℝ via OfScientific, and the ℤ → ℝ coercion on discr K is standard.
• Challenge.Mazur.torsion_ncard_le: States that the torsion subgroup of (E⁄ℚ).Point has Set.ncard ≤ 16; the intentional weakening (ncard returns 0 for infinite sets, so this reads "at most 16 or infinite") is explicitly documented in both the docstring and the YAML informal statement, matching the FLT assumption exactly.
• Both registry entries carry all required YAML fields, module docstrings are consistent with what --write-challenge-cards would generate from challenges.yml, imports are strictly Mathlib-only, and the Challenge.lean index is updated.

Confidence Score: 5/5

Safe to merge; adds two well-formed open challenge statements with no closed proof code beyond the sorry stubs.

Both Lean statements typecheck structurally, the module docstrings are consistent with the YAML entries (the quality gate will verify this), imports are Mathlib-only, and the intentional Set.ncard weakening in the Mazur statement is explicitly documented. No regressions to existing pool code are possible since challenge files are isolated by design.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
Challenge/Odlyzko.lean	New challenge file for the Odlyzko root-discriminant bound; statement faithfully encodes the informal description, imports are Mathlib-only, module docstring matches what the card generator would produce from challenges.yml.
Challenge/Mazur.lean	New challenge file for Mazur's torsion bound; Set.ncard semantics (returns 0 on infinite sets) are intentionally and explicitly documented in both the docstring and the informal YAML entry, matching the FLT project's stated assumption.
Challenge/challenges.yml	Two new registry entries; all required fields present and consistent with the Lean files.
Challenge.lean	Top-level index updated with import statements for both new challenge modules; consistent with running lake exe mk_all on the Challenge library.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    CL["Challenge.lean\n(top-level index)"]
    CM["Challenge/Mazur.lean\ntorsion_ncard_le := sorry"]
    CO["Challenge/Odlyzko.lean\nabs_discr_ge := sorry"]
    CY["Challenge/challenges.yml\nregistry"]

    CL -->|"import Challenge.Mazur"| CM
    CL -->|"import Challenge.Odlyzko"| CO

    CM -->|"registered in"| CY
    CO -->|"registered in"| CY

    M1["Mathlib.AlgebraicGeometry\n.EllipticCurve.Affine.Point"]
    M2["Mathlib.GroupTheory.Torsion"]
    M3["Mathlib.NumberTheory.NumberField\n.Discriminant.Defs"]
    M4["Mathlib.NumberTheory.NumberField\n.InfinitePlace.TotallyRealComplex"]

    CM -->|"import"| M1
    CM -->|"import"| M2
    CO -->|"import"| M3
    CO -->|"import"| M4

    CY -->|"card sync gate\n(quality.py)"| CM
    CY -->|"card sync gate\n(quality.py)"| CO

Loading

_{Reviews (4): Last reviewed commit: "Challenges: Odlyzko root-discriminant bo..." | Re-trigger Greptile}

[github-actions]

🤖 LLM review — challenge (gpt-5.6-sol)

Reviewed head: 47416c29e8c31b994d4a2f3dd1302d5c5ce72ce7

Verdict: ✅ approve

This PR adds two established but unformalized inputs used by the FLT project: the Poitou–Odlyzko discriminant bound for totally complex fields of degree at least 18, and the numerical consequence of Mazur’s torsion classification giving a maximum finite torsion size of 16. Both Lean declarations match their registry prose, including the intentional infinite-set behavior of Set.ncard, and both belong on the board.

Aspect	Value
Significance	✅ high
Faithful to the prose	✅ faithful
Matches cited source	✅ matches
Vacuity risk	✅ none
Difficulty	research
Estimated solution size	~55,000 lines — This aggregates roughly 50000 lines for Mazur’s theorem, whose modular-curve, Jacobian, and Eisenstein-ideal infrastructure is absent from Mathlib, and roughly 5000 for the explicit-formula and numerical analysis behind the Odlyzko bound.

Statement check: The Odlyzko declaration states the exact degree, signature, and discriminant inequality from the prose, while the Mazur declaration states that finite rational torsion has cardinality at most 16 and deliberately assigns cardinality zero in the infinite case.

Both challenges are significant, faithful numerical consequences of the cited results and have no evident vacuity, trivial proof, or gameable formulation.

---

Tokens: 5,073 in / 6,546 out · Tier: flex · Effort: xhigh · Cost: $0.1109
Automated review against .github/CHALLENGE_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

/review

Re-running the challenge review to confirm the notation fix in #291: the first pass rendered over ℚ as over ^R09.

[Vilin97]

/review — re-run to live-test the gpt-5.6-sol @ xhigh upgrade (752d7bf); comparing cost against the gpt-5.5 baseline on the same head.