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

1,217 Problems · 2 with reviewed evidence

23/26

Number	Question	Source says	Formal	Result here
#1057	Is it true that $C(x)=x^{1-o(1)}$ ?Source says openFormalized	open	In Lean	No Result decision
#1058	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1059	Are there infinitely many primes $p$ such that $p - k!$ is composite for each $k$ such that $1 ≤ k! < p$ ?Source says openFormalized	open	In Lean	No Result decision
#1060	The conjecture is about the function $f(n)$ which counts the number of solutions to $k\sigma(k)=n$ , where $\sigma(k)$ is the sum of divisors of $k$ . The first bound is that $f(n)$ grows slower than any power of $n^(\frac{1}{\log\log n})$ . The second bound is that $f(n)$ is at most a power of $\log n$ .Source says openFormalized	open	In Lean	No Result decision
#1061	How many (ordered) solutions are there to `σ(a) + σ(b) = σ(a + b)` with `a + b ≤ x`? Is it true that this number is asymptotic to `c * x` for some constant `c > 0`?Source says openFormalized	open	In Lean	No Result decision
#1062	Erdős asked whether the limiting density `f n / n` exists and, if so, whether it is irrational.Source says openFormalized	open	In Lean	No Result decision
#1063	Estimate $n_k$ by finding a better upper bound.Source says openFormalized	open	In Lean	No Result decision
#1064	Let $ϕ(n)$ be the Euler's totient function, then the $n$ satisfies $ϕ(n)>ϕ(n - ϕ(n))$ have asymptotic density 1. Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rdős concerning the arithmetical functions { $\phi$ } and { $\sigma$ }. Colloq. Math.Source says provedFormalized	proved	In Lean	No Result decision
#1065	Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$ ?Source says openFormalized	open	In Lean	No Result decision
#1066	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1067	Does every graph with chromatic number $\aleph_1$ contain an infinitely connected subgraph with chromatic number $\aleph_1$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1068	Does every graph with chromatic number $\aleph_1$ contain a countable subgraph which is infinitely connected?Source says openFormalized	open	In Lean	No Result decision
#1069	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1070	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1071	Can a finite set of disjoint unit segments in a unit square be maximal? Solved affirmatively by [Da85], who gave an explicit construction.Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1072	Is it true that there are infinitely many $p$ for which $f(p) = p − 1$ ?Source says openFormalized	open	In Lean	No Result decision
#1073	Is it true that $A(x) \le x^{o(1)}$ ?Source says openFormalized	open	In Lean	No Result decision
#1074	Let $S$ be the set of all $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$ . Does $\lim\frac{\|S\cap[1, x]\|}{x}$ exist?Source says openFormalized	open	In Lean	No Result decision
#1075	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1076	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1077	We call a graph $D$ -balanced (or $D$ -almost-regular) if the maximum degree is at most $D$ times the minimum degree.Source says disprovedFormalized	disproved	In Lean	No Result decision
#1078	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1079	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1080	Let $G$ be a bipartite graph on $n$ vertices such that one part has $\lfloor n^{2/3}\rfloor$ vertices. Is there a constant $c>0$ such that if $G$ has at least $cn$ edges then $G$ must contain a $C_6$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1081	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#1082	Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Does $A$ determine at least $\lfloor n/2\rfloor$ distinct distances?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#1083	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1084	It is easy to check that $f_2(n) < 3n$ .Source says openFormalized	open	In Lean	No Result decision
#1085	Erdős showed $f_2(n) > n^{1+c/\log\log n}$ for some $c > 0$ .Source says openFormalized	open	In Lean	No Result decision
#1086	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1087	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1088	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1089	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1090	Let $k\geq 3$ . Does there exist a finite set $A\subset \mathbb{R}^2$ such that, in any $2$ -colouring of $A$ , there exists a line which contains at least $k$ points from $A$ , and all the points of $A$ on the line have the same colour?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1091	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1092	Is it true that $f_2(n) \gg n$ ? Disproved by Rödl, who showed $f_r(n) = o(n)$ for all fixed $r \geq 2$ . A conjecture of Erdős, Hajnal, and Szemerédi.Source says disprovedFormalized	disproved	In Lean	No Result decision
#1093	Are there infinitely many binomial coefficients with deficiency 1?Source says openFormalized	open	In Lean	No Result decision
#1094	For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$ , with only finitely many exceptions.Source says openFormalized	open	In Lean	No Result decision
#1095	Sorenson, Sorenson, and Webster [SSWE20] give heuristic evidence that $\log g(k) \asymp \frac{k}{\log k}$ .Source says openFormalized	open	In Lean	No Result decision
#1096	Let $1<q<1+\epsilon$ and consider the set of numbers of the shape $\sum_{i\in S}q^i$ (for all finite $S$ ), ordered by size as $0=x_1<x_2<\cdots$ .Source says provedFormalized	proved	In Lean	No Result decision
#1097	The main conjecture: for any finite set of integers $A$ with $\|A\| = n$ , the number of distinct common differences in three-term arithmetic progressions is $O(n^{3/2})$ .Source says openFormalized	open	In Lean	No Result decision
#1098	Let $G$ be a group and $\Gamma=\Gamma(G)$ be the non-commuting graph, with vertices the elements of $G$ and an edge between $g$ and $h$ if and only if $g$ and $h$ do not commute, $gh\neq hg$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1099	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1100	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1101	1. There is NO good sequence with polynomial growth.Source says openFormalized	open	In Lean	No Result decision
#1102	If `A = {a₁ < a₂ < …}` has property P, then `A` has natural density `0`. Equivalently, `(a_j / j) → ∞` as `j → ∞`. -Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1103	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1104	Lower bound (Hefty–Horn–King–Pfender 2025). There exists a constant $c_1 \in (0,1]$ such that, for sufficiently large $n$ , $c_1 \sqrt{\frac{n}{\log n}} \le f(n),$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as `triangleFreeMaxChromatic n`.Source says openFormalized	open	In Lean	No Result decision