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.

翻译：数域及其整数环作为有理数与整数的推广，是数论中的基础对象。目前存在多个关注其计算方面的计算机代数系统与数据库。特别地，计算给定数域的整数环是计算代数数论的主要任务之一。本文描述了在Lean 4中实现此类计算认证的形式化工作。为实现这一目标，我们开发了若干适用于计算的数据类型。此外，许多其他基础数学概念与结果也必须被形式化，其中大部分本身也具有独立的研究价值。这些内容包括结式与判别式，以及证明有限域和有理数域上单变量多项式不可约性的方法。为说明我们策略的可行性，我们形式化验证了《L-函数与模形式数据库》（LMFDB）中《数域》章节的部分条目。这些条目涉及多个数域中明确给出的整数环《整基》及其《判别式》。为此，我们编写了SageMath代码来计算相应的证明证书，并输出待验证命题的Lean证明。