Window counting bound implies Erdős 1210 (partial summation)

Proved

Erdos1210.erdos_1210_of_window_count_bound

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

erdos-problemsnumber-theoryprimes

Suppose there is a constant $K$ such that for all $n$ , all pairwise coprime $A\subseteq[1,n)$ and all $x\ge2$ ,

|A\cap[n-x,n)|\le\pi(x)+\frac{Kx}{(\log x)^2}.

Then the affirmative answer to Erdős Problem 1210 holds: there is $C$ with $\sum_{a\in A}\frac1{n-a}\le\sum_{p<n}\frac1p+C$ for all $n$ and all pairwise coprime $A\subseteq[1,n)$ .

This is the partial-summation step of the reduction discussed on the erdosproblems.com forum. The hypothesis itself is not known: as noted in that discussion, it would imply an inequality of the form $\pi(x+y)\le\pi(x)+\pi(y)+O(y/(\log y)^2)$ (compare Problem 855). The milestone isolates the implication, which is unconditional.

Formalization Note The window $[n-x,n)$ is encoded as $a\ge n-x$ with truncated subtraction, together with the standing hypothesis $a<n$ .

Preamble

import Mathlib
open Finset

Formal statement

namespace Erdos1210

theorem erdos_1210_of_window_count_bound
    (h : ∃ K : ℝ, ∀ n : ℕ, ∀ A : Finset ℕ,
      (∀ a ∈ A, 1 ≤ a ∧ a < n) →
      (∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) →
      ∀ x : ℕ, 2 ≤ x →
        ((A.filter (fun a => n - x ≤ a)).card : ℝ) ≤
          (Nat.primeCounting x : ℝ) + K * x / (Real.log x) ^ 2) :
    ∃ C : ℝ, ∀ n : ℕ, ∀ A : Finset ℕ,
      (∀ a ∈ A, 1 ≤ a ∧ a < n) →
      (∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) →
      ∑ a ∈ A, (1 / ((n : ℝ) - a)) ≤
        (∑ p ∈ (range n).filter Nat.Prime, (1 / (p : ℝ))) + C := by sorry

end Erdos1210

Source

erdosproblems.com forum thread for Problem 1210, https://www.erdosproblems.com/forum/thread/1210 , comment by T. Bloom (8 Apr 2026, relaying a suggested argument): the bound |A ∩ [n−x,n)| ≤ π(x) + O(x/(log x)^2) for all x implies the problem 'by partial summation'; follow-up by N. Sothanaphan (8 Apr 2026) on why the bound itself is not known.

Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, with full knowledge of the source and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; an independent blind read-back is still recommended before launch.

This is an implication. Hypothesis: there is a real constant $K$ (of any sign) such that for every natural number $n$ , every finite set $A$ of natural numbers with $1\le a<n$ for all $a\in A$ and with distinct elements pairwise coprime, and every natural number $x\ge 2$ ,

\#\{a\in A:\ a\ge n-x\}\;\le\;\pi(x)+\frac{K\,x}{(\log x)^2},

where $\pi(x)$ counts primes $\le x$ , $\log$ is the natural logarithm (positive since $x\ge2$ ), and $n-x$ is truncated natural subtraction (equal to $0$ when $x\ge n$ , in which case the left side is $|A|$ ).

Conclusion: there is a real constant $C$ such that for every natural $n$ and every finite $A$ with $1\le a<n$ for all $a\in A$ and distinct elements pairwise coprime,

\sum_{a\in A}\frac{1}{n-a}\;\le\;\sum_{\substack{p\ \text{prime}\\ p<n}}\frac1p+C,

with $n-a\ge1$ computed in the reals. The statement asserts nothing about whether the hypothesis is true; it only claims the hypothesis implies the conclusion. $K$ and $C$ are uniform in $n$ , $A$ (and $x$ ).

Human review

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

View graph