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

2/26

Number	Question	Source says	Formal	Result here
#49	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#50	Let $f$ be the asymptotic distribution function of $\varphi(n)/n$ , so that for each $c \in [0,1]$ , $f(c)$ is the natural density of $\{n : \varphi(n) < cn\}$ . Is it true that there is no $x$ such that the derivative $f'(x)$ exists and is positive?Source says openFormalized	open	In Lean	No Result decision
#51	Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$ , there is an integer n such that $\phi(n)=a$ , and yet if $n_a$ is the smallest such integer, then $\frac{n_a}{a} → \infty$ as $a → ∞$ ?Source says openFormalized	open	In Lean	No Result decision
#52	Let $A$ be a finite set of integers. Is it true that for every $\epsilon>0$ $\max( \lvert A+A\rvert,\lvert AA\rvert)\gg_\epsilon \lvert A\rvert^{2-\epsilon}?$ Source says openFormalized	open	In Lean	No Result decision
#53	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#54	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#55	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#56	Suppose $A \subseteq \{1,\dots,N\}$ is such that there are no $k+1$ elements of $A$ which are relatively prime. An example is the set of all multiples of the first $k$ primes. Is this the largest such set? To avoid trivial counterexamples, we must insist that $N$ be at least the $k$ th prime.Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#57	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#58	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#59	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#60	Does every graph on $n$ vertices with $>\mathrm{ex}(n;C_4)$ edges contain $\gg n^{1/2}$ many copies of $C_4$ ?Source says openFormalized	open	In Lean	No Result decision
#61	The Erdős–Hajnal Conjecture states that there is a constant $c(H) > 0$ for each $H$ such that we can take $f(n) = n^{c(H)}$ in the above formulation.Source says openFormalized	open	In Lean	No Result decision
#62	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#63	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#64	Does every finite graph with minimum degree at least $3$ contain a cycle of length $2^k$ for some $k \geq 2$ ?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#65	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#66	Is there and $A \subset \mathbb{N}$ is such that $\lim_{n\to \infty}\frac{1_A\ast 1_A(n)}{\log n}$ exists and is $\ne 0$ ?Source says openFormalized	open	In Lean	No Result decision
#67	The Erdős discrepancy problemSource says provedFormalized	proved	In Lean	No Result decision
#68	Is $\sum_{n=2}^\infty \frac{1}{n!-1}$ irrational?Source says openFormalized	open	In Lean	No Result decision
#69	Is $\sum_{n\geq 2}\frac{\omega(n)}{2^n}$ irrational? (Here $\omega(n)$ counts the number of distinct prime divisors of $n$ .)Source says provedFormalized	proved	In Lean	No Result decision
#70	Erdős Problem 70: Let $\mathfrak{c}$ be the cardinality of the continuum, let $\beta$ be a countable ordinal, and let $2 \le n < \omega$ . Is it true that $\mathfrak{c} \to (\beta, n)^3_2$ ?Source says openFormalized	open	In Lean	No Result decision
#71	Is it true that for every infinite arithmetic progression $P$ which contains even numbers there is some constant $c=c(P)$ such that every graph with average degree at least $c$ contains a cycle whose length is in $P$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#72	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#73	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#74	Let $f(n)\to \infty$ possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on $n$ vertices can be made bipartite by deleting at most $f(n)$ edges?Source says openFormalized	open	In Lean	No Result decision
#75	Is there a graph of chromatic number `ℵ_ 1` with `ℵ_ 1` vertices such that for all `ε > 0`, if `n` is sufficiently large and `H` is a subgraph on `n` vertices, then `H` contains an independent set of size `> n ^ (1 - ε)`?Source says openFormalized	open	In Lean	No Result decision
#76	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#77	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#78	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#79	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#80	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#81	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#82	$F(n) / \log n \to \infty as n \to \infty$ Source says openFormalized	open	In Lean	No Result decision
#83	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#84	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#85	Is it true that, for all large $n$ , $f(n + 1) \ge f(n)$ ?Source says openFormalized	open	In Lean	No Result decision
#86	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#87	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#88	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#89	Erdős [Er46] asked whether every set of $n$ distinct points in $\mathbb{R}^2$ determines $\gg \frac{n}{\sqrt{\log n}}$ many distinct distances.Source says openFormalized	open	In Lean	No Result decision
#90	Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $n^{1+O(\frac{1}{\log\log n})}$ many pairs which are distance $1$ apart?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#91	Suppose $A\subset \mathbb{R}^2$ has $\lvert A\rvert=n$ and minimises the number of distinct distances between points in $A$ . Prove that for large $n$ there are at least two (and probably many) such $A$ which are non-similar.Source says openFormalized	open	In Lean	No Result decision
#92	A sanity check to ensure the set of possible `f(n)` values is bounded above. A trivial bound is `n`, since the points equidistant from any `x` form a subset of the other `n - 1` points. This ensures `sSup` is well-defined.Source says disprovedFormalized	disproved	In Lean	No Result decision
#93	If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then they determine at least $\lfloor \frac{n}{2}\rfloor$ distinct distances.Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#94	Suppose $n$ points in $\mathbb{R}^2$ determine a convex polygon and the set of distances between them is $\{u_1,\ldots,u_t\}$ . Suppose $u_i$ appears as the distance between $f(u_i)$ many pairs of points. Then $\sum_i f(u_i)^2 \ll n^3.$ Source says proved (Lean)FormalizedResult here accepted	proved (Lean)	In Lean	accepted
#95	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#96	This lemma confirms that the set of possible unit-distance counts is bounded above, which ensures that taking the supremum (`sSup`) is a well-defined operation. The trivial upper bound is the total number of pairs of points, $\binom{n}{2}$ .Source says openFormalized	open	In Lean	No Result decision