Erdős Problem 848

Is the maximum size of a set $A \subseteq \{1, \dots, N\}$ such that $ab + 1$ is never squarefree (for all $a, b \in A$) achieved by taking those $n \equiv 7 \pmod{25}$?

References:

• erdosproblems.com/848
• [Er92b] Erdős, P. "Some of my favourite problems in number theory, combinatorics, and geometry." Resenhas do Instituto de Matemático e Estatística da Universidade de São Paulo 2.2 (1995): 165-186.
• [Sa25] Sawhney, M. "Problem 848." (2025) https://www.math.columbia.edu/~msawhney/Problem_848.pdf
• Full formal proof of asymptotic result: https://github.com/The-Obstacle-Is-The-Way/erdos-banger

def Erdos848.NonSquarefreeProductProp (A : Finset ℕ) : Prop

A set $A$ has the non-squarefree product property if $ab + 1$ is not squarefree for all $a, b ∈ A$.

Equations

• Erdos848.NonSquarefreeProductProp A = ∀ a ∈ A, ∀ b ∈ A, ¬Squarefree (a * b + 1)

def Erdos848.A₇ (N : ℕ) : Finset ℕ

The candidate extremal set: $\{n ∈ \{0, \dots, N-1\} : n ≡ 7 (mod 25)\}$.

Equations

• Erdos848.A₇ N = {n ∈ Finset.range N | n % 25 = 7}

def Erdos848.Erdos848For (N : ℕ) : Prop

The Erdős Problem 848 statement for a fixed $N$: any set $A ⊆ \{0, \dots, N-1\}$ with the non-squarefree product property has cardinality at most $|A₇(N)|$.

Equations

• Erdos848.Erdos848For N = ∀ A ⊆ Finset.range N, Erdos848.NonSquarefreeProductProp A → A.card ≤ (Erdos848.A₇ N).card

theorem Erdos848.erdos_848 : True ↔ ∀ (N : ℕ), Erdos848For N

Is the maximum size of a set $A ⊆ \{1, \dots, N\}$ such that $ab + 1$ is never squarefree (for all $a, b ∈ A$) achieved by taking those $n ≡ 7 \pmod{25}$?

This asks whether Erdos848 N holds for all $N$ (formulated using A ⊆ Finset.range N).

This was solved for all sufficiently large $N$ by Sawhney in this note. In fact, Sawhney proves something slightly stronger, that there exists some constant $c>0$ such that if $\lvert A\rvert \geq (\frac{1}{25}-c)N$ and $N$ is large then $A$ is contained in either $\{ n\equiv 7\pmod{25}\}$ or $\{n\equiv 18\pmod{25}\}$.

theorem Erdos848.erdos_848_asymptotic : ∀ᶠ (N : ℕ) in Filter.atTop, Erdos848For N

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