PNT+ used to prove irrationality of zeta(3)

Stream: PrimeNumberTheorem+

[Terence Tao]

Not sure if this has been posted before, but I just saw this paper on the arXiv formalizing the irrationality of zeta(3) in Lean, using our proof of the prime number theorem as one of the ingredients!

[Alastair Irving]

Very nice result. I wonder though if it really needs the full proof of PNT. ON a very quick reading it looks like maybe a Chebyshev upper bound would be sufficient. Maybe the constant you would need would be so close to 1 that it's easier just to use PNT.

[Moritz Firsching]

For convenience here's the the link mentioned in that paper: https://github.com/ahhwuhu/zeta_3_irrational

[Kevin Buzzard]

IIRC there's a discussion on how much less than PNT you can get away with in the Coq paper formalising the same result

[Alex Kontorovich]

For the application to Apery, it's enough to show something like: For all x sufficiently large, $\pi(x)\le 1.3 x / \log x$. (Or maybe you need $1.03$; regardless, upper bounds like these are much simpler than an asymptotic formula...)

[Terence Tao]

It's relatively easy to establish Chebyshev's original bounds $(0.92129+o(1))x/\log x \leq \pi(x) \leq (1.1055+o(1))x/\log x$ with effective error terms, see e.g., Section 3 of https://scispace.com/pdf/elementary-methods-in-the-study-of-the-distribution-of-prime-1w89mv6dwv.pdf . If there is interest I can try to create a blueprint for this to formalize as part of the PNT. (But there is some conceptual overlap with https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Bertrand.html , athough the arguments there are not structured in a way that make it immediately easy to get to Chebyshev's bounds.)

[Junqi Liu]

Thank you all for your attention to our work. We believe this should be the first formalization of this result in Lean 4. The two theorems used in the paper from the PNT+ were completed by @Jujian Zhang , @Lihong Zhi and me and submitted as a PR to the PNT+ project. It's a great honor to make a small contribution to the PNT+ project. :smiley: