Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certifying rings of integers in number fields

Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen

TL;DR

This work presents a Lean 4 formalization for certifying rings of integers in number fields, constructing a verification pipeline in which external SageMath certificates are checked by Lean to certify integral bases and discriminants. It develops compute-friendly representations and certificates for irreducibility (Rabin tests, degree analysis, LPFW certificates), builds a subalgebra framework with a times-table to perform arithmetic in rings of integers, and applies local maximality criteria (Dedekind criterion; Pohst–Zassenhaus) to deduce global maximality. The contributions include formalizing resultants and discriminants, implementing certificate structures for monogenic and non-monogenic cases, and successfully verifying LMFDB entries up to degree 8, thus bridging computational algebra with formal verification. The results demonstrate the feasibility of verified computation in algebraic number theory and lay groundwork for extending certification to broader invariants and higher degrees, with a path toward tighter CAS–proof assistant integration.

Abstract

Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the $\textit{Number fields}$ section of the $\textit{L-functions and modular forms database}$ (LMFDB). These concern, for several number fields, the explicitly given $\textit{integral basis}$ of the ring of integers and the $\textit{discriminant}$. To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.

Certifying rings of integers in number fields

TL;DR

This work presents a Lean 4 formalization for certifying rings of integers in number fields, constructing a verification pipeline in which external SageMath certificates are checked by Lean to certify integral bases and discriminants. It develops compute-friendly representations and certificates for irreducibility (Rabin tests, degree analysis, LPFW certificates), builds a subalgebra framework with a times-table to perform arithmetic in rings of integers, and applies local maximality criteria (Dedekind criterion; Pohst–Zassenhaus) to deduce global maximality. The contributions include formalizing resultants and discriminants, implementing certificate structures for monogenic and non-monogenic cases, and successfully verifying LMFDB entries up to degree 8, thus bridging computational algebra with formal verification. The results demonstrate the feasibility of verified computation in algebraic number theory and lay groundwork for extending certification to broader invariants and higher degrees, with a path toward tighter CAS–proof assistant integration.

Abstract

Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the section of the (LMFDB). These concern, for several number fields, the explicitly given of the ring of integers and the . To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.
Paper Structure (26 sections, 10 theorems, 14 equations)

This paper contains 26 sections, 10 theorems, 14 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Forms of Computation in Lean
  4. Irreducibility
  5. Polynomials as Lists
  6. Over Finite Fields
  7. Certificate
  8. Degree Analysis
  9. LPFW Certificate
  10. Verifying Rings of Integers
  11. Construction of the Subalgebra
  12. Arithmetic in $\mathcal{O}\xspace$
  13. Local Maximality
  14. The Pohst--Zassenhaus Theorem
  15. Dedekind Criterion
  16. ...and 11 more sections

Key Result

theorem 1

Let $f$ be a polynomial over $\mathbf{F}_q$ of degree $n > 0$. Then $f$ is irreducible if and only if:

Theorems & Definitions (11)

  • theorem 1: Rabin's test
  • proposition 1
  • proposition 2
  • proposition 3
  • proposition 4
  • theorem 2
  • definition 1
  • proposition 5
  • proposition 6
  • proposition 7
  • ...and 1 more