Formal target: Corpus.WikipediaTranscendental.exp_add_pi_transcendental
Is the real number e + π transcendental over the rational numbers? Here e = exp(1), and π is the usual circle constant. Transcendental means that no nonzero polynomial with rational coefficients has e + π as a root. This is stronger than asking whether e + π is irrational.
Exact formal statement
Transcendental.{0, 0} Rat (HAdd.hAdd.{0, 0, 0} (Real.exp 1) Real.pi)This target is a formal statement, not a proof of the problem.
Environment availability: available.