e_plus_pi_irrational
Provedalgebranumbertheoryopen-problemopenproblemtranscendencetheory
e + π and e·π cannot both be rational: At least one of e+π, e·π is irrational (since if both were rational, then e and π would be roots of a quadratic with rational coefficients, contradicting their transcendence). Whether either is irrational individually is unknown. It's known both can't be algebraic.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem e_plus_pi_irrational :
Irrational (Real.exp 1 + Real.pi) ∨ Irrational (Real.exp 1 * Real.pi) := by
sorrySource