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

16/26

Number	Question	Source says	Formal	Result here
#721	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#722	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#723	If there is a finite projective plane of order $n$ then must $n$ be a prime power?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#724	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#725	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#726	As $n\to \infty$ ranges over integers $\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}$ ?Source says openFormalized	open	In Lean	No Result decision
#727	Let $k ≥ 2$ . Does $((n+k)!)^2∣(2n)!$ hold for infinitely many $n$ ?Source says openFormalized	open	In Lean	No Result decision
#728	Let $\varepsilon$ be sufficiently small and $C, C' > 0$ . Are there integers $a, b, n$ such that $a, b > \varepsilon n\quad a!\, b! \mid n!\, (a + b - n)!,$ and $C \log n < a + b - n < C' \log n ?$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#729	Let $C>0$ be a constant. Are there infinitely many integers $a,b,n$ with $a+b> n+C\log n$ such that the denominator of $\frac{n!}{a!b!}$ contains only primes $\ll_C 1$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#730	Are there infinitely many pairs of integers $n < m$ such that $\binom{2n}{n}$ and $\binom{2m}{m}$ have the same set of prime divisors?Source says openFormalized	open	In Lean	No Result decision
#731	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#732	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#733	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#734	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#735	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#736	No statement retained — open to read what the source holdsSource says not provableNo formal declaration	not provable	No formal statement	No Result decision
#737	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#738	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#739	No statement retained — open to read what the source holdsSource says not provableNo formal declaration	not provable	No formal statement	No Result decision
#740	Let $\mathfrak{m}$ be an infinite cardinal and $G$ be a graph with chromatic number $\mathfrak{m}$ . Let $r\geq 1$ . Must $G$ contain a subgraph of chromatic number $\mathfrak{m}$ which does not contain any odd cycle of length $\leq r$ ?Source says openFormalized	open	In Lean	No Result decision
#741	Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive upper density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive upper density?Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#742	The complete bipartite graph $K_{a, b}$ has exactly $a \cdot b$ edges. The bound $\lfloor n^2 / 4 \rfloor$ in the Murty-Simon conjecture is attained by the balanced case $K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}$ .Source says decidableFormalized	decidable	In Lean	No Result decision
#743	No statement retained — open to read what the source holdsSource says falsifiableNo formal declaration	falsifiable	No formal statement	No Result decision
#744	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#745	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#746	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#747	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#748	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#749	Let $\epsilon>0$ . Does there exist $A\subseteq \mathbb{N}$ such that the lower density of $A+A$ is at least $1-\epsilon$ and yet $1_A\ast 1_A(n) \ll_\epsilon 1$ for all $n$ ?Source says openFormalized	open	In Lean	No Result decision
#750	Let $f(m)$ be some function such that $f(m)\to \infty$ as $m\to \infty$ . Does there exist a graph $G$ of infinite chromatic number such that every subgraph on $m$ vertices contains an independent set of size at least $\frac{m}{2}-f(m)$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#751	Let $G$ be a graph with chromatic number $\chi(G)=4$ . If $m_1<m_2<\cdots$ are the lengths of the cycles in $G$ then can $\min(m_{i+1}-m_i)$ be arbitrarily large?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#752	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#753	The list chromatic number $\chi_L(G)$ is defined to be the minimal $k$ such that for any assignment of a list of $k$ colours to each vertex of $G$ (perhaps different lists for different vertices) a colouring of each vertex by a colour on its list can be chosen such that adjacent vertices receive distinct colours.Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#754	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#755	Erdős asked whether every $n$ -point set in $\mathbb{R}^6$ spans at most $(1/27 + o(1)) n^3$ unit equilateral triangles.Source says provedFormalized	proved	In Lean	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$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#757	What is the supremum of the set of admissible numbers?Source says openFormalized	open	In Lean	No Result decision
#758	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#759	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#760	The cochromatic number of $G$ , denoted by $\zeta(G)$ , is the minimum number of colours needed to colour the vertices of $G$ such that each colour class induces either a complete graph or independent set.Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#761	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#762	The cochromatic number of $G$ , denoted by $\zeta(G)$ , is the minimum number of colours needed to colour the vertices of $G$ such that each colour class induces either a complete graph or empty graph.Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#763	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#764	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#765	No statement retained — open to read what the source holdsSource says solved (Lean)No formal declaration	solved (Lean)	No formal statement	No Result decision
#766	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#767	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#768	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision