Exponentials conjectures and theorems

Reference: Wikipedia

theorem Exponentials.four_exponentials_conjecture (x y : Fin 2 → ℂ) (h1 : LinearIndependent ℚ x) (h2 : LinearIndependent ℚ y) : ∃ (i : Fin 2) (j : Fin 2), Transcendental ℚ (Complex.exp (x i * y j))

Four exponentials conjecture Let $x_0, x_1$ and $y_0, y_1$ be $\mathbb Q$-linearly independent pairs of complex numbers, then some $e^{x_i y_j}$ is transcendental.

theorem Exponentials.two_pow_three_pow_transcendental (t : ℝ) (h : Irrational t) : Transcendental ℚ (2 ^ t) ∨ Transcendental ℚ (3 ^ t)

The four exponential conjecture would imply that for any irrational number $t$, at least one of the numbers $2^t$ and $3^t$ is transcendental.