{"id":"palomar/PALOMAR-2026-09-05-000006","url":"https://github.com/n-yamaguchi-0729/KroneckerWeber/tree/c3de19b9368d3ba1a28804efe1c21d1302db8f54","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-05-000006-v1.json","repo":"https://github.com/n-yamaguchi-0729/KroneckerWeber","tags":["math.NT","msc:11R37","class-field-theory","lean-formalization","number-theory"],"score":0,"title":"The global Kronecker–Weber theorem in Lean 4","trust":"high","domain":"math.NT","source":"palomar","authors":["Naganori Yamaguchi"],"reviews":0,"subject":"math.NT","summary":"This project formalizes the global Kronecker–Weber theorem in Lean 4: every finite abelian extension of the rational numbers embeds into a cyclotomic field. For a number field L that is abelian Galois over the rationals, the selected declaration gives a positive integer n and a rational algebra embedding from L into CyclotomicField n ℚ. The proof is supplied by the ClassFieldTheory library at a fixed commit, using Lean 4.33.0 and Mathlib.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-05","reactions":{},"formalized":true,"formalizes":[{"title":"Algebraic Number Theory","identifier":"https://doi.org/10.1007/978-3-662-03983-0","relationship":"formalizes"}]}