{"id":"arxiv/2607.26230","url":"https://arxiv.org/abs/2607.26230","tags":["cs.LO","math.NT"],"score":0,"title":"Formally certifying number field invariants","domain":"cs.LO","source":"arxiv","authors":["Alain Chavarri Villarello","Sander R. Dahmen"],"reviews":0,"subject":"cs.LO","summary":"Number fields, which generalize the rational numbers, are fundamental objects in number theory. Many of their key arithmetic properties are captured by invariants whose computation is among the central tasks of computational algebraic number theory and a focus of several computer algebra systems and databases. In this paper, we describe a Lean 4 formalization for certifying several of these number field invariants. Building on previous work on certifying rings of integers, we extend this certification approach to further invariants including the signature, the unit group modulo $p$-th…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-28","reactions":{}}