Skip to content

Erdős problem 1193

Start work

Let A⊂NA\subset \mathbb{N} and let g(n)g(n) be a non-decreasing function of nn which is always >0>0.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1193.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1193.leanErdos1193.erdos_1193.parts.i3 linesExact file
False ↔  ∀ (A : Set ℕ) (g : ℕ → ℕ),    Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1193
  • PLBY Lean proofsErdosProblems.Erdos1193

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry