Zudilin: one of is irrational
ProvedFCP.Zeta.zudilin_five_seven_nine_elevenZudilin's theorem (2001). At least one of , , , is irrational. The proof refines the Ball--Rivoal hypergeometric construction; the theorem is the sharpest known localisation of irrationality among small odd zeta values, and it does not identify which value is irrational.
import Mathlib
namespace FCP.Zeta
theorem zudilin_five_seven_nine_eleven :
({5, 7, 9, 11} ∩ {a : ℕ | ∃ x : ℝ, Irrational x ∧ riemannZeta a = x}).Nonempty := by sorry
end FCP.ZetaRead-back
What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)
Non-blind read-back. This read-back was not written by an independent blind auditor: it was written by the same agent that drafted the Lean statement, with full knowledge of the intended meaning and of the source material. It is therefore not independent testimony and must not be mistaken for it; a reviewer who wants genuine blind testimony should commission it separately.
Consider the set of natural numbers and the set of natural numbers for which there exists an irrational real with . The claim is that the intersection of these two sets is nonempty: some has real and irrational.
No claim is made about which works, and the statement would also be satisfied if several of them were irrational.
Confirmed by the mission captain (proposal self-audit).