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

10/26

Number	Question	Source says	Formal	Result here
#433	No statement retained — open to read what the source holdsSource says proved (Lean)No formal declaration	proved (Lean)	No formal statement	No Result decision
#434	Let $k \le n$ . What choice of $A\subseteq\{1, \dots, n\}$ (with $\text{gcd}(A) = 1$ ) of size $\|A\| = k$ maximises the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed)? Is it $\{n, n - 1, \dots, n - k + 1\}$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#435	Let $n\in\mathbb{N}$ with $n\neq p^k$ for any prime $p$ and $k\geq 0$ . What is the largest integer not of the form $\sum_{1\leq i<n}c_i\binom{n}{i}$ where the $c_i\geq 0$ are integers?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#436	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#437	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#438	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#439	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#440	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#441	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#442	Let $\operatorname{Log} x := \max\{\log x, 1\}$ , $\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x)$ , and $\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)).$ Is it true that if $A\subseteq\mathbb{N}$ is such that $\frac{1}{\operatorname{Log}_2 x} \sum_{n\in A: n\leq x} \frac{1}{n}\to\infty$ then $\left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2 \sum_{n, m \in A: n < m \leq x} \frac{1}{\operatorname{lcm}(n, m)}\to\infty$ as $x\to\infty$ ?Source says disprovedFormalized	disproved	In Lean	No Result decision
#443	Let $m,n\geq 1$ . What is $\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}?$ Can it be arbitrarily large?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#444	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#445	Is it true that, for any $c>1/2$ , if $p$ is a sufficiently large prime then, for any $n\geq 0$ , there exist $a,b\in(n,n+p^c)$ such that $ab\equiv 1\pmod{p}$ ?Source says openFormalized	open	In Lean	No Result decision
#446	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#447	How large can a union-free collection $\mathcal{F}$ of subsets of $[n]$ be? By union-free we mean there are no solutions to $A\cup B=C$ with distinct $A,B,C\in \mathcal{F}$ . Must $\lvert \mathcal{F}\rvert =o(2^n)$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#448	Let $\tau(n)$ count the divisors of $n$ and $\tau^+(n)$ count the number of $k$ such that $n$ has a divisor in $[2^k, 2^{k+1})$ . Is it true that, for all $\epsilon > 0$ , $\tau^+(n) < \epsilon \cdot \tau(n)$ for almost all $n$ ?Source says disprovedFormalized	disproved	In Lean	No Result decision
#449	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#450	How large must $y=y(\epsilon,n)$ be such that the number of integers in $(x,x+y)$ with a divisor in $(n,2n)$ is at most $\epsilon y$ ?Source says openFormalized	open	In Lean	No Result decision
#451	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#452	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#453	Is it true that, for all sufficiently large $n$ , there exists some $i<n$ such that $p_n^2 < p_{n+i}p_{n-i},$ where $p_k$ is the $k$ th prime?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#454	Is it true that `limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤`?Source says openFormalized	open	In Lean	No Result decision
#455	Let `q : ℕ → ℕ` be a strictly increasing sequence of primes such that `q (n + 2) - q (n + 1) ≥ q (n + 1) - q n`. Must `lim q n / (n ^ 2) = ∞`?Source says openFormalized	open	In Lean	No Result decision
#456	Is it true that $m_n<p_n$ for almost all $n$ ?Source says openFormalized	open	In Lean	No Result decision
#457	Is there some $\epsilon > 0$ such that there are infinitely many $n$ where all primes $p \le (2 + \epsilon) \log n$ divide $\prod_{1 \le i \le \log n} (n + i)?$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#458	Let $\operatorname{lcm}(1, \dots, n)$ denote the least common multiple of $\{1, \dots, n\}$ . Let $p_k$ be the $k$ -th prime. Is it true that for all $k \geq 1$ , $\operatorname{lcm}(1, \dots, p_{k+1}-1) < p_k \cdot \operatorname{lcm}(1, \dots, p_k)$ ?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#459	Let $f(u)$ be the largest $v$ such that no $m\in (u,v)$ is composed entirely of primes dividing $uv$ . Estimate $f(u)$ .Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#460	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#461	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#462	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#463	Is there a function $f$ with $f(n)\to\infty$ as $n\to\infty$ such that, for all large $n$ , there is a composite number $m$ such that $n + f(n) < m < n + p(m)$ Here $p(m)$ is the least prime factor of $m$ .Source says openFormalized	open	In Lean	No Result decision
#464	Let $A=\{n_1<n_2<\cdots\}\subset \mathbb{N}$ be a lacunary sequence (so there exists some $\epsilon>0$ with $n_{k+1}\geq (1+\epsilon)n_k$ for all $k$ ). Must there exist an irrational $\theta$ such that $\{ \\|\theta n_k\\| : k\geq 1\}$ is not dense in $[0,1]$ (where $\\| x\\|$ is the distance to the nearest integer)?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#465	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#466	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#467	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#468	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#469	Let $A$ be the set of all $n$ such that $n = d_1 + ⋯ + d_k$ with $d_i$ distinct proper divisors of $n$ , but this is not true for any $m ∣ n$ with $m < n$ . Does: $\sum_{n ∈ A} \frac 1 n$ converge?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#470	Are there any odd weird numbers?Source says openFormalized	open	In Lean	No Result decision
#471	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#472	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#473	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#474	No statement retained — open to read what the source holdsSource says not provableNo formal declaration	not provable	No formal statement	No Result decision
#475	No statement retained — open to read what the source holdsSource says decidableNo formal declaration	decidable	No formal statement	No Result decision
#476	Let $A\subseteq \mathbb{F}_p$ . Let $A\hat{+}A = \{ a+b : a\neq b \in A\}.$ Is it true that $\lvert A\hat{+}A\rvert \geq \min(2\lvert A\rvert-3,p)?$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#477	Is there a polynomial $f:\mathbb{Z}\to \mathbb{Z}$ of degree at least $2$ and a set $A\subset \mathbb{Z}$ such that for any $z\in \mathbb{Z}$ there is exactly one $a\in A$ and $b\in \{ f(n) : n\in\mathbb{Z}\}$ such that $z=a+b$ ?Source says openFormalized	open	In Lean	No Result decision
#478	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#479	Is it true that, for all $k\neq 1$ , there are infinitely many $n$ such that $2^n\equiv k\pmod{n}$ ?Source says openFormalized	open	In Lean	No Result decision
#480	Let $x_1,x_2,\ldots\in [0,1]$ be an infinite sequence. Is it true that $\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq 5^{-1/2}\approx 0.447?$ A conjecture of Newman.Source says provedFormalized	proved	In Lean	No Result decision