Euler's constant measures the gap between the harmonic numbers and the logarithm:
It appears wherever the harmonic series is compared against an integral, and it is the value at of the digamma function, , equivalently . Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
For and the arithmetic questions were settled long ago: both are irrational and transcendental. For , neither is known. It is not known whether is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.
The goal theorem of this mission is transcendence,
with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.
Progress has come in three forms, and the milestones below formalize each.
Conditional bounds on a putative denominator. If were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing to places by an algorithm built on modified Bessel functions, showed any denominator exceeds ; a continued-fraction analysis by Papanikolaou (1997) pushed this past . These are not steps toward a proof so much as a measurement of how far brute computation can go.
Disjunctive results. The strongest unconditional statements pair with the Euler–Gompertz constant
Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of and is irrational. Rivoal later strengthened this to at least one of them is transcendental. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.
Irrationality criteria. Sondow, adapting Beukers' treatment of Apéry's theorem for , gave criteria equivalent to the irrationality of in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of , together with the identifications and and the numeric bounds . Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.
namespace EulerMascheroni theorem gamma_transcendental : Transcendental ℚ Real.eulerMascheroniConstant := by sorry end EulerMascheroni
Euler's constant
is transcendental: it is not a root of any non-zero polynomial with rational coefficients.
This is the goal of the mission and is open. It is expected to be true — no classical constant of this kind is believed to be algebraic — but nothing close to a proof is known, and even the far weaker assertion that is irrational is open. The transcendence methods that settled (Hermite, 1873) and (Lindemann, 1882) do not apply, because is not known to be a period or a value of the exponential at an algebraic point.
Formalization note. Transcendental ℚ x is Mathlib's predicate that x is not algebraic over , and Real.eulerMascheroniConstant is Mathlib's definition of as the limit of .