Searcharxiv⌕ Search

arXiv subjects

Sander R. Dahmen

Publications and source records attributed to Sander R. Dahmen.

13 recordsLinked to original sources
arXiv2026

Formally certifying number field invariants

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.

cs.LO↗
arXiv2025

On the generalized Fermat equation $x^{13} + y^{13} = z^n$

Let $n \in \mathbb{Z}_{\geq 2}$. We study the generalized Fermat equation \[x^{13}+y^{13}=z^n, \quad x,y,z \in \mathbb{Z}, \quad \gcd(x,y,z)=1.\] Using a combination of techniques, including the modular method, classical descent, unit sieves, and Chabauty and Mordell--Weil sieve methods over number fields, we show that for $n=5$ all its solutions $(a,b,c)$ are trivial, i.e. satisfy $abc=0$. Under the assumption of GRH, we also show that for $n=7$ there are only trivial solutions. Furthermore, we provide partial results towards solving the equation for general $n \in \mathbb{Z}_{\geq 2}$, in particular that any solution $(a,b,c)$ with $13\mid c$ is trivial.

math.NT↗
arXiv2025

Certifying rings of integers in number fields

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.

cs.LO↗
arXiv2023

Explicitly bounding perfect powers in elliptic divisibility sequences

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.

math.NT↗
arXiv2022

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

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.

cs.LO↗
arXiv2022

A formalization of Dedekind domains and class groups of global fields

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.

cs.LO↗
arXiv2019

Formalizing the Solution to the Cap Set Problem

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.

cs.LO↗
arXiv2014

Shifted powers in binary recurrence sequences

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$.

math.NT↗
arXiv2014

Perfect powers expressible as sums of two fifth or seventh powers

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.

math.NT↗
arXiv2010

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

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}$.

math.NT↗
arXiv2010

Visualizing elements of Sha[3] in genus 2 jacobians

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.

math.NT↗
arXiv2009

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

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$.

math.NT↗