There exists $N₀$ such that for all $N ≥ N₀$, if $A ⊆ \{1, \dots, N\}$ satisfies that $ab + 1$
is never squarefree for all $a, b ∈ A$, then $|A| ≤ |\{n ≤ N : n ≡ 7 \pmod{25}\}|$.
More precisely, Sawhney proves: there exist absolute constants $η > 0$ and $N₀$
such that for all $N ≥ N₀$, if $|A| ≥ (1/25 - η)N$ then $A ⊆ \{n : n ≡ 7 \pmod{25}\}$ or
$A ⊆ \{n : n ≡ 18 \pmod{25}\}$.
A complete formal Lean 4 proof is available at:
https://github.com/The-Obstacle-Is-The-Way/erdos-banger
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
