Certifying rings of integers in number fields

TL;DR

This paper presents a formalization in Lean 4 for certifying computations of rings of integers in number fields, including the development of mathematical data types and verification of entries from the LMFDB database.

Contribution

It introduces a new formalization framework in Lean 4 for certifying algebraic number theory computations, including the formalization of key concepts and verification methods.

Findings

Successfully verified entries from the LMFDB database.

Developed formalized data types for algebraic number theory.

Demonstrated the feasibility of certified computations in number fields.

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.