Coprime pairs with equal sum of divisors, assuming smooth shifted primes

Source abstract

Let $h(x)$ be the number of pairs $1\le a 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.