Open questions on transcendence of numbers

The question

exp_add_pi_transcendental. $e+\pi$ is transcendental.

exp_mul_pi_transcendental. $e\pi$ is transcendental.

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

exp_exp_transcendental. $e^e$ is transcendental.

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

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

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

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

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

pi_pow_pi_pow_pi_pow_pi_not_integer. ${\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

rlog_pi_transcendental. $\log (\pi )$ is transcendental.

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

sin_exp_transcendental. $\sin (e)$ is transcendental.

transcendental_catalanConstant. The Catalan constant $G$ is transcendental.

transcendental_gompertzConstant. The Gompertz constant $\delta$ is transcendental.

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

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.Transcendental (16 statements).

theorem exp_add_pi_transcendental : Transcendental ℚ (exp 1 + π)

theorem exp_mul_pi_transcendental : Transcendental ℚ (exp 1 * π)

theorem exp_pow_pi_sq_transcendental : Transcendental ℚ (exp (π ^ 2))

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

theorem pi_pow_exp_transcendental : Transcendental ℚ (π ^ (exp 1))

theorem pi_pow_sqrt_two_transcendental : Transcendental ℚ (π ^ √2)

theorem pi_pow_pi_transcendental : Transcendental ℚ (π ^ π)

theorem pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (π ^ (π ^ π))

theorem pi_pow_pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (π ^ (π ^ (π ^ π)))

theorem pi_pow_pi_pow_pi_pow_pi_not_integer : ¬ ∃ (n : ℤ), π ^ π ^ π ^ π = n

theorem rlog_pi_transcendental : Transcendental ℚ (log π)

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

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

theorem transcendental_catalanConstant : Transcendental ℚ catalanConstant

theorem transcendental_gompertzConstant : Transcendental ℚ gompertzConstant

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

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Wikipedia

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.