Zeta(5) has been proven irrational (also Lean-verified)

This reaches 1/3 milestones deemed a "breakthrough" by Epoch AI: https://epoch.ai/frontiermath/open-problems/apery-irrational...

The remaining two "breakthrough" milestones are (i) a proof or refutation of the Poincaré conjecture in 4 dimensions (ii) an improvement to the best-known classical prime factorisation algorithms.