Erdős Problem 152

#TODO: Formalize the corresponding conjecture for infinite Sidon sets.

References:

• erdosproblems.com/152
• [DM26a] DeepMind prover agent, formal proof of Erdős problem 152 (2026)
• [DM26b] DeepMind prover agent, formal proof of the quadratic variant of Erdős problem 152 (2026)
• [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.

noncomputable def Erdos152.f (n : ℕ) : ℕ

Define f n to be the minimum of |{s | s - 1 ∉ A + A, s ∈ A + A, s + 1 ∉ A + A}| as A ranges over all Sidon sets of size n.

Equations

• Erdos152.f n = ⨅ (A : ↑{A : Set ℕ | A.ncard = n ∧ IsSidon A}), {s : ℕ | s - 1 ∉ ↑A + ↑A ∧ s ∈ ↑A + ↑A ∧ s + 1 ∉ ↑A + ↑A}.ncard

theorem Erdos152.erdos_152 : True ↔ Filter.Tendsto f Filter.atTop Filter.atTop

Must lim f n = ∞?

This was proved formally by the DeepMind prover agent [DM26a].

theorem Erdos152.erdos_152.variants.square : True ↔ (fun (n : ℕ) => ↑n ^ 2) =O[Filter.atTop] fun (n : ℕ) => ↑(f n)

Must f n ≫ n ^ 2?

This stronger quadratic variant was also proved formally by the DeepMind prover agent [DM26b].