Formal target: Corpus.WikipediaRiemannZetaValues.irrational_five

$\zeta(5)$ is irrational.

Exact formal statement

Exists.{1} fun x => And (Irrational x) (Eq.{1} (riemannZeta 5) (Complex.ofReal x))

This target is a formal statement, not a proof of the problem.

Environment availability: available.