Papers With

← All papers
First page of A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4

A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4

Junqi Liu, Jujian Zhang, Lihong Zhi

math.NT Feb 28, 2025 · v1
formalization mathlib number-theory
Read PDF arXiv abstract Code
TL;DR
Formalizes the irrationality of zeta(3) in Lean 4 via Beukers' method, extending Mathlib with new analytic number theory.
Abstract
We formalize a proof of the irrationality of $ζ(3)$ in Lean 4, using Beukers' method. To support this, we extend the Lean mathematical library (Mathlib) by formalizing shifted Legendre polynomials and important results in analytic number theory that were previously missing. As part of the Lean 4 PrimeNumberTheoremAnd project, we also formalize the asymptotic behavior of the prime counting function, giving the first formal proof in Lean 4 of a version of the Prime Number Theorem with an error term which is stronger than what had previously been formalized. This result is a crucial ingredient in proving the irrationality of $ζ(3)$. Our complete Lean 4 formalization is publicly available on GitHub.
Problem

The irrationality of zeta(3), proved by Apery in 1978, is a landmark result in number theory that had never been formally verified in Lean 4. Key prerequisites such as shifted Legendre polynomials and strong forms of the Prime Number Theorem were also missing from Mathlib.

Approach

The authors formalize a proof of the irrationality of zeta(3) in Lean 4 using Beukers' method. They extend Mathlib by formalizing shifted Legendre polynomials and their properties, and as part of the PrimeNumberTheoremAnd project, they formalize the asymptotic behavior of the prime counting function with an error term stronger than previously formalized versions. This Prime Number Theorem result serves as a crucial ingredient in the irrationality proof.

Results

The work delivers the first complete formalization of the irrationality of zeta(3) in Lean 4, along with the first formal proof in Lean 4 of a version of the Prime Number Theorem with an error term stronger than what had previously been formalized.