Prove2Me

lcm⁡(1,…,m)≤e(1+δ)m\operatorname{lcm}(1,\dots,m)\le e^{(1+\delta)m} for all large mm

Proved
PiIrrationality.lcmUpto_le_exp

by moona3k · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprime-number-theorem

For every δ>0\delta>0 there is m0m_0 such that

lcm⁡(1,2,…,m) ≤ e(1+δ)m(m≥m0).\operatorname{lcm}(1,2,\dots,m)\ \le\ e^{(1+\delta)m}\qquad (m\ge m_0).

Since log⁡lcm⁡(1,…,m)=ψ(m)\log\operatorname{lcm}(1,\dots,m)=\psi(m), this is the upper half of the prime number theorem ψ(x)∼x\psi(x)\sim x. It is the standard estimate for the common denominators of linear forms built from rational functions with poles of bounded order.

Preamble
import Mathlib.NumberTheory.Chebyshev
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Order.Filter.AtTopBot.Basic
Formal statement
theorem PiIrrationality.lcmUpto_le_exp (δ : ℝ) (hδ : 0 < δ) :
    ∀ᶠ m : ℕ in Filter.atTop, (Nat.lcmUpto m : ℝ) ≤ Real.exp ((1 + δ) * (m : ℝ)) := by
  sorry
Source
Hardy–Wright, An Introduction to the Theory of Numbers, Thm. 6 and §22.2 (ψ(x) = log lcm(1..x), ψ(x) ~ x); used in D. Zeilberger and W. Zudilin, The irrationality measure of π is at most 7.103205334137…, Moscow J. Combin. Number Theory 9 (2020), no. 4, 407–419, arXiv:1912.06345, World record paragraph.

View graph