Erdős problem 1193 · problems.science

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

Sources

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

4 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

1193.lean

Retained formal statement3 of 4

Indeed if $A=\mathbb{N}$ (assuming $0\in\mathbb{N}$ ) then $1_A\ast 1_A(n)=n+1$ for all $n$ .

FormalConjectures/ErdosProblems/1193.leanErdos1193.erdos_1193.variants.sumRep_univ1 lineExact file

1∀ (n : ℕ), AdditiveCombinatorics.sumRep Set.univ n = n + 1

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.