Open questions on transcendence of numbers

Reference: Wikipedia

theorem Transcendental.exp_add_pi_transcendental : Transcendental ℚ (Real.exp 1 + Real.pi)

$e + \pi$ is transcendental.

theorem Transcendental.exp_mul_pi_transcendental : Transcendental ℚ (Real.exp 1 * Real.pi)

$e\pi$ is transcendental.

theorem Transcendental.exp_pow_pi_sq_transcendental : Transcendental ℚ (Real.exp (Real.pi ^ 2))

$e^{\pi^2}$ is transcendental.

theorem Transcendental.exp_exp_transcendental : Transcendental ℚ (Real.exp (Real.exp 1))

$e^e$ is transcendental.

theorem Transcendental.pi_pow_exp_transcendental : Transcendental ℚ (Real.pi ^ Real.exp 1)

$\pi^e$ is transcendental.

theorem Transcendental.pi_pow_sqrt_two_transcendental : Transcendental ℚ (Real.pi ^ √2)

$\pi^{\sqrt{2}}$ is transcendental.

theorem Transcendental.pi_pow_pi_transcendental : Transcendental ℚ (Real.pi ^ Real.pi)

$\pi^{\pi}$ is transcendental.

theorem Transcendental.pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (Real.pi ^ Real.pi ^ Real.pi)

$\pi^{\pi^{\pi}}$ is transcendental.

theorem Transcendental.pi_pow_pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (Real.pi ^ Real.pi ^ Real.pi ^ Real.pi)

$\pi^{\pi^{\pi^\pi}}$ is transcendental.

theorem Transcendental.pi_pow_pi_pow_pi_pow_pi_not_integer : ¬∃ (n : ℤ), Real.pi ^ Real.pi ^ Real.pi ^ Real.pi = ↑n

$\pi^{\pi^{\pi^\pi}}$ is not an integer.

This would follow from $\pi^{\pi^{\pi^\pi}}$ being transcendental, but this formulation is of interest in its own right, as it could in principle be proven by direct computation.

Reference: YouTube

theorem Transcendental.rlog_pi_transcendental : Transcendental ℚ (Real.log Real.pi)

$\log(\pi)$ is transcendental.

theorem Transcendental.rlog_rlog_two_transcendental : Transcendental ℚ (Real.log (Real.log 2))

$\log(\log(2))$ is transcendental.

theorem Transcendental.sin_exp_transcendental : Transcendental ℚ (Real.sin (Real.exp 1))

$\sin(e)$ is transcendental.

theorem Transcendental.exp_add_pi_or_exp_add_mul_transcendental : Transcendental ℚ (Real.pi + Real.exp 1) ∨ Transcendental ℚ (Real.pi * Real.exp 1)

At least one of $\pi + e$ and $\pi e$ is transcendental.

theorem Transcendental.transcendental_catalanConstant_or_gompertzConstant : Transcendental ℚ catalanConstant ∨ Transcendental ℚ gompertzConstant

At least one of Catalan constant and the Gompertz constant is transcendental.

theorem Transcendental.transcendental_catalanConstant : Transcendental ℚ catalanConstant

The Catalan constant $G$ is transcendental.

theorem Transcendental.transcendental_gompertzConstant : Transcendental ℚ gompertzConstant

The Gompertz constant $\delta$ is transcendental.

theorem Transcendental.transcendental_gamma_one_div_two : Transcendental ℚ (Real.Gamma (1 / 2))

$\Gamma(1/2)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem Transcendental.transcendental_gamma_one_div_three : Transcendental ℚ (Real.Gamma (1 / 3))

$\Gamma(1/3)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem Transcendental.transcendental_gamma_one_div_four : Transcendental ℚ (Real.Gamma (1 / 4))

$\Gamma(1/4)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem Transcendental.transcendental_gamma_one_div_six : Transcendental ℚ (Real.Gamma (1 / 6))

$\Gamma(1/6)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem Transcendental.transcendental_gamma_one_div (n : ℕ) (hn : 2 ≤ n) : Transcendental ℚ (Real.Gamma (1 / ↑n))

$\Gamma(1/n)$ for n ≥ 2 is transcendental.