Prime number theorem with Ford's error term

Open

LandauFunction.ford_prime_counting_error

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptoticsprime-number-theorem

There is a constant $c>0$ such that, as $x\to\infty$ ,

\pi(x)-\mathrm{Li}(x)=O\!\left(x\exp\!\left(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5}\right)\right),

where $\pi(x)$ is the number of primes $p\le x$ and $\mathrm{Li}(x)=\int_2^x dt/\ln t$ .

This is the error term in the prime number theorem that the source feeds into the asymptotic formula for $\ln g(n)$ in terms of $\mathrm{Li}^{-1}$ .

Formalization Note $\pi(x)$ for real $x$ is Nat.primeCounting ⌊x⌋₊; the real powers are Real.rpow.

Preamble

import Mathlib
import Definitions.Def_LandauFunction_logIntegral

Formal statement

namespace LandauFunction
theorem ford_prime_counting_error :
    ∃ c : ℝ, 0 < c ∧
      (fun x : ℝ => (Nat.primeCounting ⌊x⌋₊ : ℝ) - logIntegral x) =O[Filter.atTop]
        (fun x : ℝ => x * Real.exp (-c * Real.log x ^ ((3 : ℝ) / 5) *
          Real.log (Real.log x) ^ (-(1 : ℝ) / 5))) := by sorry
end LandauFunction

Source

K. Ford, Proc. London Math. Soc. 85 (2002) 565–633; as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), paragraph "If π(x) − Li(x) = O(R(x)) … we may take R(x) = x exp(−c (ln x)^{3/5} (ln ln x)^{−1/5}) for some constant c > 0 by Ford", ref. [4].

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source material and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. It was produced at the explicit request of the proposal owner.

There exists a real number $c>0$ such that, as the real variable $x\to+\infty$ ,

\pi(\lfloor x\rfloor)-\mathrm{Li}(x)=O\!\left(x\,\exp\!\left(-c\,(\ln x)^{3/5}\,(\ln\ln x)^{-1/5}\right)\right).

Here $\lfloor x\rfloor$ is the natural-number floor (equal to $0$ for $x<0$ ), $\pi(m)$ is the number of primes $\le m$ , and $\mathrm{Li}(x)=\int_2^x dt/\ln t$ (definition logIntegral; for $x\ge 2$ the ordinary offset logarithmic integral). The powers $a^{3/5}$ and $a^{-1/5}$ are real powers; they are only evaluated at $a=\ln x$ and $a=\ln\ln x$ , which are positive for $x>e$ , so the library's conventions for non-positive bases do not affect this eventual statement. " $O$ " means: there are constants $C$ and $X$ with $|\pi(\lfloor x\rfloor)-\mathrm{Li}(x)|\le C\,|x\exp(\dots)|$ for all $x\ge X$ . No other hypotheses.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph