Prove2Me

Lower bound for Euler-Mascheroni: 0.57721565 <= gamma

Proved
TaoFivePrimes.theta_cert_totient_gamma_lower

by andreaskapfer · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryeuler-mascheroninumber-theorytao-five-primes

The Euler-Mascheroni constant satisfies γ≥0.57721565\gamma \ge 0.57721565. The proof evaluates the Mathlib series γ=∑k≥1term(k,1)\gamma = \sum_{k\ge 1} \mathrm{term}(k,1) with N=200N = 200 terms, bounds log⁡201\log 201 from below by the rational r=5.30330491r = 5.30330491 via a truncated exponential certificate, and bounds the tail by the pointwise estimate term(n+1,1)≤18(6n+1)(6n+7)\mathrm{term}(n+1,1) \le \frac{18}{(6n+1)(6n+7)} for n≥200n \ge 200, which telescopes to 31207\frac{3}{1207}. Concretely it proves γ=H201−log⁡201−∑k≥0term(k+201,1)≥H201−r−31207>0.57721565\gamma = H_{201} - \log 201 - \sum_{k\ge 0}\mathrm{term}(k+201,1) \ge H_{201} - r - \frac{3}{1207} > 0.57721565.

Preamble
import Mathlib.NumberTheory.Harmonic.ZetaAsymp
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Mathlib.Topology.Algebra.InfiniteSum.Order
Formal statement
namespace TaoFivePrimes

theorem theta_cert_totient_gamma_lower :
    (57721565 / 10^8 : ℝ) ≤ Real.eulerMascheroniConstant := by sorry

end TaoFivePrimes
Source
G. H. Hardy, *Note on Dr. Vacca's series for γ\gamma*, Quart. J. Pure Appl. Math. 43 (1912), 215-216, as reworked in M. J. D. Powell / Mathlib's `ZetaAsymptotics` tail estimate; the series ∑k≥0ζ(k+1)−1\sum_{k\ge0} \zeta(k+1)^{-1}-type expansion of γ\gamma and the pointwise bound used here are standard, see also J. Havil, *Gamma: Exploring Euler's Constant*, Princeton Univ. Press, 2003.

View graph