AI 中文总结
本文提出Lean 4形式化方法，改进数域不变量验证技术，将其扩展到符号、单位群、类群等，验证LMFDB中数百个数域的相关条目，推动计算代数数论的形式化验证发展。
AI 中文摘要
数域是有理数的推广，是数论中的基础对象，其诸多关键算术性质由不变量刻画，计算这些不变量是计算代数数论的核心任务之一，也是多个计算机代数系统和数据库的研究重点。本文描述了一种用于验证多种数域不变量的Lean 4形式化方法。基于之前关于整数环验证的工作，我们将该验证方法扩展到更多不变量，包括符号、模p次幂的单位群，最终还有类群。我们还改进了判别式验证，使得之前工作中不可行的更高次数数域的验证成为可能。我们引入了基于代数对象表示的、适合计算的结构，包括用于验证理想算术的可复用结构。在此过程中，我们形式化了若干基础数学结果，例如关于实闭域和伪剩余序列的结果，这些结果具有独立的研究价值。我们将该框架应用于验证L-函数与模形式数据库（LMFDB）中数百个数域条目，涉及不同数域的判别式、符号、类数和类群结构。为此，我们编写了一个SageMath脚本，用于计算验证证书并输出对应命题的Lean证明。
英文摘要
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 powers, and, ultimately, the class group. We also improve discriminant certification, allowing verifications for higher-degree number fields infeasible in previous work. We introduce structures based on representations of algebraic objects suited to computation, including reusable ones for certifying ideal arithmetic. Along the way, we formalize several underlying mathematical results, for instance on real closed fields and pseudo-remainder sequences, which are of independent interest. We apply our framework to verify hundreds of entries of the $\textit{L-functions and modular forms database}$ (LMFDB) concerning the discriminant, signature, class number, and class group structure of various number fields. To this end, we wrote a SageMath script that computes the certificates and outputs Lean proofs of the corresponding statements.
Comments39 pages, 2 figures. Source code available at https://github.com/alainchmt/CertifyingInvariantsNF/tree/v1
