Optimal bounds for an Erdős problem on matching integers to distinct multiples
Wouter van Doorn, Yanyang Li, Quanyu Tang
math.CO
Mar 30, 2026 · v1
TL;DR
The argument resolving an Erdős divisibility problem was made fully rigorous and formally verified in Lean by the Aristotle system.
Abstract
Let $f(m)$ be the largest integer such that for every set $A = \{a_1 < \cdots < a_m\}$ of $m$ positive integers and every open interval $I$ of length $2a_m$, there exist at least $f(m)$ disjoint pairs $(a, b)$ with $a \in A$ dividing $b \in I$. Solving a problem of Erdős, we determine $f(m)$ exactly, and show $$ f(m)=\min\bigl(m,\lceil 2\sqrt{m}\,\rceil\bigr) $$ for all $m$. The proof was obtained through an AI-assisted workflow: the proof strategy was first proposed by ChatGPT, and the detailed argument was subsequently made fully rigorous and formally verified in Lean by Aristotle. The exposition and final proofs presented here are entirely human-written. [This paper solves Problem #650 on Bloom's website "Erdős problems".]
Problem
Erdos posed the problem of determining f(m), the largest integer such that for every set A of m positive integers and every open interval I of length 2*a_m, there exist at least f(m) disjoint pairs (a, b) with a in A dividing b in I. The exact value was unknown.
Approach
The proof strategy was first proposed by ChatGPT, then made fully rigorous and formally verified in Lean by Aristotle (Harmonic's automated theorem proving tool). The argument establishes both an upper bound via a two-parameter construction showing f(st) <= s+t, and a lower bound via matching arguments. During formalization, a gap in ChatGPT's original proof was discovered and repaired.
Results
The exact value f(m) = min(m, ceil(2*sqrt(m))) is determined for all m, solving Erdos Problem #650. All results are formally verified in Lean 4.
