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

2/26

Number	Question	Source says	Formal	Result here
#49	No statement retained — open to read what the source holdsprovedNo 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?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 → ∞$ ?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}?$ openFormalized	open	In Lean	No Result decision
#53	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#54	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#55	No statement retained — open to read what the source holdssolvedNo 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.disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#57	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#58	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#59	No statement retained — open to read what the source holdsdisprovedNo 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$ ?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.openFormalized	open	In Lean	No Result decision
#62	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#63	No statement retained — open to read what the source holdsprovedNo 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$ ?falsifiableFormalized	falsifiable	In Lean	No Result decision
#65	No statement retained — open to read what the source holdsopenNo 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$ ?openFormalized	open	In Lean	No Result decision
#67	The Erdős discrepancy problemprovedFormalized	proved	In Lean	No Result decision
#68	Is $\sum_{n=2}^\infty \frac{1}{n!-1}$ irrational?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$ .)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$ ?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$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#72	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#73	No statement retained — open to read what the source holdsprovedNo 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?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 - ε)`?openFormalized	open	In Lean	No Result decision
#76	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#77	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#78	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#79	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#80	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#81	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#82	$F(n) / \log n \to \infty as n \to \infty$ openFormalized	open	In Lean	No Result decision
#83	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#84	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#85	Is it true that, for all large $n$ , $f(n + 1) \ge f(n)$ ?openFormalized	open	In Lean	No Result decision
#86	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#87	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#88	No statement retained — open to read what the source holdsprovedNo 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.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?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.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.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.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.$ proved (Lean)FormalizedResult accepted	proved (Lean)	In Lean	accepted
#95	No statement retained — open to read what the source holdsprovedNo 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}$ .openFormalized	open	In Lean	No Result decision

Problems

Search problems.science