Erdős Problems

1,217 source-owned questions · 604 with a formal statement · searchable by statement, number, topic and source status.

Full distribution

Collection coverage

Source status, exact formal material, and reviewed Results are separate signals.

Exact formal statement available604 / 1,217

With Repository-reviewed evidence2 / 1,217

102 Problems

3/3

Number	Question	Source says	Formal	Result here
#1192	Does there exist, for all $r\geq 2$ , a basis $A$ of order $r$ (so that $f_r(n)>0$ for all large $n$ ) such that $\sum_{n\leq x}f_r(n)^2 \ll x$ for all $x$ ?Source says openFormalized	open	In Lean	No Result decision
#1193	Let $A\subset \mathbb{N}$ and let $g(n)$ be a non-decreasing function of $n$ which is always $>0$ .Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1194	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1198	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#1199	Is it true that in any 2-colouring of $\mathbb{N}$ there exists an infinite set $A$ such that all elements of $A+A$ are the same colour?Source says openFormalized	open	In Lean	No Result decision
#1213	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision