Conjectures.io

Number theory

Erdős 28

If A⊆NA ⊆ \mathbb{N} is such that A+AA + A contains all but finitely many integers then lim sup⁡1A∗1A(n)=∞\limsup 1_A ∗ 1_A(n) = \infty.

References

No one has attempted this yet.

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-379fc029-erdos28-erdos-28-77dad45f08-formalized-v1
Task commitment
sha256:470998ec104abd6d7d2bb7e7695f50af1954b7e7924cfab98e7eb7533eac51d6

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.