Erdős problem 848 · problems.science

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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

848.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/848.leanErdos848.erdos_848.variants.asymptotic1 lineExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science