Erdős problem 1193

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

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.