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

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.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
#97	Does every convex polygon have a vertex with no other 4 vertices equidistant from it?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$ ?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?openFormalized	open	In Lean	No Result decision
#100	Is the diameter of $A$ at least $Cn$ for some constant $C > 0$ ?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)$ .openFormalized	open	In Lean	No Result decision
#102	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#103	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#104	No statement retained — open to read what the source holdsopenNo 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$ ?disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#106	No statement retained — open to read what the source holdsfalsifiableNo 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$ .falsifiableFormalized	falsifiable	In Lean	No Result decision
#135	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#173	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#174	No statement retained — open to read what the source holdsopenNo 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?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?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?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$ ?disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#210	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#211	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#212	Is there a dense subset of ℝ^2 such that all pairwise distances are rational?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?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?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#215	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#216	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#217	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#223	No statement retained — open to read what the source holdssolvedNo 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.proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#232	No statement retained — open to read what the source holdsprovedNo 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?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?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.$ 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.openFormalized	open	In Lean	No Result decision
#504	No statement retained — open to read what the source holdssolvedNo 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)$ .disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#506	No statement retained — open to read what the source holdsdecidableNo 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)$ .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](https://de.wikipedia.org/wiki/Moser-Spindel) or the [Golomb graph](https://en.wikipedia.org/wiki/Golomb_graph) graph.openFormalized	open	In Lean	No Result decision
#526	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#528	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision

Problems

Search problems.science