Showing 1–11 of 11 results for author: Dahmen, S R

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

Explicitly bounding perfect powers in elliptic divisibility sequences

Authors: Sander R. Dahmen, Joey M. van Langen

Abstract: In this paper we consider elliptic divisibility sequences generated by a point on an elliptic curve over $\mathbb{Q}$ with $j$-invariant $1728$ given by an integral short Weierstrass equation. For several different such elliptic divisibility sequences, we determine explicitly a finite set of primes such that for all primes $l$ outside this set, the elliptic divisibility sequence contains no $l$-th… ▽ More In this paper we consider elliptic divisibility sequences generated by a point on an elliptic curve over $\mathbb{Q}$ with $j$-invariant $1728$ given by an integral short Weierstrass equation. For several different such elliptic divisibility sequences, we determine explicitly a finite set of primes such that for all primes $l$ outside this set, the elliptic divisibility sequence contains no $l$-th powers. Our approach uses, amongst other ingredients, the modular method for $\mathbb{Q}$-curves. The corresponding explicit computations fit into a general computational framework for $\mathbb{Q}$-curves, for which they provide illustrative examples. △ Less

Submitted 19 October, 2023; originally announced October 2023.

Comments: 23 pages

MSC Class: 11D41; 11F11; 11F80; 11G18

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

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

Formalizing the Solution to the Cap Set Problem

Authors: Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis

Abstract: In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the \emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the \emph{Annals of Mathematics} and is noteworthy for it… ▽ More In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the \emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the \emph{Annals of Mathematics} and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in $\mathbb{F}^n_q$ and concrete values for the case $q = 3$. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants. △ Less

Submitted 2 July, 2019; originally announced July 2019.

Comments: To appear in proceedings of Interactive Theorem Proving (ITP) 2019

Shifted powers in binary recurrence sequences

Authors: Michael A. Bennett, Sander R. Dahmen, Maurice Mignotte, Samir Siksek

