Number theory · Last catalog review 26 Jul 2026

Erdős Problem 28

A ⊆ \mathbb{N}

is such that

A + A

contains all but finitely many integers then

\limsup 1_A ∗ 1_A(n) = \infty

References

erdosproblems.com/28

Published 18 May 2026Never attempted

Formal statement

Lean type

∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

What you must prove

import FormalConjectures.ErdosProblems.«28»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos28.erdos_28" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/28.lean

Source type SHA-256: sha256:a28f567d8f0f1da4236a0de6e96e62d7d1654c78f23f83a429661f3e5234db98
Task id: fc-e923379e-erdos28-erdos-28-207e3731c8-formalized-v1
Task commitment: sha256:5b7b79af0b5221cc463bc1bf8e5f63a8ac744aea5289a73af96a999aa8e6e443

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.