{"id":"palomar/PALOMAR-2026-10-22-000033","url":"https://github.com/F-Najman/normalizer-lean/tree/d943984531cfa220bae8c6c7f504b300514b0bfa","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000033-v1.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:20H05","msc:20E28","msc:22E40","msc:68V20","modular-forms","fuchsian-groups","group-theory"],"score":0,"title":"Helling's theorem: the maximal subgroups of SL₂(ℝ) commensurable with SL₂(ℤ)","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, of Helling's theorem and of consequences for normalizers. A subgroup G ≤ SL₂(ℝ) is commensurable with SL₂(ℤ) if G ∩ SL₂(ℤ) has finite index in G and in SL₂(ℤ); Γ₀(N)⁺ is the group generated by the Atkin–Lehner elements of level N, and contains Γ₀(N). Every G commensurable with SL₂(ℤ) is conjugate into Γ₀(N)⁺ for some squarefree N, by (det A)^{−1/2}·A for an integral matrix A with det A > 0. For every N ≥ 1, Γ₀(N)⁺ is commensurable with SL₂(ℤ), and for squarefree N it is maximal among such groups; so the maximal subgroups of SL₂(ℝ)…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Bestimmung der Kommensurabilitätsklasse der Hilbertschen Modulgruppe","identifier":"doi:10.1007/BF01112194","relationship":"formalizes"},{"title":"Arithmetic groups and the affine E₈ Dynkin diagram","identifier":"arXiv:0810.1465v2","relationship":"formalizes"}]}