A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913979535720448 |
|---|---|
| author | Liu, Junqi Zhang, Jujian Zhi, Lihong |
| author_facet | Liu, Junqi Zhang, Jujian Zhi, Lihong |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_07625 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4 Liu, Junqi Zhang, Jujian Zhi, Lihong Number Theory 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. |
| title | A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4 |
| topic | Number Theory |
| url | https://arxiv.org/abs/2503.07625 |