From 3f18008b3dab067957e772ff20b8dbb19e3ec709 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 25 Sep 2026 03:55:48 +0800 Subject: [PATCH 1/3] feat(ComplexAnalysis): unbounded denominators conjecture --- .../UnboundedDenominators.lean | 45 +++++++++++++++++++ manifests/problems/unbounded_denominator.toml | 15 +++++++ 2 files changed, 60 insertions(+) create mode 100644 LeanEval/ComplexAnalysis/UnboundedDenominators.lean create mode 100644 manifests/problems/unbounded_denominator.toml diff --git a/LeanEval/ComplexAnalysis/UnboundedDenominators.lean b/LeanEval/ComplexAnalysis/UnboundedDenominators.lean new file mode 100644 index 00000000..be5f6dbc --- /dev/null +++ b/LeanEval/ComplexAnalysis/UnboundedDenominators.lean @@ -0,0 +1,45 @@ +import Mathlib +import EvalTools.Markers + +/-! +# Unbounded denominators conjecture + +The main theorem (Theorem 1.0.1) in *The Unbounded Denominators Conjecture* by +Frank Calegari, Vesselin Dimitrov, and Yunqing Tang (https://arxiv.org/abs/2109.09040) +states that if `f` is a modular form for some finite index subgroup of SL(2,ℤ) that +is holomorphic on the upper half-plane and at infinity and meromorphic at cusps other +than the infinity, with all Fourier (q-expansion) coefficients at infinity algebraic +integers (see Remark 6.3.1), then `f` is a modular form for some congruence subgroup of SL(2,ℤ). + +The proof uses arithmetic holonomy bounds and Nevanlinna theory, which are also central to +the three authors' subsequent work, another LeanEval challenge +https://lean-lang.org/eval/problems/cdt_linearIndependent/. + +## More references +* Published paper: https://www.math.uchicago.edu/~fcale/papers/UDC.pdf +* Séminaire Bourbaki by Javier Fresán: http://javier.fresan.perso.math.cnrs.fr/unbounded.pdf +* Vector valued version and Mason's conjecture: https://divizio.perso.math.cnrs.fr/SemDiff/dimitrov.pdf +* https://www.quantamagazine.org/long-sought-math-proof-unlocks-more-mysterious-modular-forms-20230309/ +-/ + +namespace LeanEval.ComplexAnalysis + +open scoped Manifold + +/-- A slash invariant holomorphic function `f` on the upper half-plane is meromorphic at a cusp +if every slash action that brings the cusp to infinity brings `f` to a function that is O(eⁱᵗᶻ) +for some `t : ℝ` as Im z → ∞. -/ +def IsMeromorphicAt (c : OnePoint ℝ) (f : UpperHalfPlane → ℂ) (k : ℤ) : Prop := + ∀ g : GL (Fin 2) ℝ, g • OnePoint.infty = c → + ∃ t : ℝ, SlashAction.map k g f =O[UpperHalfPlane.atImInfty] fun z ↦ (z.1 * t * .I).exp + +/-- In the statement we use the fact that if `[SL(2,ℤ) : Γ] = n`, then `n!` is a period of `f`: +in general, if `[G : H] = n` then the `n!`th power of every element of `G` is in `H`. -/ +@[eval_problem] +theorem unbounded_denominators (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] + (k : ℤ) (f : SlashInvariantForm Γ k) (mdiff : MDiff f) (mero : ∀ c, IsMeromorphicAt c f k) + (int : ∀ n, IsIntegral ℤ (UpperHalfPlane.qExpansion Γ.index.factorial f n)) : + ∃ N, ∀ γ ∈ CongruenceSubgroup.Gamma N, SlashAction.map k γ ⇑f = f := by + sorry + +end LeanEval.ComplexAnalysis diff --git a/manifests/problems/unbounded_denominator.toml b/manifests/problems/unbounded_denominator.toml new file mode 100644 index 00000000..613f4686 --- /dev/null +++ b/manifests/problems/unbounded_denominator.toml @@ -0,0 +1,15 @@ +id = "unbounded_denominators" +title = "Unbounded denominators conjecture" +group = "formalization-evaluation" +status = "active" +visible = true +statement_revision = 1 +tags = [] +module = "LeanEval.ComplexAnalysis.UnboundedDenominators" +holes = ["unbounded_denominators"] +submitter = "Junyan Xu" + +[[status_history]] +status = "active" +effective_date = "2026-09-24" +reason = "policy" \ No newline at end of file From c2627ec5ccb61a2cfea10fe4c2225d9910964eca Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 25 Sep 2026 04:37:14 +0800 Subject: [PATCH 2/3] rename toml --- .../{unbounded_denominator.toml => unbounded_denominators.toml} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename manifests/problems/{unbounded_denominator.toml => unbounded_denominators.toml} (100%) diff --git a/manifests/problems/unbounded_denominator.toml b/manifests/problems/unbounded_denominators.toml similarity index 100% rename from manifests/problems/unbounded_denominator.toml rename to manifests/problems/unbounded_denominators.toml From 79b7111474317ab327cf1d066651ef914aca78cb Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 25 Sep 2026 17:50:07 +0800 Subject: [PATCH 3/3] add missing bounded at infinity condition --- LeanEval/ComplexAnalysis/UnboundedDenominators.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanEval/ComplexAnalysis/UnboundedDenominators.lean b/LeanEval/ComplexAnalysis/UnboundedDenominators.lean index be5f6dbc..c23d70e5 100644 --- a/LeanEval/ComplexAnalysis/UnboundedDenominators.lean +++ b/LeanEval/ComplexAnalysis/UnboundedDenominators.lean @@ -37,7 +37,8 @@ def IsMeromorphicAt (c : OnePoint ℝ) (f : UpperHalfPlane → ℂ) (k : ℤ) : in general, if `[G : H] = n` then the `n!`th power of every element of `G` is in `H`. -/ @[eval_problem] theorem unbounded_denominators (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] - (k : ℤ) (f : SlashInvariantForm Γ k) (mdiff : MDiff f) (mero : ∀ c, IsMeromorphicAt c f k) + (k : ℤ) (f : SlashInvariantForm Γ k) (mdiff : MDiff f) + (bdd : UpperHalfPlane.IsBoundedAtImInfty f) (mero : ∀ c, IsMeromorphicAt c f k) (int : ∀ n, IsIntegral ℤ (UpperHalfPlane.qExpansion Γ.index.factorial f n)) : ∃ N, ∀ γ ∈ CongruenceSubgroup.Gamma N, SlashAction.map k γ ⇑f = f := by sorry