3 papers
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.AI2025
Aristotle: IMO-level Automated Theorem Proving
Tudor Achim, Alex Best, Alberto Bietti +20
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical O…
cs.FL2025
A complete formalization of Fermat's Last Theorem for regular primes in Lean
Alex Best, Christopher Birkbeck, Riccardo Brasca +3
We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstr…