{"id":"palomar/PALOMAR-2026-10-18-000010","url":"https://github.com/F-Najman/normalizer-lean/tree/17c911351938f13d620262a54de45c275db9de57","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000010-v2.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:20H05","msc:14G35","msc:14H37","msc:68V20","modular-curves","normalizers","lean"],"score":0,"title":"Normalizers of Γ_Δ(N), Γ(N) and ±Γ₁(N)","trust":"high","domain":"math.NT","source":"palomar","authors":["Filip Najman"],"reviews":0,"subject":"math.NT","summary":"Formal statements and proofs, in Lean 4 with Mathlib, about the normalizers in SL₂(ℝ) of the groups Γ_Δ(N) between Γ₁(N) and Γ₀(N), and the quotients Nor(Γ)/Γ, the modular automorphism groups of the curves X_Δ(N): a generalization of Newman's description of the normalizer to Γ_Δ(N); Nor(Γ(N)) = SL₂(ℤ), so the modular automorphism group of X(N) is SL₂(ℤ/N)/{±1}; and, for N ≠ 4, Nor(±Γ₁(N)) is generated by Γ₀(N) and the Atkin–Lehner elements, so X₁(N) has 2^ω(N) φ(N)/2 modular automorphisms for N ≥ 3 (N = 4 is an exception). 34 theorems, no sorry, only the axioms propext, Classical.choice and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"The normalizer of Γ₁(N) in PSL₂(ℝ)","identifier":"","relationship":"formalizes"},{"title":"Normalizer of Γ₁(m)","identifier":"","relationship":"formalizes"}]}