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

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)}$ ?openFormalized	open	In Lean	No Result decision
#1058	No statement retained — open to read what the source holdsprovedNo 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$ ?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$ .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`?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.openFormalized	open	In Lean	No Result decision
#1063	Estimate $n_k$ by finding a better upper bound.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.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$ ?openFormalized	open	In Lean	No Result decision
#1066	No statement retained — open to read what the source holdsopenNo 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$ ?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?openFormalized	open	In Lean	No Result decision
#1069	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#1070	No statement retained — open to read what the source holdsopenNo 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.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$ ?openFormalized	open	In Lean	No Result decision
#1073	Is it true that $A(x) \le x^{o(1)}$ ?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?openFormalized	open	In Lean	No Result decision
#1075	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1076	No statement retained — open to read what the source holdsprovedNo 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.disprovedFormalized	disproved	In Lean	No Result decision
#1078	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1079	No statement retained — open to read what the source holdssolvedNo 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$ ?disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1081	No statement retained — open to read what the source holdsdisprovedNo 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?falsifiableFormalized	falsifiable	In Lean	No Result decision
#1083	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1084	It is easy to check that $f_2(n) < 3n$ .openFormalized	open	In Lean	No Result decision
#1085	Erdős showed $f_2(n) > n^{1+c/\log\log n}$ for some $c > 0$ .openFormalized	open	In Lean	No Result decision
#1086	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1087	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1088	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1089	No statement retained — open to read what the source holdssolvedNo 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?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1091	No statement retained — open to read what the source holdssolvedNo 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.disprovedFormalized	disproved	In Lean	No Result decision
#1093	Are there infinitely many binomial coefficients with deficiency 1?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.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}$ .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$ .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})$ .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$ .proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1099	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1100	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1101	1. There is NO good sequence with polynomial growth.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 → ∞`. -solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1103	No statement retained — open to read what the source holdsopenNo 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`.openFormalized	open	In Lean	No Result decision

Problems

Search problems.science