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

110 Problems · 1 with reviewed evidence

1/3

Number	Question	Source says	Formal	Result here
#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
#97	Does every convex polygon have a vertex with no other 4 vertices equidistant from it?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#98	Let $h(n)$ be such that any $n$ points in $\mathbb{R}^2$ , with no three on a line and no four on a circle, determine at least $h(n)$ distinct distances. Does $h(n)/n\to \infty$ ?Source says openFormalized	open	In Lean	No Result decision
#99	For sufficiently large n, is it the case that any set of n points with minimum distance $1$ that minimizes diameter must contain an equilateral triangle of side length 1?Source says openFormalized	open	In Lean	No Result decision
#100	Is the diameter of $A$ at least $Cn$ for some constant $C > 0$ ?Source says openFormalized	open	In Lean	No Result decision
#101	Given $n$ points in $\mathbb{R}^2$ , no five of which are on a line, the number of lines containing four points is $o(n^2)$ .Source says openFormalized	open	In Lean	No Result decision
#102	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#103	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#104	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#105	Let $A,B\subset \mathbb{R}^2$ be disjoint sets of size $n$ and $n-3$ respectively, with not all of $A$ contained on a single line. Is there a line which contains at least two points from $A$ and no points from $B$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#106	No statement retained — open to read what the source holdsSource says falsifiableNo formal declaration	falsifiable	No formal statement	No Result decision
#107	Let $f(n)$ be minimal such that any $f(n)$ points in $ℝ^2$ , no three on a line, contain $n$ points which form the vertices of a convex $n$ -gon. Prove that $f(n) = 2^{n-2} + 1$ .Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#135	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#173	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#174	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#188	What is the smallest $k$ such that $\mathbb{R}^2$ can be red/blue coloured with no pair of red points unit distance apart, and no $k$ -term arithmetic progression of blue points with distance 1?Source says openFormalized	open	In Lean	No Result decision
#189	If $\mathbb{R}^2$ is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#193	Let $S \subseteq \mathbb{Z}^3$ be a finite set and let $A = \lbrace a_1, a_2, \ldots \rbrace$ be an infinite $S$ -walk, so that $a_{i+1} - a_i \in S$ for all $i$ . Must $A$ contain three collinear points?Source says openFormalized	open	In Lean	No Result decision
#209	Let $A$ be a finite collection of $d\geq 4$ non-parallel lines in $\mathbb{R}^2$ such that there are no points where at least four lines from $A$ meet. Must there exist a 'Gallai triangle' (or 'ordinary triangle'): three lines from $A$ which intersect in three points, and each of these intersection points only intersects two lines from $A$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#210	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#211	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#212	Is there a dense subset of ℝ^2 such that all pairwise distances are rational?Source says openFormalized	open	In Lean	No Result decision
#213	Let $n \geq 4$ . Are there $n$ points in $\mathbb{R}^2$ , no three on a line and no four on a circle, such that all pairwise distances are integers?Source says openFormalized	open	In Lean	No Result decision
#214	Let $S\subset \mathbb{R}^2$ be such that no two points in $S$ are distance $1$ apart. Must the complement of $S$ contain four points which form a unit square?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#215	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#216	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#217	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#223	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#224	If $A\subseteq \mathbb{R}^d$ is any set of $2^d+1$ points then some three points in $A$ determine an obtuse angle.Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#232	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#352	Is there some $c > 0$ such that every measurable $A \subseteq \mathbb{R}^2$ of measure $\geq c$ contains the vertices of a triangle of area 1?Source says openFormalized	open	In Lean	No Result decision
#353	Let $A\subseteq \mathbb{R}^2$ be a measurable set with infinite measure. Must $A$ contain the vertices of an isosceles trapezoid of area $1$ ? What about an isosceles triangle, or a right-angled triangle, or a cyclic quadrilateral, or a convex polygon with congruent sides?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#502	What is the size of the largest $A\subseteq \mathbb{R}^n$ such that there are only two distinct distances between elements of $A$ ? That is, $\# \{ \lvert x-y\rvert : x\neq y\in A\} = 2.$ Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#503	What is the size of the largest $A \subseteq \mathbb{R}^n$ such that every three points from $A$ determine an isosceles triangle? That is, for any three points $x$ , $y$ , $z$ from $A$ , at least two of the distances $\|x - y\|$ , $\|y - z\|$ , $\|x - z\|$ are equal.Source says openFormalized	open	In Lean	No Result decision
#504	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#505	Erdős Problem 505 (disproved). Borsuk's conjecture is false for sufficiently large $n$ : there exists a dimension $n$ and a bounded set $S \subseteq \mathbb{R}^n$ with positive diameter such that $S$ cannot be covered by $n + 1$ subsets each of diameter strictly less than $\operatorname{diam}(S)$ .Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#506	No statement retained — open to read what the source holdsSource says decidableNo formal declaration	decidable	No formal statement	No Result decision
#507	Let $\alpha(n)$ be such that every set of $n$ points in the unit disk contains three points which determine a triangle of area at most $\alpha(n)$ . Estimate $\alpha(n)$ .Source says openFormalized	open	In Lean	No Result decision
#508	The "chromatic number of the plane" is at least 4. This can be proven by considering the Moser-Spindel graph or the Golomb graph graph.Source says openFormalized	open	In Lean	No Result decision
#526	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#528	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision