Irrationality of $e + \pi$

Open

FCP.Transcendence.irrational_e_add_pi

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

analysisnumber-theory

Is $e + \pi$ irrational? Stated here in the affirmative. Although $e$ and $\pi$ are both transcendental, nothing is known about $e + \pi$ : it is not even known to be irrational. What is known is that $e + \pi$ and $e\pi$ cannot both be algebraic, since $e$ and $\pi$ are the roots of $X^2 - (e+\pi)X + e\pi$ .

Preamble

import Mathlib

open Real

Formal statement

namespace FCP.Transcendence

theorem irrational_e_add_pi : Irrational (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/Irrational.lean); https://en.wikipedia.org/wiki/Irrational_number#Open_questions

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 obtained as the sum of $\exp(1)$ and $\pi$ is irrational, i.e. it does not lie in the image of the rationals in $\mathbb{R}$ . Here $\exp$ is the real exponential function, so $\exp(1) = e$ , and $\pi$ is the real circle constant.

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

Irrationality of e+πe + \pie+π

Irrationality of $e + \pi$