An Average-Order Theorem for a Shifted Pairwise-Coprime Extremal Problem

Abstract

For $n\ge 2$, let $M(n)$ be the supremum of ${\sum }_{a\in A}1/(n-a)$ over pairwise coprime sets $A\subset [1,n)$. Erdős asked whether $M(n)\le {\sum }_{p<n}1/p+O(1)$ uniformly in $n$. We prove the quantitative average-order formula ${\sum }_{n\le N}M(n)=e^{-\gamma }N\log \log N+O(N)$. The proof combines the self-rough lower construction $\{n-d:P^{-}(n-d)>d\}$ with a bounded-cost dual certificate and Buchstab--de Bruijn estimates. We also show $M(n)=(e^{-\gamma }+o(1))\log \log n$ for almost all $n$, with a quantitative exceptional-set bound, so Erdős's inequality holds for almost all $n$. The argument combines a long-interval two-dimensional beta sieve for two moving forbidden residue classes with an exact finite singular-series cancellation. The remaining obstacles to a full variance estimate are a shifted-prime second moment for $d>\sqrt{2N}$ and finite-$u$ rough correlations in the intermediate tail, yielding a precise conditional criterion. For every $\epsilon >0$ we also prove the uniform pointwise bound $M(n)\le (2+\epsilon )\log \log n+O_{\epsilon }(1)$ and explain the linear-sieve barrier at the constant $2$. The results of this paper have been formally verified in Lean.

36 pages, no figures. v2 adds an accompanying Lean 4 formalisation, a formalisation section and repository link, and expanded acknowledgements; exposition revised