2 papers
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…
math.NT2025
New exponent pairs, zero density estimates, and zero additive energy estimates: a systematic approach
Terence Tao, Tim Trudgian, Andrew Yang
We obtain several new bounds on exponents of interest in analytic number theory, including four new exponent pairs, new zero density estimates for the Riemann zeta-function, and ne…