Showing 1–5 of 5 results for author: Baanen, A

Certifying rings of integers in number fields

Authors: Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen

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… ▽ More 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. △ Less

Submitted 16 January, 2025; v1 submitted 26 September, 2024; originally announced September 2024.

Comments: 14 pages. Source code available at https://github.com/alainchmt/RingOfIntegersProject

MSC Class: 68V20; 11Y40; 11R09; 11R04; 11R29 ACM Class: F.4.1

Journal ref: CPP 2025: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 50-66

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Authors: Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen

Abstract: Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form $y^2=x^3+d$, where $d$ is a (given) nonzero integer number and all solutions in integers $x$ and $y$ have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in… ▽ More Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form $y^2=x^3+d$, where $d$ is a (given) nonzero integer number and all solutions in integers $x$ and $y$ have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of $d<0$. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond. △ Less

Submitted 23 December, 2022; v1 submitted 30 September, 2022; originally announced September 2022.

Comments: 14 pages. Accepted for CPP '23. Source code available at https://github.com/lean-forward/class-group-and-mordell-equation

MSC Class: 68V20; 11D25; 11R11; 11R29 ACM Class: F.4.1

Use and abuse of instance parameters in the Lean mathematical library

Authors: Anne Baanen

Abstract: The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameter… ▽ More The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them. △ Less

Submitted 2 May, 2022; v1 submitted 3 February, 2022; originally announced February 2022.

Comments: To be published at Interactive Theorem Proving 2022 (Haifa, Israel). Unabridged, interactive versions of the listings are available at https://github.com/lean-forward/mathlib-classes/

ACM Class: F.4.1

A formalization of Dedekind domains and class groups of global fields

Authors: Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio

Abstract: Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful i… ▽ More Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib's decentralized collaboration processes involved in this project. △ Less

Submitted 30 August, 2022; v1 submitted 4 February, 2021; originally announced February 2021.

Comments: Expanded version of https://drops.dagstuhl.de/opus/volltexte/2021/13900/ (appeared ar in the Leibniz International Proceedings in Informatics - Conference Interactive Theorem Proving 2021 (Rome, Italy)). To appear in the Journal of Automated Reasoning

MSC Class: 68V20; 68V15; 11R29

Combining predicate transformer semantics for effects: a case study in parsing regular languages

Authors: Anne Baanen, Wouter Swierstra

Abstract: This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a single effect, parsing requires a combination of effects: non-determinism, general recursion and mutable state. Reasoning about such combinations of effects is n… ▽ More This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a single effect, parsing requires a combination of effects: non-determinism, general recursion and mutable state. Reasoning about such combinations of effects is notoriously difficult, yet our approach using predicate transformers enables the careful separation of program syntax, correctness proofs and termination proofs. △ Less

Submitted 30 April, 2020; originally announced May 2020.

Comments: In Proceedings MSFP 2020, arXiv:2004.14735

ACM Class: F.3.1; F.3.2

Journal ref: EPTCS 317, 2020, pp. 39-56