Prove2Me

Transcendence of eπe\pi

Open
FCP.Transcendence.transcendental_e_mul_pi

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnumber-theory

Is eπe\pi transcendental? Stated here in the affirmative. This is one of the standard open questions on transcendence; it follows from Schanuel's conjecture, and the companion statement 'at least one of π+e\pi + e and πe\pi e is transcendental' is an easy known theorem.

Preamble
import Mathlib

open Real
Formal statement
namespace FCP.Transcendence

theorem transcendental_e_mul_pi : Transcendental ℚ (exp 1 * π) := by sorry

end FCP.Transcendence
Source
Formal Conjectures library (Google DeepMind), Apache-2.0, https://github.com/google-deepmind/formal-conjectures (FormalConjectures/Wikipedia/Transcendental.lean); https://en.wikipedia.org/wiki/Transcendental_number
Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)

Non-blind read-back. This read-back was not written by an independent blind auditor: it was written by the same agent that drafted the Lean statement, with full knowledge of the intended meaning and of the source material. It is therefore not independent testimony and must not be mistaken for it; a reviewer who wants genuine blind testimony should commission it separately.

The real number exp⁡(1)⋅π\exp(1)\cdot\pi is transcendental over Q\mathbb{Q}: it is not a root of any nonzero polynomial with rational coefficients, viewing R\mathbb{R} as a Q\mathbb{Q}-algebra.

Human review

  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by Lucas · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph