Irrationality of the Euler--Mascheroni constant $\gamma$

Open

FCP.Transcendence.irrational_eulerMascheroni

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

analysisnumber-theory

Is $\gamma$ irrational? The Euler--Mascheroni constant $\gamma = \lim_{n\to\infty}\left(\sum_{k\le n} 1/k - \log n\right) \approx 0.5772$ is not known to be irrational; the statement is recorded here in the affirmative. Known partial results are of the form 'at least one of $\gamma$ and a companion constant is transcendental' (Rivoal, 2012).

Preamble

import Mathlib

Formal statement

namespace FCP.Transcendence

theorem irrational_eulerMascheroni : Irrational Real.eulerMascheroniConstant := 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/Euler%27s_constant

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 denoted by Mathlib's Euler--Mascheroni constant — the limit of $\sum_{k=1}^{n} 1/k - \log n$ — is irrational, i.e. it is not the image of any rational number in $\mathbb{R}$ .

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 the Euler--Mascheroni constant γ\gammaγ

Irrationality of the Euler--Mascheroni constant $\gamma$