{"id":"arxiv/2604.23211","url":"https://arxiv.org/abs/2604.23211","tags":["math.CO","cs.LO","math.AG"],"score":0,"title":"Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4","domain":"math.CO","source":"arxiv","authors":["Yihe Huang","Sizhe Cui","Jiaqi Wang","Jujian Zhang"],"reviews":0,"subject":"math.CO","summary":"Combinatorial curve neighborhoods are somewhat foundational when setting up the quantum Schubert calculus for affine flag manifolds. In the specific case of type $A_1^{(1)}$, you can encode these neighborhoods entirely within the moment graph of the infinite dihedral group $D_\\infty$. Building on the framework developed by Mihalcea and Norton, this paper presents a complete, axiom-free formalization of these combinatorial curve neighborhoods in Lean 4. Rather than just wrapping mathematical statements, we formalized $D_\\infty$ directly as a Coxeter system to explicitly compute length…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-25","reactions":{}}