Optimal bounds for an Erd\H{o}s problem on matching integers to distinct multiples

TL;DR

This paper determines the exact value of a function related to Erdős's problem on matching integers to multiples, using an AI-assisted proof workflow involving ChatGPT and formal verification in Lean.

Contribution

It provides the exact formula for the function f(m), solving a longstanding Erdős problem with a novel AI-assisted proof approach.

Findings

The function f(m) equals min(m, ⌈2√m⌉) for all m.

The proof strategy was initially proposed by ChatGPT.

The detailed proof was rigorously verified in Lean.

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\H{o}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\H{o}s problems".]