Coprime pairs with equal sum of divisors, assuming smooth shifted primes
Shisheng Li, Zhong Zhuang
math.NT
Oct 11, 2026 · v1
TL;DR
Formalizes in Lean 4 with Mathlib the conditional implication from smooth shifted primes to h(x)>x^{2-ε} for Erdős Problem #824, sorry-free.
Abstract
Let $h(x)$ be the number of pairs $1\le a<b<x$ with $\gcd(a,b)=1$ and $σ(a)=σ(b)$. Erdős Problem #824 asks whether $h(x)>x^{2-o(1)}$. By an argument of Pollack and Pomerance, this follows if for every fixed $δ>0$ there are $y^{1-o(1)}$ primes $p\le5y$ with $p+1$ free of prime factors exceeding $y^δ$. We write this implication out with explicit parameters and formalize it in Lean 4. We then check that the argument of the recent OpenAI preprint "Weighted dilation graphs, smooth shifted primes and totient fibers", which claims the corresponding statement for $p-1$, applies to $p+1$ after a change of sign in two of its sections. Consequently $h(x)=x^{2-o(1)}$, conditionally on the correctness of that preprint, which has not been refereed and whose main new estimates we have not independently verified.
Problem
Erdős Problem #824 asks whether the number h(x) of coprime pairs a<b<x with σ(a)=σ(b) exceeds x^{2-o(1)}. A Pollack–Pomerance argument reduces this to the existence of many primes p with p+1 smooth.
Approach
The reduction is written out with explicit parameters under a weak hypothesis (y^{1-o(1)} smooth shifted primes) and formalized in Lean 4 with Mathlib. The formalization was produced by ChatGPT and adapted by Codex. The authors then check that the argument of an unrefereed OpenAI preprint on smooth p-1 carries over to p+1 after sign changes in two sections.
Results
The Lean theorem proving the lower bound of h from the hypothesis has no sorry and uses only the standard axioms. Conditionally on the preprint's correctness, h(x)=x^{2-o(1)}. The squarefree addendum and the preprint's main estimates are not formally verified.
