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

14/26

Number	Question	Source says	Formal	Result here
#625	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#626	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#627	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#628	Let $G$ be a graph with chromatic number $k$ containing no $K_k$ . If $a,b\geq 2$ and $a+b=k+1$ then must there exist two disjoint subgraphs of $G$ with chromatic numbers $\geq a$ and $\geq b$ respectively?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#629	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#630	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#631	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#632	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#633	Which triangles can only be decomposed into a square number of congruent triangles?Source says solvedFormalized	solved	In Lean	No Result decision
#634	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#635	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#636	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#637	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#638	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#639	Is it true that if the edges of $K_n$ are 2-coloured then there are at most $n^2/4$ many edges which do not occur in a monochromatic triangle?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#640	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#641	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#642	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#643	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#644	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#645	If ℕ is $2$ -coloured then there must exist a monochromatic three-term arithmetic progression $x,x+d,x+2d$ such that $d>x$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#646	Let $p_1,\ldots,p_k$ be distinct primes. Are there infinitely many $n$ such that $n!$ is divisible by an even power of each of the $p_i$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#647	Let $\tau(n)$ count the number of divisors of $n$ . Is there some $n > 24$ such that $\max_{m < n}(m + \tau(m)) \leq n + 2?$ Source says verifiableFormalized	verifiable	In Lean	No Result decision
#648	Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1<a_2<\cdots <a_t <n$ such that $P(a_1)>P(a_2)>\cdots >P(a_t)$ where $P(m)$ is the greatest prime factor of $m$ . Estimate $g(n)$ .Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#649	Let $P(m)$ denote the greatest prime factor of $m$ . Is it true that, for any two primes $p,q$ , there exists some integer $n$ such that $P(n)=p$ and $P(n+1)=q$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#650	Let $f(m)$ be such that if $A\subseteq \{1,\ldots,N\}$ has $\lvert A\rvert=m$ then every interval in $[1,\infty)$ of length $2N$ contains $\geq f(m)$ many distinct integers $b_1,\ldots,b_r$ where each $b_i$ is divisible by some $a_i\in A$ , where $a_1,\ldots,a_r$ are distinct.Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#651	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#652	No statement retained — open to read what the source holdsSource says provedNo 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$ ?Source says openFormalized	open	In Lean	No Result decision
#654	No statement retained — open to read what the source holdsSource says openNo 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?Source says openFormalized	open	In Lean	No Result decision
#656	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#657	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#658	No statement retained — open to read what the source holdsSource says proved (Lean)No formal declaration	proved (Lean)	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}}$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#660	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#661	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#662	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#663	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#664	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#665	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#666	Let $Q_n$ be the $n$ -dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Is it true that, for every $\epsilon>0$ , if $n$ is sufficiently large, every subgraph of $Q_n$ with $\geq \epsilon n2^{n-1}$ many edges contains a $C_6$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#667	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#668	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#669	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#670	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#671	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#672	Can the product of an arithmetic progression of positive integers $n, n + d, ..., n + (k - 1)d$ of length ≥ 4, with $(n, d) = 1$ , be a perfect power?Source says verifiableFormalized	verifiable	In Lean	No Result decision