class group 1discriminant 1invariant certification 1lean theorem prover 1lmfdb verification 1number fields 1
From the 1 of 3 linked papers with an AI index.
3 papers
cs.LO2026
Formally certifying number field invariants
Alain Chavarri Villarello, Sander R. Dahmen
The paper presents a Lean 4 formalization that certifies key invariants of number fields—such as discriminant, signature, unit groups modulo p‑th powers, and class groups—and uses…
math.NT2025
On the generalized Fermat equation
Alex J. Best, Sander R. Dahmen, Nuno Freitas
Let . 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,…
cs.LO2025
Certifying rings of integers in number fields
Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen
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 sys…