Open questions on irrationality of numbers

Reference: Wikipedia

theorem irrational_e_plus_pi : Irrational (Real.exp 1 + Real.pi)

$e + \pi$ is irrational

theorem irrational_e_times_pi : Irrational (Real.exp 1 * Real.pi)

$e \pi$ is irrational

theorem irrational_e_to_e : Irrational (Real.exp 1 ^ Real.exp 1)

$e ^ e$ is irrational

theorem irrational_pi_to_e : Irrational (Real.pi ^ Real.exp 1)

$\pi ^ e$ is irrational

theorem irrational_pi_to_pi : Irrational (Real.pi ^ Real.pi)

$\pi ^ \pi$ is irrational

theorem irrational_ln_pi : Irrational (Real.log Real.pi)

$\ln(\pi)$ is irrational

theorem irrational_euler_mascheroni : Irrational Real.eulerMascheroniConstant

The the difference between harmonic series and natural logarithm, also known as Euler-Mascheroni constant $\gamma$ is irrational

theorem irrational_catalan_constant : Irrational (∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) ^ 2)

The Catalan constant is irrational