exists_irrational_of_five_seven_nine_eleven

Specification

At least one of $\zeta(5), \zeta(7), \zeta(9)$ or $\zeta(11)$ is irrational. [Zu01] W. Zudilin (2001). _One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational_. Russ. Math. Surv. 56 (4): 774–776.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem exists_irrational_of_five_seven_nine_eleven :
    {5, 7, 9, 11} ∩ { a | ∃ x, Irrational x ∧ riemannZeta a = x} |>.Nonempty

ID: Wikipedia__RiemannZetaValues__exists_irrational_of_five_seven_nine_eleven

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.