Open questions on irrationality of numbers

Reference: Wikipedia

theorem Irrational.algebraicIndependent_e_pi : AlgebraicIndependent ℚ ![Real.exp 1, Real.pi] ↔ sorry

Are $e$ and $\pi$ algebraically independent?

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

Is $e + \pi$ irrational?

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

Is $e \pi$ irrational?

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

Is $e ^ e$ irrational?

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

Is $\pi ^ e$ irrational?

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

Is $\pi ^ \pi$ irrational?

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

Is $\ln(\pi)$ irrational?

theorem Irrational.irrational_eulerMascheroniConstant : Irrational Real.eulerMascheroniConstant ↔ sorry

Is the Euler-Mascheroni constant $\gamma$ irrational?

theorem Irrational.irrational_catalanConstant : Irrational catalanConstant ↔ sorry

Is the Catalan constant $$G = \sum_{n=0}^∞ (-1)^n / (2n + 1)^2 \approx 0.91596$$ irrational?