A positive second-order lower bound for prime counting

Proved

OddGoldbach19.primeCounting_second_order

by Yuxuan Xu · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprime-counting

For each natural number n with natural logarithm at least100, the number of primes at most n is at least n/log(n)+0.46*n/log(n)^2. The coefficient0.46 and logarithmic threshold100 are explicit constants derived from the existing Rosser–Schoenfeld theta estimate and partial summation. This is a prime-counting estimate, not a complete prime-sum campaign endpoint.

Preamble

import Mathlib

Formal statement

theorem OddGoldbach19.primeCounting_second_order (n : ℕ) (hl : 100 ≤ Real.log (n : ℝ)) :
    (n : ℝ) / Real.log n + 0.46 * n / (Real.log n) ^ 2 ≤ (Nat.primeCounting n : ℝ) := by sorry

Source

Derived from Rosser–Schoenfeld (1962) Theorem4 eq(3.14), proved platform theorem TaoFivePrimes.rosser_schoenfeld_theta_lower_analytic https://prove2.me/theorems/d4cf496a-eed1-4284-8d5d-f9cfbfb07786 ; Mathlib Chebyshev.primeCounting_eq_theta_div_log_add_integral. Constants0.46 and100 derived here, not quoted from the source.

View graph