Big news on irrational numbers! Aabir Fauzan from Aalto University released a preprint on Zenodo before it hit the arXiv, and a formalisation has been posted by Moritz Firsching. Since the statement is so elementary, the repo is set up to be checked by the stringent anti goal-hacking framework Comparator, and moreover the machinery used is the PNT+ project run by @tao@mathstodon.xyz and Alex Kantorovic, which is high-quality hand-rolled analytic number theory in Lean, I'm fairly confident this is sound. https://github.com/mo271/zeta5 also has the link to the preprint.