Email Gateway (Aug 22 2022 at 21:11): Email Gateway (Aug 22 2022 at 21:11):From: Tobias Nipkow <nipkow@in.tum.de>
The Irrationality of ζ(3)
Manuel Eberl
This article provides a formalisation of Beukers's straightforward analytic
proof that ζ(3) is irrational. This was first proven by Apéry (which is why this
result is also often called ‘Apéry's Theorem’) using a more algebraic approach.
This formalisation follows Filaseta's presentation of Beukers's proof.
https://www.isa-afp.org/entries/Zeta_3_Irrational.html
Enjoy!
PS Only 1800 lines - This is a great example of the power of the Prime Number
Theorem!
smime.p7s
Email Gateway (Aug 22 2022 at 21:11):From: Manuel Eberl <eberlm@in.tum.de>
It is certainly convenient to have strong results like the PNT available
and not having to work around it every time, but many applications
(including this one) do not need its full strength. It would have been
enough to show something like lcm{1..n} ∈ O(3.2^n), whereas the PNT
gives you lcm{1..n} ∈(c^n) for any c > e. Proving such a suitable result
in an elementary way would probably not be /that/ much work (maybe an
additional 1000 lines).
Not that I would advocate for doing that. We have these advanced
results, so we ought to make use of them. It was certainly refreshing to
formalise a result without having to search through troves of related
papers for more elementary routes to the same result first and coming up
with hacks and tricks to get around using results and concepts that are
not available in our system yet.
Manuel
Last updated: Apr 19 2024 at 04:17 UTC