{"id":"palomar/PALOMAR-2026-10-18-000013","url":"https://github.com/F-Najman/normalizer-lean/tree/e7ca694d9e349326e03e5acfa4e41ed823e4e2dc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000013-v2.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:14G35","msc:14H37","msc:11G18","msc:68V20","cartan-modular-curves","modular-automorphisms","lean"],"score":0,"title":"Modular automorphisms of Cartan modular curves of prime level","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 defining the split and non-split Cartan modular curves and their normalizer curves: for any level N, every element of the normalizer of a group containing Γ(N) is a rational matrix of a restricted form; X_sp(N) ≅ X₀(N²); X_sp(p) (p ≥ 5) and X_ns(p) (p odd) have exactly 2 modular automorphisms; X_sp⁺(p) (p ≥ 7) and X_ns⁺(p) (p ≥ 5) have none, and both bounds on p are sharp. 17 theorems, no sorry, only the axioms propext, Classical.choice and Quot.sound.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Automorphisms of Cartan modular curves of prime and composite level","identifier":"arXiv:2005.09009v2","relationship":"formalizes"},{"title":"Automorphisms of general modular curves","identifier":"arXiv:2610.08998v1","relationship":"formalizes"}]}