Abstract: Let $u_k$ be a Lucas sequence. A standard technique for determining the perfect powers in the sequence $u_k$ combines bounds coming from linear forms in logarithms with local information obtained via Frey curves and modularity. The key to this approach is the fact that the equation $u_k=x^n$ can be translated into a ternary equation of the form $a y^2=b x^{2n}+c$ (with $a$, $b$,… ▽ More Let $u_k$ be a Lucas sequence. A standard technique for determining the perfect powers in the sequence $u_k$ combines bounds coming from linear forms in logarithms with local information obtained via Frey curves and modularity. The key to this approach is the fact that the equation $u_k=x^n$ can be translated into a ternary equation of the form $a y^2=b x^{2n}+c$ (with $a$, $b$, $c \in \mathbb{Z}$) for which Frey curves are available. In this paper we consider shifted powers in Lucas sequences, and consequently equations of the form $u_k=x^n+c$ which do not typically correspond to ternary equations with rational unknowns. However, they do, under certain hypotheses, lead to ternary equations with unknowns in totally real fields, allowing us to employ Frey curves over those fields instead of Frey curves defined over $\mathbb{Q}$. We illustrate this approach by showing that the quaternary Diophantine equation $x^{2n} \pm 6 x^n+1=8 y^2$ has no solutions in positive integers $x$, $y$, $n$ with $x$, $n>1$. △ Less

Submitted 7 August, 2014; originally announced August 2014.

Comments: 24 pages

MSC Class: 11D61 (Primary); 11D41 (Secondary); 11F80; 11F41

Journal ref: Math. Proc. Camb. Phil. Soc. 158 (2015) 305-329

Perfect powers expressible as sums of two fifth or seventh powers

Authors: Sander R. Dahmen, Samir Siksek

Abstract: We show that the generalized Fermat equations with signatures (5,5,7), (5,5,19), and (7,7,5) (and unit coefficients) have no non-trivial primitive integer solutions. Assuming GRH, we also prove the nonexistence of non-trivial primitive integer solutions for the signatures (5,5,11), (5,5,13), and (7,7,11). The main ingredients for obtaining our results are descent techniques, the method of Chabauty… ▽ More We show that the generalized Fermat equations with signatures (5,5,7), (5,5,19), and (7,7,5) (and unit coefficients) have no non-trivial primitive integer solutions. Assuming GRH, we also prove the nonexistence of non-trivial primitive integer solutions for the signatures (5,5,11), (5,5,13), and (7,7,11). The main ingredients for obtaining our results are descent techniques, the method of Chabauty-Coleman, and the modular approach to Diophantine equations. △ Less

Submitted 26 January, 2014; v1 submitted 16 September, 2013; originally announced September 2013.

Comments: The current version incorporates minor comments of the referee

MSC Class: 11D41

Level lowering modulo prime powers and twisted Fermat equations

Authors: Sander R. Dahmen, Soroosh Yazdani

Abstract: We discuss a clean level lowering theorem modulo prime powers for weight $2$ cusp forms. Furthermore, we illustrate how this can be used to completely solve certain twisted Fermat equations $ax^n+by^n+cz^n=0$. We discuss a clean level lowering theorem modulo prime powers for weight $2$ cusp forms. Furthermore, we illustrate how this can be used to completely solve certain twisted Fermat equations $ax^n+by^n+cz^n=0$. △ Less

Submitted 1 September, 2010; originally announced September 2010.

MSC Class: Primary 11D41; 11F33; Secondary 11F11; 11F80; 11G05

Journal ref: Can. J. Math.-J. Can. Math. 64 (2012) 282-300

A refined modular approach to the Diophantine equation $x^2+y^{2n}=z^3$

Authors: Sander R. Dahmen

Abstract: Let $n$ be a positive integer and consider the Diophantine equation of generalized Fermat type $x^2+y^{2n}=z^3$ in nonzero coprime integer unknowns $x,y,z$. Using methods of modular forms and Galois representations for approaching Diophantine equations, we show that for $n \in \{5, 31\}$ there are no solutions to this equation. Combining this with previously known results, this allows a complete… ▽ More Let $n$ be a positive integer and consider the Diophantine equation of generalized Fermat type $x^2+y^{2n}=z^3$ in nonzero coprime integer unknowns $x,y,z$. Using methods of modular forms and Galois representations for approaching Diophantine equations, we show that for $n \in \{5, 31\}$ there are no solutions to this equation. Combining this with previously known results, this allows a complete description of all solutions to the Diophantine equation above for $n \leq 10^7$. Finally, we show that there are also no solutions for $n\equiv -1 \pmod{6}$. △ Less

Submitted 29 January, 2010; originally announced February 2010.

Comments: 12 pages

MSC Class: 11D41; 11F11; 11F80; 11G05

Visualizing elements of Sha[3] in genus 2 jacobians

Authors: Nils Bruin, Sander R. Dahmen

Abstract: Mazur proved that any element xi of order three in the Shafarevich-Tate group of an elliptic curve E over a number field k can be made visible in an abelian surface A in the sense that xi lies in the kernel of the natural homomorphism between the cohomology groups H^1(k,E) -> H^1(k,A). However, the abelian surface in Mazur's construction is almost never a jacobian of a genus 2 curve. In this pap… ▽ More Mazur proved that any element xi of order three in the Shafarevich-Tate group of an elliptic curve E over a number field k can be made visible in an abelian surface A in the sense that xi lies in the kernel of the natural homomorphism between the cohomology groups H^1(k,E) -> H^1(k,A). However, the abelian surface in Mazur's construction is almost never a jacobian of a genus 2 curve. In this paper we show that any element of order three in the Shafarevich-Tate group of an elliptic curve over a number field can be visualized in the jacobians of a genus 2 curve. Moreover, we describe how to get explicit models of the genus 2 curves involved. △ Less

Submitted 28 January, 2010; originally announced January 2010.

Comments: 12 pages

MSC Class: 11G30; 14H40

Journal ref: Algorithmic Number Theory Lecture Notes in Computer Science, 2010, Volume 6197/2010, 110-125

On the residue class distribution of the number of prime divisors of an integer

Authors: Michael Coons, Sander R. Dahmen

Abstract: The {\em Liouville function} is defined by $\gl(n):=(-1)^{Ω(n)}$ where $Ω(n)$ is the number of prime divisors of $n$ counting multiplicity. Let $\z_m:=e^{2πi/m}$ be a primitive $m$--th root of unity. As a generalization of Liouville's function, we study the functions $\gl_{m,k}(n):=\z_m^{kΩ(n)}$. Using properties of these functions, we give a weak equidistribution result for $Ω(n)$ among residue… ▽ More The {\em Liouville function} is defined by $\gl(n):=(-1)^{Ω(n)}$ where $Ω(n)$ is the number of prime divisors of $n$ counting multiplicity. Let $\z_m:=e^{2πi/m}$ be a primitive $m$--th root of unity. As a generalization of Liouville's function, we study the functions $\gl_{m,k}(n):=\z_m^{kΩ(n)}$. Using properties of these functions, we give a weak equidistribution result for $Ω(n)$ among residue classes. More formally, we show that for any positive integer $m$, there exists an $A>0$ such that for all $j=0,1,...,m-1,$ we have $$#\{n\leq x:Ω(n)\equiv j (\bmod m)\}=\frac{x}{m}+O(\frac{x}{\log^A x}).$$ Best possible error terms are also discussed. In particular, we show that for $m>2$ the error term is not $o(x^\ga)$ for any $\ga<1$. △ Less

Submitted 4 June, 2009; originally announced June 2009.

Comments: 7 pages

MSC Class: 11N37; 11N60