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

55 Problems · 1 with reviewed evidence

1/2

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
#103	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#132	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#135	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	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
#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
#232	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	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
#604	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#605	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#652	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#653	Let $x_1,\ldots,x_n\in \mathbb{R}^2$ and let $R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}$ , where the points are ordered such that $R(x_1)\leq \cdots \leq R(x_n).$ Let $g(n)$ be the maximum number of distinct values the $R(x_i)$ can take. Is it true that $g(n) \geq (1-o(1))n$ ?openFormalized	open	In Lean	No Result decision
#654	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#655	Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points. Are there at least $(1+c)\frac{n}{2}$ distinct distances determined between the $x_i$ , for some constant $c>0$ and all $n$ sufficiently large?openFormalized	open	In Lean	No Result decision
#657	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#659	Is there a set of $n$ points in $\mathbb{R}^2$ such that every subset of $4$ points determines at least $3$ distances, yet the total number of distinct distances is $\ll \frac{n}{\sqrt{\log n}}$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#660	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#661	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#662	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#668	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#670	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#754	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#756	Let $A\subset \mathbb{R}^2$ be a set of $n$ points. Can there be $\gg n$ many distinct distances each of which occurs for more than $n$ many pairs from $A$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#757	What is the supremum of the set of admissible numbers?openFormalized	open	In Lean	No Result decision
#953	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#956	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#957	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#958	Let $A\subset \mathbb{R}^2$ be a finite set of size $n$ , and let $\{d_1,\ldots,d_k\}$ be the set of distances determined by $A$ . Let $f(d)$ be the multiplicity of $d$ , that is, the number of unordered pairs from $A$ of distance $d$ apart.disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#959	Let $A\subseteq \mathbb{R}^2$ be a set of size $n$ and let $\{d_1,\ldots,d_k\}$ be the set of distinct distances determined by $A$ . Let $f(d)$ be the number of times the distance $d$ is determined, ordered so that $f(d_1)\geq f(d_2)\geq \cdots \geq f(d_k)$ . Estimate $\max (f(d_1)-f(d_2)),$ where the maximum is taken over all $A$ of size $n$ (this is `extremalGap n`).openFormalized	open	In Lean	No Result decision
#982	If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then some vertex has at least $\lfloor\frac{n}{2}\rfloor$ different distances to other vertices.falsifiableFormalized	falsifiable	In Lean	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

Problems

Search problems.science