From c4c79ddc4667ea823d223122a23a418a29a8ae05 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 6 Nov 2026 20:00:52 +0000 Subject: [PATCH 1/3] Rename ramanujan_petersson to Ramanujan's conjecture and fix informal proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Following the Zulip discussion (Sphere packing in 8 dimensions > SphereCeti): - The bound |τ(p)| ≤ 2 p^(11/2) is Ramanujan's conjecture alone; the Ramanujan–Petersson conjecture is Petersson's generalisation to all cuspidal eigenforms. Retitle the problem and update the notes and Lean docstrings accordingly, and drop Petersson's paper from the sources. - The informal proof wrongly located τ(p) in the étale cohomology of the universal elliptic curve. Weight-12 eigenvalues live in H¹_! of the modular curve with coefficients in Sym¹⁰ R¹f_*Q_ℓ, and through it in H¹¹ of the 10-fold fibre power (Kuga–Sato variety). Rewrite the sketch: Eichler–Shimura isomorphism and congruence relation give X² − τ(p)X + p¹¹, and purity comes either from Weil I applied to a smooth compactification of the Kuga–Sato variety (Deligne 1969/1974) or from Weil II applied to the sheaf directly (Freitag–Kiehl). Add the Weil II and Freitag–Kiehl references. The problem ID and the theorem name stay `ramanujan_petersson`: the ID is a member of the frozen v1 set, and renaming the theorem would change the trusted statement and require a statement revision. The Lean statement itself is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01SXjhFkcnZG1eciaA1Rjhdh --- LeanEval/NumberTheory/RamanujanTau.lean | 11 ++++++----- manifests/problems/ramanujan_petersson.toml | 8 ++++---- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/LeanEval/NumberTheory/RamanujanTau.lean b/LeanEval/NumberTheory/RamanujanTau.lean index ecedddb75..890dd63a1 100644 --- a/LeanEval/NumberTheory/RamanujanTau.lean +++ b/LeanEval/NumberTheory/RamanujanTau.lean @@ -6,14 +6,15 @@ namespace NumberTheory namespace RamanujanTauProblem /-! -# The Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem) +# Ramanujan's conjecture for the τ-function (Deligne's theorem) The Ramanujan τ-function is defined by the Fourier expansion `Δ = ∑_{n ≥ 1} τ(n) qⁿ` of the modular discriminant `Δ(z) = η(z)²⁴ = q ∏_{n ≥ 1} (1 - qⁿ)²⁴`, the normalised cusp form of weight `12` and level `1`. Ramanujan (1916) conjectured that `|τ(p)| ≤ 2 p^(11/2)` -for every prime `p`; Petersson generalised the conjecture to all cusp forms, -and Deligne proved it in 1974 as a consequence of the Weil conjectures. +for every prime `p`, and Deligne proved it in 1974 using his proof of the Weil +conjectures. This bound is due to Ramanujan alone; the Ramanujan–Petersson +conjecture is Petersson's generalisation to all cuspidal Hecke eigenforms. Here `τ n` is the `n`-th `q`-expansion coefficient of mathlib's `ModularForm.discriminant`. The coefficients are a priori complex, so the @@ -29,8 +30,8 @@ noncomputable def τ (n : ℕ) : ℂ := (qExpansion 1 discriminant).coeff n /-- Normalisation check: `τ 1 = 1`. -/ theorem τ_one : τ 1 = 1 := discriminant_qExpansion_coeff_one -/-- **The Ramanujan–Petersson conjecture for `τ`** (Ramanujan 1916; proved by -Deligne in 1974). For every prime `p`, `|τ(p)| ≤ 2 p^(11/2)`. -/ +/-- **Ramanujan's conjecture for `τ`** (Ramanujan 1916; proved by Deligne in +1974). For every prime `p`, `|τ(p)| ≤ 2 p^(11/2)`. -/ @[eval_problem] theorem ramanujan_petersson : ∀ p : ℕ, Prime p → ‖τ p‖ ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 2) := by diff --git a/manifests/problems/ramanujan_petersson.toml b/manifests/problems/ramanujan_petersson.toml index af7bc2e1a..ce2802fdc 100644 --- a/manifests/problems/ramanujan_petersson.toml +++ b/manifests/problems/ramanujan_petersson.toml @@ -1,5 +1,5 @@ id = "ramanujan_petersson" -title = "Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem)" +title = "Ramanujan's conjecture for the τ-function (Deligne's theorem)" group = "formalization-evaluation" status = "active" visible = true @@ -8,9 +8,9 @@ tags = [] module = "LeanEval.NumberTheory.RamanujanTau" holes = ["ramanujan_petersson"] submitter = "Seewoo Lee" -notes = "τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916) conjectured |τ(p)| ≤ 2 p^(11/2) for every prime p; Petersson generalised it to all cusp forms, and Deligne proved it in 1974 from the Weil conjectures. The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖." -source = "S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. H. Petersson, 'Theorie der automorphen Formen beliebiger reeller Dimension und ihre Darstellung durch eine neue Art Poincaréscher Reihen', Math. Ann. 103 (1930) 369–436. P. Deligne, 'Formes modulaires et représentations ℓ-adiques', Séminaire Bourbaki 1968/69: Exposés 347–363, Lecture Notes in Math. 179, Springer (1971). P. Deligne, 'La conjecture de Weil. I', Publ. Math. IHÉS 43 (1974) 273–307. Background: https://en.wikipedia.org/wiki/Ramanujan%E2%80%93Petersson_conjecture" -informal_solution = "Deligne's proof: the ℓ-adic Galois representation attached to Δ (Eichler–Shimura, Deligne) realises τ(p) as the trace of Frobenius on a weight-11 piece of the étale cohomology of the universal elliptic curve over the modular curve, and Deligne's proof of the Weil conjectures (1974) gives Frobenius eigenvalues α, β with αβ = p¹¹ and |α| = |β| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2)." +notes = "τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916) conjectured |τ(p)| ≤ 2 p^(11/2) for every prime p, and Deligne proved it in 1974 using his proof of the Weil conjectures. This bound on τ is due to Ramanujan alone; the Ramanujan–Petersson conjecture is Petersson's generalisation to the Hecke eigenvalues of all cuspidal eigenforms, and is not what is stated here. The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖." +source = "S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. P. Deligne, 'Formes modulaires et représentations ℓ-adiques', Séminaire Bourbaki 1968/69, Exposé 355, Lecture Notes in Math. 179, Springer (1971) 139–172. P. Deligne, 'La conjecture de Weil. I', Publ. Math. IHÉS 43 (1974) 273–307. P. Deligne, 'La conjecture de Weil. II', Publ. Math. IHÉS 52 (1980) 137–252. E. Freitag and R. Kiehl, 'Étale Cohomology and the Weil Conjecture', Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 13, Springer (1988). Background: https://en.wikipedia.org/wiki/Ramanujan_tau_function" +informal_solution = "Deligne's proof. Δ is a normalised Hecke eigenform, so T_p Δ = τ(p) Δ. Fix N ≥ 4 prime to p and a prime ℓ ≠ p, let M be the modular curve over Z[1/N] classifying elliptic curves with a point of order N (a fine moduli scheme), and let f : E → M be the universal elliptic curve. τ(p) does not come from the cohomology of E itself: Hecke eigenvalues of forms of weight k appear in the cohomology of the base M with coefficients in the lisse sheaf Sym^(k−2) R¹f_*Q_ℓ, and through it in H^(k−1) of the (k−2)-fold fibre power E ×_M ⋯ ×_M E. For Δ (k = 12) the sheaf is V = Sym¹⁰ R¹f_*Q_ℓ. Shimura's form of the Eichler–Shimura isomorphism identifies the parabolic cohomology H¹_!(M(C), Sym¹⁰ R¹f_*Z) ⊗ C (the image of compactly supported cohomology in ordinary cohomology) with S₁₂(Γ₁(N)) ⊕ conj(S₁₂(Γ₁(N))), compatibly with the Hecke operators. By the comparison theorem the ℓ-adic group H¹_!(M_Q̄, V) has the same Hecke eigenvalues, and it also carries an action of Gal(Q̄/Q) that is unramified at p. The Eichler–Shimura congruence relation T_p = Frob_p + p¹¹⟨p⟩ Frob_p⁻¹ then shows that on the non-zero Δ-isotypic part of H¹_!(M_Q̄, V), on which ⟨p⟩ acts trivially, Frobenius at p satisfies X² − τ(p)X + p¹¹ = 0. So Frobenius has an eigenvalue α there that is a root of this polynomial, and with β = p¹¹/α we get τ(p) = α + β. Purity gives |α| = p^(11/2) for every complex embedding, in either of two ways: Deligne (Bourbaki 1969) realises H¹_!(M_Q̄, V) as a direct summand of H¹¹ of a smooth projective compactification of the Kuga–Sato variety E ×_M ⋯ ×_M E (10 factors), which has good reduction at p, so Weil I (1974) applies; or Weil II (1980), applied to V, which is pure of weight 10, shows directly that H¹_! is pure of weight 11 without taking the fibre power, as in Freitag–Kiehl. Then |β| = p¹¹/|α| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2)." [[status_history]] status = "active" From 0cffe1dd35b6482a4db43e95276fc8b4a8c63288 Mon Sep 17 00:00:00 2001 From: Seewoo Lee <49933279+seewoo5@users.noreply.github.com> Date: Sat, 7 Nov 2026 18:17:23 +0100 Subject: [PATCH 2/3] Apply suggestion from @alreadydone Co-authored-by: Junyan Xu --- manifests/problems/ramanujan_petersson.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manifests/problems/ramanujan_petersson.toml b/manifests/problems/ramanujan_petersson.toml index ce2802fdc..98aabafc1 100644 --- a/manifests/problems/ramanujan_petersson.toml +++ b/manifests/problems/ramanujan_petersson.toml @@ -8,7 +8,7 @@ tags = [] module = "LeanEval.NumberTheory.RamanujanTau" holes = ["ramanujan_petersson"] submitter = "Seewoo Lee" -notes = "τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916) conjectured |τ(p)| ≤ 2 p^(11/2) for every prime p, and Deligne proved it in 1974 using his proof of the Weil conjectures. This bound on τ is due to Ramanujan alone; the Ramanujan–Petersson conjecture is Petersson's generalisation to the Hecke eigenvalues of all cuspidal eigenforms, and is not what is stated here. The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖." +notes = "τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916) conjectured |τ(p)| ≤ 2 p^(11/2) for every prime p; Petersson generalised it to all cusp forms, and Deligne (1971) used the Eichler–Shimura isomorphism to reduce the Ramanujan–Petersson conjecture to the Weil conjectures that he later proved (1974). The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖." source = "S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. P. Deligne, 'Formes modulaires et représentations ℓ-adiques', Séminaire Bourbaki 1968/69, Exposé 355, Lecture Notes in Math. 179, Springer (1971) 139–172. P. Deligne, 'La conjecture de Weil. I', Publ. Math. IHÉS 43 (1974) 273–307. P. Deligne, 'La conjecture de Weil. II', Publ. Math. IHÉS 52 (1980) 137–252. E. Freitag and R. Kiehl, 'Étale Cohomology and the Weil Conjecture', Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 13, Springer (1988). Background: https://en.wikipedia.org/wiki/Ramanujan_tau_function" informal_solution = "Deligne's proof. Δ is a normalised Hecke eigenform, so T_p Δ = τ(p) Δ. Fix N ≥ 4 prime to p and a prime ℓ ≠ p, let M be the modular curve over Z[1/N] classifying elliptic curves with a point of order N (a fine moduli scheme), and let f : E → M be the universal elliptic curve. τ(p) does not come from the cohomology of E itself: Hecke eigenvalues of forms of weight k appear in the cohomology of the base M with coefficients in the lisse sheaf Sym^(k−2) R¹f_*Q_ℓ, and through it in H^(k−1) of the (k−2)-fold fibre power E ×_M ⋯ ×_M E. For Δ (k = 12) the sheaf is V = Sym¹⁰ R¹f_*Q_ℓ. Shimura's form of the Eichler–Shimura isomorphism identifies the parabolic cohomology H¹_!(M(C), Sym¹⁰ R¹f_*Z) ⊗ C (the image of compactly supported cohomology in ordinary cohomology) with S₁₂(Γ₁(N)) ⊕ conj(S₁₂(Γ₁(N))), compatibly with the Hecke operators. By the comparison theorem the ℓ-adic group H¹_!(M_Q̄, V) has the same Hecke eigenvalues, and it also carries an action of Gal(Q̄/Q) that is unramified at p. The Eichler–Shimura congruence relation T_p = Frob_p + p¹¹⟨p⟩ Frob_p⁻¹ then shows that on the non-zero Δ-isotypic part of H¹_!(M_Q̄, V), on which ⟨p⟩ acts trivially, Frobenius at p satisfies X² − τ(p)X + p¹¹ = 0. So Frobenius has an eigenvalue α there that is a root of this polynomial, and with β = p¹¹/α we get τ(p) = α + β. Purity gives |α| = p^(11/2) for every complex embedding, in either of two ways: Deligne (Bourbaki 1969) realises H¹_!(M_Q̄, V) as a direct summand of H¹¹ of a smooth projective compactification of the Kuga–Sato variety E ×_M ⋯ ×_M E (10 factors), which has good reduction at p, so Weil I (1974) applies; or Weil II (1980), applied to V, which is pure of weight 10, shows directly that H¹_! is pure of weight 11 without taking the fibre power, as in Freitag–Kiehl. Then |β| = p¹¹/|α| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2)." From 82d2b6929f08804b4f8006a360db8e59976431eb Mon Sep 17 00:00:00 2001 From: Seewoo Lee <49933279+seewoo5@users.noreply.github.com> Date: Sun, 8 Nov 2026 13:54:32 +0100 Subject: [PATCH 3/3] Apply suggestion from @alreadydone Co-authored-by: Junyan Xu --- manifests/problems/ramanujan_petersson.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manifests/problems/ramanujan_petersson.toml b/manifests/problems/ramanujan_petersson.toml index 98aabafc1..d6be94ba3 100644 --- a/manifests/problems/ramanujan_petersson.toml +++ b/manifests/problems/ramanujan_petersson.toml @@ -10,7 +10,7 @@ holes = ["ramanujan_petersson"] submitter = "Seewoo Lee" notes = "τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916) conjectured |τ(p)| ≤ 2 p^(11/2) for every prime p; Petersson generalised it to all cusp forms, and Deligne (1971) used the Eichler–Shimura isomorphism to reduce the Ramanujan–Petersson conjecture to the Weil conjectures that he later proved (1974). The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖." source = "S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. P. Deligne, 'Formes modulaires et représentations ℓ-adiques', Séminaire Bourbaki 1968/69, Exposé 355, Lecture Notes in Math. 179, Springer (1971) 139–172. P. Deligne, 'La conjecture de Weil. I', Publ. Math. IHÉS 43 (1974) 273–307. P. Deligne, 'La conjecture de Weil. II', Publ. Math. IHÉS 52 (1980) 137–252. E. Freitag and R. Kiehl, 'Étale Cohomology and the Weil Conjecture', Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 13, Springer (1988). Background: https://en.wikipedia.org/wiki/Ramanujan_tau_function" -informal_solution = "Deligne's proof. Δ is a normalised Hecke eigenform, so T_p Δ = τ(p) Δ. Fix N ≥ 4 prime to p and a prime ℓ ≠ p, let M be the modular curve over Z[1/N] classifying elliptic curves with a point of order N (a fine moduli scheme), and let f : E → M be the universal elliptic curve. τ(p) does not come from the cohomology of E itself: Hecke eigenvalues of forms of weight k appear in the cohomology of the base M with coefficients in the lisse sheaf Sym^(k−2) R¹f_*Q_ℓ, and through it in H^(k−1) of the (k−2)-fold fibre power E ×_M ⋯ ×_M E. For Δ (k = 12) the sheaf is V = Sym¹⁰ R¹f_*Q_ℓ. Shimura's form of the Eichler–Shimura isomorphism identifies the parabolic cohomology H¹_!(M(C), Sym¹⁰ R¹f_*Z) ⊗ C (the image of compactly supported cohomology in ordinary cohomology) with S₁₂(Γ₁(N)) ⊕ conj(S₁₂(Γ₁(N))), compatibly with the Hecke operators. By the comparison theorem the ℓ-adic group H¹_!(M_Q̄, V) has the same Hecke eigenvalues, and it also carries an action of Gal(Q̄/Q) that is unramified at p. The Eichler–Shimura congruence relation T_p = Frob_p + p¹¹⟨p⟩ Frob_p⁻¹ then shows that on the non-zero Δ-isotypic part of H¹_!(M_Q̄, V), on which ⟨p⟩ acts trivially, Frobenius at p satisfies X² − τ(p)X + p¹¹ = 0. So Frobenius has an eigenvalue α there that is a root of this polynomial, and with β = p¹¹/α we get τ(p) = α + β. Purity gives |α| = p^(11/2) for every complex embedding, in either of two ways: Deligne (Bourbaki 1969) realises H¹_!(M_Q̄, V) as a direct summand of H¹¹ of a smooth projective compactification of the Kuga–Sato variety E ×_M ⋯ ×_M E (10 factors), which has good reduction at p, so Weil I (1974) applies; or Weil II (1980), applied to V, which is pure of weight 10, shows directly that H¹_! is pure of weight 11 without taking the fibre power, as in Freitag–Kiehl. Then |β| = p¹¹/|α| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2)." +informal_solution = "Deligne's proof. Δ is a normalised Hecke eigenform, so Tₚ Δ = τ(p) Δ. Fix N ≥ 4 prime to p and a prime ℓ ≠ p, let ℳ be the modular curve over ℤ[1/N] classifying elliptic curves with a point of order N (a fine moduli scheme), and let f : ℰ → ℳ be the universal elliptic curve. τ(p) does not come from the cohomology of ℰ itself: Hecke eigenvalues of forms of weight k appear in the cohomology of the base ℳ with coefficients in the lisse sheaf Symᵏ⁻² R¹f_*ℚ_ℓ, and through it in Hᵏ⁻¹ of the (k−2)-fold fibre power ℰ ×_ℳ ⋯ ×_ℳ ℰ. For Δ (k = 12) the sheaf is V = Sym¹⁰ R¹f_*ℚ_ℓ. Shimura's form of the Eichler–Shimura isomorphism identifies the parabolic cohomology H¹_!(ℳ(ℂ), Sym¹⁰ R¹f_*ℤ) ⊗ ℂ (the image of compactly supported cohomology in ordinary cohomology) with S₁₂(Γ₁(N)) ⊕ conj(S₁₂(Γ₁(N))), compatibly with the Hecke operators. By the comparison theorem the ℓ-adic group H¹_!(ℳ_Q̄, V) has the same Hecke eigenvalues, and it also carries an action of Gal(Q̄/ℚ) that is unramified at p. The Eichler–Shimura congruence relation Tₚ = Frobₚ + p¹¹⟨p⟩ Frobₚ⁻¹ then shows that on the non-zero Δ-isotypic part of H¹_!(ℳ_Q̄, V), on which ⟨p⟩ acts trivially, Frobenius at p satisfies X² − τ(p)X + p¹¹ = 0. So Frobenius has an eigenvalue α there that is a root of this polynomial, and with β = p¹¹/α we get τ(p) = α + β. Purity gives |α| = p^(11/2) for every complex embedding, in either of two ways: Deligne (Bourbaki 1969) realises H¹_!(ℳ_Q̄, V) as a direct summand of H¹¹ of a smooth projective compactification of the Kuga–Sato variety ℰ ×_ℳ ⋯ ×_ℳ ℰ (10 factors), which has good reduction at p, so Weil I (1974) applies; or Weil II (1980), applied to V, which is pure of weight 10, shows directly that H¹_! is pure of weight 11 without taking the fibre power, as in Freitag–Kiehl. Then |β| = p¹¹/|α| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2)." [[status_history]] status = "active"