Let be the number of pairs with and . Erdős Problem #824 asks whether . By an argument of Pollack and Pomerance, this follows if for every fixed there are primes with free of prime factors exceeding . 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 , applies to after a change of sign in two of its sections. Consequently , conditionally on the correctness of that preprint, which has not been refereed and whose main new estimates we have not independently verified.

生成讲解博客的中文版本

生成AI智能校验的中文版本