Erdős Problems

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

Add a contribution Collection details

Full distribution

Collection coverage

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

Open per source608
Resolved per source556
Other source status53

Exact formal statement available604 / 1,217

With Repository-reviewed evidence2 / 1,217

9 Problems

Number	Question	Source says	Formal	Result here
#229	Let $(S_n)_{n \ge 1}$ be a sequence of sets of complex numbers, none of which have a finite limit point. Does there exist an entire transcendental function $f(z)$ such that, for all $n \ge 1$ , there exists some $k_n \ge 0$ such that $f^{(k_n)}(z) = 0$ for all $z \in S_n$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#408	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#409	How many iterations of $n\mapsto\phi(n) + 1$ are needed before a prime is reached?Source says openFormalized	open	In Lean	No Result decision
#410	Let $σ_1(n) = σ(n)$ , the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$ .Source says openFormalized	open	In Lean	No Result decision
#411	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#412	Let $σ_1(n)=σ(n)$ , the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$ . Is it true that, for every $m, n ≥ 2$ , there exist some $i, j$ such that $σ_i(m) = σ_j(n)$ ?Source says openFormalized	open	In Lean	No Result decision
#413	Are there infinitely many barriers for `ω`?Source says openFormalized	open	In Lean	No Result decision
#414	Let $h_1(n) = h(n)$ and $h_k(n) = h(h_{k-1}(n))$ . Is it true, for any $m,n$ , there exist $i$ and $j$ such that $h_i(m) = h_j(n)$ ?Source says openFormalized	open	In Lean	No Result decision
#906	Does there exists an entire non-zero transcendental function `f : ℂ → ℂ` such that for any sequence `n₀ < n₁ < ...`, `{ z \| ∃ k, iteratedDeriv (n k) f z = 0 }` is dense.Source says openFormalized	open	In Lean	No Result decision