Is the maximum size of a set $A\subseteq \{1,\ldots,N\}$ such that $ab+1$ is never squarefree (for all $a,b\in A$) achieved by taking those $n\equiv 7\pmod{25}$? Resolved for all sufficiently large $N$: any near-maximal $A$ is contained in $\{n\equiv 7\pmod{25}\}$ or $\{n\equiv 18\pmod{25}\}$, leaving only a finite check.

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