Problems · Open Proof Network

erdos-1003openstatement unchecked

Are there infinitely many solutions to $\phi(n) = \phi(n+1)$, where $\phi$ is the Euler totient function?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/1003

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-1003the problem's statementopen1 attemptWork on this →

erdos-1050provedstatement unchecked

Erdős Problem 1050. The series $\sum_{n=1}^\infty \frac{1}{2^n - 3}$ is irrational. The source sum runs over $n \ge 1$; as a tsum over ℕ (which starts at $0$) it is reindexed $n \mapsto n + 1$, i.e. $\sum_{n=0}^\infty 1/(2^{n+1} - 3)$.

Statement from formal-conjectures (FormalConjectures/ErdosProblems/1050.lean) · erdosproblems.com/1050; the record lists no licensed source text.

ProvedExplainedWritten up Calibration target, no steward needed 6 files need words View the graph →

erdos-1050the problem's statementproved2 attemptsView proof →

Show 13 more statements, 1 open

erdos-1050--h1left open by a proof skeletonsuperseded0 attemptsBlocked$\exists\, a,b:\ \bigl(\forall n\in\mathbb{N},\ b_n\,T-a_n\neq 0\bigr)\ \wedge\ \lim_{n\to\infty}\bigl(b_n\,T-a_n\bigr)=0,\qquad T=\sum_{m=0}^{\infty}\frac{1}{2^{m+3}-3}$

erdos-1050--h1-v2left open by a proof skeletonproved4 attemptsView proof →$\exists\, a,b:\mathbb{N}\to\mathbb{Z}\ \ \bigl(\forall n\in\mathbb{N},\ b_n\,T-a_n\neq 0\bigr)\ \wedge\ \lim_{n\to\infty}\bigl(b_n\,T-a_n\bigr)=0,\qquad T=\sum_{m=0}^{\infty}\frac{1}{2^{m+3}-3}$

erdos-1050--h1-v2--h1left open by a proof skeletonopen2 attemptsWork on this →$T=\sum_{n=0}^{\infty}\frac{1}{2^{n+3}-3}=\frac15+\frac1{13}+\frac1{29}+\frac1{61}+\cdots\ \notin\ \mathbb{Q}$

erdos-1050--h1-v2--h2left open by a proof skeletonproved1 attemptView proof →$\exists\, a,b:\mathbb{N}\to\mathbb{Z}\ \ \forall n\ge 1:\qquad b(n)\,z-a(n)\;=\;9^n\,W(n)\,E(n)$

erdos-1050--h1-v2--h2--h1derived by the compilerproved0 attemptsView proof →$\exists\, a:\mathbb{N}\to\mathbb{Z}\ \ \forall n\ge 1:\qquad a(n)\;=\;9^n\,W(n)\,\bigl(S_1(n)-S_2(n)\bigr)$

erdos-1050--h1-v2--h3derived by the compilerproved0 attemptsView proof →$\forall n\in\mathbb{N}\ \ \exists d\in\mathbb{N}:\qquad d>0,\quad d^2\le 2^{3n^2},\quad d\,Q_x(n)\in\mathbb{Z},\quad d\,A_q(n)\in\mathbb{Z}$

erdos-1050--h1-v2--h4derived by the compilerproved0 attemptsView proof →$\forall n\in\mathbb{N}:\qquad R_n>0\quad\wedge\quad R_n^{2}\,2^{4n^2}\le 2^{2n+4},\qquad R_n=3T\,Q_x(n)-A_q(n),\quad T=\sum_{m=0}^{\infty}\frac{1}{2^{m+3}-3}$

spec-180d8b72 erdos_1050_pade_remainder_boundproposed by a contributorproved0 attemptsView proof →$\forall n\in\mathbb{N}:\qquad R_n>0\quad\wedge\quad R_n^{2}\,2^{4n^2}\le 2^{2n+4},\qquad R_n=3T\,Q_x(n)-A_q(n),\quad T=\sum_{m=0}^{\infty}\frac{1}{2^{m+3}-3}$

spec-1a5ab7c3 erdos_1050_upper_half_mersenne_clearsproposed by a contributorproved0 attemptsView proof →$\forall n,k\in\mathbb{N},\ k\le n,\ \ \forall c:\mathbb{N}\to\mathbb{Z}\ \ \exists z\in\mathbb{Z}:\qquad z=\Bigl(\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)\Bigr)\cdot\sum_{j=0}^{k}\frac{c_j}{2^{\,k-j}-1}$

spec-440db0f9 erdos_1050_gauss_binom_two_intproposed by a contributorproved0 attemptsView proof →$\forall n,k\in\mathbb{N}\ \ \exists z\in\mathbb{Z}:\qquad z=\prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}$

spec-eb1219eb erdos_1050_hden_small_casesproposed by a contributorproved0 attemptsView proof →$\forall n\in\{5,7\}\ \ \exists d\in\mathbb{N}:\qquad d>0,\quad d^2\le 2^{3n^2},\quad d\,Q_x(n)\in\mathbb{Z},\quad d\,A_q(n)\in\mathbb{Z}$

spec-f2b55478 erdos_1050_pade_remainder_coeffproposed by a contributorproved0 attemptsView proof →$\forall n<m:\quad \sum_{j=0}^{n}\frac{(-1)^j\,2^{j(j-1)/2}\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}}{2^{\,m-j}-1} \;=\;\frac{2^{n^2}\prod_{i=0}^{n-1}(2^{\,i+1}-1)\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}}{\prod_{j=0}^{n}(2^{\,m-j}-1)}$

spec-ffd3137a erdos_1050_pade_numerator_closed_formproposed by a contributorproved0 attemptsView proof →$\forall k\le n:\quad \sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\;=\;Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}}-\sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1}-\sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr)+\sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1}$

erdos-1065openstatement unchecked

Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$? This is mentioned as B46 in Unsolved Problems in Number Theory by Richard K. Guy

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/1065

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-1065the problem's statementopen0 attemptsWork on this →

erdos-1094openstatement unchecked

For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions.

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/1094

ProvedExplainedWritten up Steward · Michael Higgins self-admitted 112 files need words View problem →

erdos-1094the problem's statementopen2 attemptsWork on this →

Show 64 more statements, 53 open

erdos-1094--h1derived by the compilerproved0 attemptsView proof →$\forall k\ge 1:\quad \Bigl\{n\in\mathbb{N} \;:\; k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor\Bigr\}\ \text{ is finite}$

erdos-1094--h2derived by the compileropen1 attemptWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$

erdos-1094--h2--h1left open by a proof skeletonopen2 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$

erdos-1094--h2--h1--h1left open by a proof skeletonopen1 attemptWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$

erdos-1094--h2--h1--h1--h1derived by the compileropen2 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$

erdos-1094--h2--h1--h1--h1--h1derived by the compileropen2 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^2,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$

erdos-1094--h2--h1--h1--h1--h1--h1derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$

erdos-1094--h2--h1--h1--h1--h1--h2derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$

erdos-1094--h2--h1--h1--h1--h2derived by the compileropen2 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$

erdos-1094--h2--h1--h1--h1--h2--h1derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$

erdos-1094--h2--h1--h1--h1--h2--h2derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k,p,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,pq,\ p,q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$

erdos-1094--h2--h1--h4left open by a proof skeletonopen1 attemptWork on this →$\exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^2\le n,\ n<k\bigl(k+3k^{21/40}\bigr),\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$

erdos-1094--h2--h1--h4--h1derived by the compileropen2 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime}\ \Longrightarrow\ k\le K$

erdos-1094--h2--h1--h4--h1--h1derived by the compileropen0 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ n\text{ prime},\ \ \gcd(n,k)=1\ \Longrightarrow\ k\le K$

erdos-1094--h2--h1--h4--h1--h2derived by the compileropen2 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ 2\le\gcd(n,k)\ \Longrightarrow\ k\le K$

erdos-1094--h2--h1--h4--h1--h2--h1derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k:\ \text{(the node's hypotheses)} \wedge 2 \le \gcd(n,k) < k \Rightarrow k \le K$

erdos-1094--h2--h2left open by a proof skeletonopen1 attemptWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^3\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$

erdos-1094--h2--h2--h1left open by a proof skeletonopen1 attemptWork on this →$\exists C>0\ \ \exists k_0\in\mathbb{N}\ \ \forall k\ge k_0:\qquad \frac{C\,k^{21/40}}{\log k}\ \le\ \#\bigl\{p\text{ prime}:\ k<p<k+k^{21/40}\bigr\}$

erdos-1094--h2--h2--h2left open by a proof skeletonproved1 attemptView proof →$\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$

erdos-1094--h2--h2--h2--h1left open by a proof skeletonproved0 attemptsView proof →$\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\tfrac12\,k^{2-21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$

erdos-1094--h2--h2--h2--h2left open by a proof skeletonproved1 attemptView proof →$\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2-21/40}<n\le\frac{k^2}{(\log k)^2}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$

erdos-1094--h2--h2--h2--h2--h1derived by the compilerproved0 attemptsView proof →$\exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2-21/40}<n\le\frac{k^2}{(\log k)^2}\ \Longrightarrow\ \#\Bigl\{m\in\mathbb{Z}:\ k<m<k+k^{21/40},\ \Bigl|\frac{n}{m}-\operatorname{round}\!\Bigl(\frac{n}{m}\Bigr)\Bigr|<\frac{1}{k^{1-21/40}}\Bigr\}<3+56\,k^{2\cdot 21/40-1}+\frac{k^{21/40}}{(\log k)^{2}}$

erdos-1094--h2--h2--h2--h3left open by a proof skeletonproved1 attemptView proof →$\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \frac{k^2}{(\log k)^2}<n\le\tfrac12\,k^{2+21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$

erdos-1094--h2--h2--h2--h3--h1derived by the compilerproved1 attemptView proof →$\#\Bigl\{m\in\mathbb{Z}:\ k<m<k+k^{21/40},\ \Bigl|\frac{n}{m}-\operatorname{round}\!\Bigl(\frac{n}{m}\Bigr)\Bigr|<\frac{1}{k^{1-21/40}}\Bigr\}<65536\,k^{21/40}\Bigl[\Bigl(\frac{n\,r!\,\lambda^r}{k^{r+1}}\Bigr)^{\frac{1}{2r-1}}+\Bigl(\frac{k^{r+21/40}}{n\,r!\,\lambda^r}\Bigr)^{\frac{1}{r-1}}+\Bigl(\frac{(r+1)\lambda}{k}\Bigr)^{\frac{1}{2r}}\Bigr]+2r\lambda$

erdos-1094--h2--h2--h2--h3--h1--h1derived by the compilerproved1 attemptView proof →$|S|<65536\,N\Bigl[(D_r\lambda^rW^2)^{\frac{1}{2r-1}}+\Bigl(\frac{\delta W^2}{D_r\lambda^r}\Bigr)^{\frac{1}{r-1}}+\Bigl(\frac{D_{r+1}\lambda W^2}{D_r}\Bigr)^{\frac{1}{2r}}\Bigr]+2r\lambda$

erdos-1094--h2--h2--h2--h3--h1--h1--h1derived by the compilerproved2 attemptsView proof →$65536\,X'<1\ \Longrightarrow\ |S'|<65536\,N'X'+2r\lambda',\qquad X'=(D'\lambda'^{\,r}W^2)^{\frac{1}{2r-1}}+\Bigl(\frac{\delta W^2}{D'\lambda'^{\,r}}\Bigr)^{\frac{1}{r-1}}+\Bigl(\frac{D_1'\lambda' W^2}{D'}\Bigr)^{\frac{1}{2r}}$

erdos-1094--h2--h2--h2--h3--h1--h1--h1--h1derived by the compilerproved0 attemptsView proof →$\exists a:\{0,\dots,2r-1\}\to\mathbb{Z}:\quad \sum_{i}a_i w_i u_i^{\,j}=0\ (j<r),\qquad \sum_{i}a_i w_i u_i^{\,r}\ne 0,\qquad |a_i|\le\Bigl(\frac{256\,M}{r}\Bigr)^{r-1}W$

erdos-1094--h2--h2--h2--h4left open by a proof skeletonproved1 attemptView proof →$\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2+21/40}<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$

erdos-1094--h2--h2--h3left open by a proof skeletonopen1 attemptWork on this →$\exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^3\le n,\ \exp\!\Bigl(\frac{(\log k)^2}{20\,\log\log k}\Bigr)<n+1,\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$

erdos-1094--h2--h2--h3--h1derived by the compileropen2 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^3\le n,\ \ \exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)<n+1,\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime}\ \Longrightarrow\ k\le K$

erdos-1094--h2--h2--h3--h1--h1derived by the compileropen0 attemptsWork on this →$\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^3\le n,\ \ \exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)<n+1,\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ k\nmid n\ \Longrightarrow\ k\le K$

erdos-1094--h3derived by the compileropen3 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^2,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$

erdos-1094--h3--h1derived by the compileropen2 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1left open by a proof skeletonopen2 attemptsWork on this →$\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ k \text{ even} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h1derived by the compileropen2 attemptsWork on this →$\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h1--h1derived by the compileropen0 attemptsWork on this →$\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k,\ \ 5\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h1--h2derived by the compileropen0 attemptsWork on this →$\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k,\ \ 5\nmid k,\ \ k \bmod 5 \le n \bmod 5 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h2derived by the compileropen1 attemptWork on this →$\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\nmid k,\ \ k \bmod 3 \le n \bmod 3 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h2--h1derived by the compileropen2 attemptsWork on this →$\exists K_3\ \forall n,k\in\mathbb{N}:\quad K_3<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\nmid k,\ \ k \bmod q \le n \bmod q\ (q=3,5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h2--h1--h1derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ k\equiv 1 \pmod 3,\ \ 1\le n \bmod 3,\ \ k \bmod q \le n \bmod q\ (q=5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h2--h1--h2derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ k\equiv 2 \pmod 3,\ \ n\equiv 2 \pmod 3,\ \ k \bmod q \le n \bmod q\ (q=5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h1--h3derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ \bigl(\forall q\le k \text{ prime},\ q\mid n \Rightarrow q\mid k\bigr) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2left open by a proof skeletonopen1 attemptWork on this →$\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h1derived by the compileropen2 attemptsWork on this →$\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h1--h1derived by the compileropen0 attemptsWork on this →$\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\mid k,\ \ 5\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h1--h2derived by the compileropen0 attemptsWork on this →$\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\mid k,\ \ 5\nmid k,\ \ k \bmod 5 \le n \bmod 5 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h2derived by the compileropen2 attemptsWork on this →$\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\nmid k,\ \ k \bmod 3 \le n \bmod 3 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h2--h1derived by the compileropen0 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ k\equiv 1 \pmod 3 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h2--h2derived by the compileropen2 attemptsWork on this →$\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ k\equiv 2 \pmod 3,\ \ n\equiv 2 \pmod 3 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h2--h2--h1derived by the compileropen0 attemptsWork on this →$5 \mid k \Rightarrow \exists\, p \le k \text{ prime},\ n \bmod p < k \bmod p$

erdos-1094--h3--h1--h2--h2--h2--h2derived by the compileropen0 attemptsWork on this →$0 < k \bmod 5 \le n \bmod 5 \Rightarrow \exists\, p \le k \text{ prime},\ n \bmod p < k \bmod p$

erdos-1094--h3--h2left open by a proof skeletonopen1 attemptWork on this →$\exists C, K_1\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n,\ \ \operatorname{minFac}\tbinom{n}{k}>k \implies k^2 \le C\cdot n\cdot\lfloor\log_2 k\rfloor$

erdos-1094--h3--h2--h1derived by the compileropen2 attemptsWork on this →$\exists c\in\mathbb{R},\ c>0,\ \exists K_2\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n,\ \ \operatorname{minFac}\tbinom{n}{k}>k \implies k^{1+c} < n$

erdos-1094--h3--h2--h1--h1derived by the compilerneeds a witness0 attemptsSupply a witness →$\exists c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$

erdos-1094--h3--h2--h2derived by the compileropen0 attemptsWork on this →$\forall c>0\ \exists K_3\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_3<k,\ \ k^{1+c}<n<k^{7/4} \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<k,\ \ p\mid\tbinom{n}{k}$

erdos-1094--h3--h2--h3derived by the compileropen0 attemptsWork on this →$\exists C, K_4\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_4<k,\ \ k^{7/4}\le n,\ \ C\cdot n\cdot\lfloor\log_2 k\rfloor < k^2 \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<k,\ \ p\mid\tbinom{n}{k}$

erdos-1094--h3--h3left open by a proof skeletonopen1 attemptWork on this →$\forall C\in\mathbb{N}\ \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ k^2\le C\cdot n\cdot\lfloor\log_2 k\rfloor,\ \ n<k^2 \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<\tfrac{11k}{20},\ \ n \bmod p < k \bmod p$

erdos-1094--h3--h3--h1left open by a proof skeletonopen1 attemptWork on this →$\exists K_3\in\mathbb{N}\ \forall k\in\mathbb{N}:\quad K_3<k \implies \frac{k}{100} \le \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p$

erdos-1094--h3--h3--h1--h1derived by the compileropen2 attemptsWork on this →$\forall \varepsilon>0\ \exists X\in\mathbb{R}\ \forall x\in\mathbb{R}:\quad X\le x \implies |\theta(x)-x| \le \varepsilon x$

erdos-1094--h3--h3--h1--h1--h1derived by the compileropen2 attemptsWork on this →$\psi(x) = x + o(x)$, i.e. $\forall \varepsilon>0\ \exists X\ \forall x\ge X,\ |\psi(x)-x|\le\varepsilon x$

erdos-1094--h3--h3--h1--h1--h1--h1derived by the compileropen0 attemptsWork on this →$f\ge0$, $\sum f(n)n^{-s}$ converges for $\Re s>1$ and $F(s)-A/(s-1)$ extends continuously to $\Re s\ge1$ $\Rightarrow$ $\frac1N\sum_{n<N}f(n)\to A$

erdos-1094--h3--h3--h1--h1--h1--h2derived by the compileropen0 attemptsWork on this →$\sum_n \Lambda(n) n^{-s} - \frac{1}{s-1}$ extends continuously to $\Re s\ge 1$

erdos-1094--h3--h3--h2left open by a proof skeletonopen1 attemptWork on this →$\forall C\in\mathbb{N},\ \varepsilon>0\ \exists K_4\ \forall n,k\in\mathbb{N}:\quad K_4<k,\ \ k^2\le C\cdot n\cdot\lfloor\log_2 k\rfloor,\ \ n<k^2 \implies \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \Bigl(\Bigl\{\frac{n}{p}\Bigr\}-\frac12\Bigr)\log p\Bigr| \le \varepsilon k$

erdos-1094--h3--h3--h2--h1derived by the compileropen0 attemptsWork on this →$\forall C\in\mathbb{N},\ \delta>0\ \exists K_5\ \forall n,k\in\mathbb{N},\ K_5<k,\ k^2\le C n\lfloor\log_2 k\rfloor,\ n<k^2,\ \forall \sigma\in[0,1]:\quad \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}}\ [\{n/p\}<\sigma]\,\log p \;-\; \sigma \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p\Bigr| \le \delta k$

erdos-172openstatement unchecked

Whether every finite colouring of the natural numbers has arbitrarily large finite sets all of whose distinct-element sums and products share one colour.

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/172

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-172the problem's statementopen0 attemptsWork on this →

erdos-212openstatement unchecked

Is there a dense subset of ℝ^2 such that all pairwise distances are rational?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/212

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-212the problem's statementopen0 attemptsWork on this →

erdos-251openstatement unchecked

Is $\sum_{n=1}^\infty \frac{p_n}{2^n}$ irrational? Here $p_n$ is the $n$-th prime ($p_1=2, p_2=3, \dots$).

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/251

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-251the problem's statementopen0 attemptsWork on this →

erdos-257openstatement unchecked

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/257

ProvedExplainedWritten up Steward · Michael Higgins self-admitted 69 files need words View problem →

erdos-257the problem's statementopen4 attemptsWork on this →

Show 41 more statements, 14 open

erdos-257--h1left open by a proof skeletonproved0 attemptsView proof →$0 \notin A,\ \sum_{a\in A} \frac{1}{2^a-1} = r \in \mathbb{Q} \implies \forall n \ge 1:\ n \in A \iff \frac{1}{2^n-1} \le r - \sum_{a \in A,\, a<n} \frac{1}{2^a-1}$

erdos-257--h18derived by the compileropen0 attemptsWork on this →$A \subseteq \mathbb{N} \text{ infinite} \Rightarrow A \in \mathcal{C}_1 \cup \cdots \cup \mathcal{C}_{15} \ \lor\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$

erdos-257--h2left open by a proof skeletonopen5 attemptsWork on this →$\forall\, r\in\mathbb{Q},\ \forall\, G\subseteq\mathbb{N}:\quad 0\notin G,\ \ \Bigl(\forall n\ge 1:\ n\in G \iff \frac{1}{2^n-1} \le r-\sum_{a\in G,\ a<n}\frac{1}{2^a-1}\Bigr),\ \ \sum_{a\in G}\frac{1}{2^a-1}=r \ \Longrightarrow\ G \text{ is finite}.$

erdos-257--h2--h1derived by the compileropen0 attemptsWork on this →$r \in \mathbb{Q},\ G = \{n \ge 1 : \tfrac{1}{2^n-1} \le r - \sum_{a \in G,\, a<n} \tfrac{1}{2^a-1}\} \Rightarrow G \text{ finite or } \{n \ge 1\} \setminus G \text{ finite}$

spec-137537c8 Opn.erdos_257_lambert_identityproposed by a contributorproved0 attemptsView proof →$\forall\, A \subseteq \mathbb{N}:\qquad \sum_{a\in A}\frac{1}{2^a-1} \;=\; \sum_{m\ge 1}\frac{f_A(m)}{2^m},\qquad f_A(m) = \#\{a \in A : a \mid m\}.$

spec-23b0fff0 Opn.erdos_257_lambert_tail_integralproposed by a contributoropen0 attemptsWork on this →$\forall\, A \subseteq \mathbb{N},\ p \in \mathbb{Z},\ q \ge 1:\qquad \sum_{a\in A}\frac{1}{2^a-1} = \frac{p}{q}\ \Longrightarrow\ \forall j \ge 0:\quad q\,T_j \;=\; p\,2^{j} - q\sum_{m=0}^{j} f_A(m)\,2^{\,j-m},$

spec-5e2e0890 Opn.erdos_257_subsum_injectiveproposed by a contributorproved1 attemptView proof →$A, B \subseteq \mathbb{N},\quad 0 \notin A,\quad 0 \notin B,\quad \sum_{n\in A}\frac{1}{2^n-1} \;=\; \sum_{n\in B}\frac{1}{2^n-1} \quad\Longrightarrow\quad A = B .$

spec-5e2e0890--h1 spec_5e2e0890__h1derived by the compilerproved0 attemptsView proof →$\sum_{m \ge 0} \frac{1}{2^m - 1} < \infty \text{ (with Lean's convention } 1/0 = 0 \text{ at } m = 0)$

spec-5e2e0890--h2 spec_5e2e0890__h2derived by the compilerproved0 attemptsView proof →$g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$

spec-689ac1ac Opn.erdos_257_divisible_blockproposed by a contributoropen0 attemptsWork on this →

spec-a70fcca4 Opn.erdos_257_half_is_a_subsumproposed by a contributorsuperseded1 attemptBlocked

spec-a70fcca4--h1 spec_a70fcca4__h1derived by the compilerproved0 attemptsView proof →$\forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$

spec-a70fcca4--h2 spec_a70fcca4__h2derived by the compilerproved0 attemptsView proof →$\sum_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$

spec-a70fcca4--h3 spec_a70fcca4__h3derived by the compilerproved0 attemptsView proof →$\sum_{n\ge 0} \frac{1}{2^n-1} < \infty$

spec-a70fcca4--h4 spec_a70fcca4__h4derived by the compileropen3 attemptsWork on this →$\forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ r_m\le\sum_{k=0}^{\infty}\frac{1}{2^{k+m}-1}.$

spec-a70fcca4--h4--h1 spec_a70fcca4__h4__h1derived by the compileropen5 attemptsWork on this →$\forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ r_m<\frac{1}{2^m-1}\ \Rightarrow\ r_m\le\frac{1}{2^m}+\frac{1}{3\cdot 4^m}.$

spec-a70fcca4--h4--h1--h1 spec_a70fcca4__h4__h1__h1derived by the compileropen0 attemptsWork on this →$m \ge 2 \ \wedge\ r_m < \frac{1}{2^m-1} \ \Longrightarrow\ \exists n,\ m < n \le 2m \ \wedge\ r_n < \frac{1}{2^n-1}$

spec-a70fcca4--h4--h1--h2 spec_a70fcca4__h4__h1__h2derived by the compileropen0 attemptsWork on this →$m \ge 1 \ \wedge\ r_m < \frac{1}{2^m-1} \ \Longrightarrow\ \exists n,\ m < n \le 3m+2 \ \wedge\ r_n < \frac{1}{2^n-1}$

spec-a70fcca4-v2 Opn.erdos_257_half_is_a_subsuma variant that refutes the problemopen0 attemptsWork on this →$\exists\, A \subseteq \mathbb{N}\ \text{infinite with}\ \sum_{n\in A}\frac{1}{2^n-1} \;=\; \frac12 .$

spec-ddd99827 Opn.erdos_257_tail_lt_termproposed by a contributorproved0 attemptsView proof →$\sum_{k=0}^{\infty} \frac{1}{2^{\,n+1+k}-1} \;<\; \frac{1}{2^{n}-1} \qquad \text{for every integer } n \ge 1 .$

variant-037e597da partial route to the problemproved0 attemptsView proof →$\sum_{n \in \{2^k : k \in \mathbb{N}\} \cup \{3^k : k \in \mathbb{N}\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-1629563fa partial route to the problemproved0 attemptsView proof →$\forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \Bigl(\forall C \in \mathbb{N}\ \exists m \in A\ \exists L \in \mathbb{N}:\ L > 0,\ \bigl(\forall a \in A,\ a < m \Rightarrow (2^a - 1) \mid L\bigr),\ 2^C L \le 2^m\Bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-2a349f4fa related variantproved0 attemptsView proof →$C = \Bigl\{\, \sum_{n \in A} \frac{1}{2^n - 1} \;:\; A \subseteq \mathbb{N} \,\Bigr\} \subseteq \mathbb{R}\ \text{ is compact and perfect, and } \operatorname{int} C = \emptyset .$

variant-2f5236aaa partial route to the problemproved0 attemptsView proof →$\sum_{n=0}^{\infty}\frac{1}{2^n-1} \ \text{ is irrational}.$

variant-41d1f19ba partial route to the problemproved0 attemptsView proof →$\forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \Bigl(\forall C \in \mathbb{N}\ \exists m \in A:\ C + \sum_{a \in A,\ a < m} a \le m\Bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-5274cf38a partial route to the problemproved2 attemptsView proof →$\forall\, A \subseteq \mathbb{N} \text{ infinite}:\quad \bigl(\exists\, p \ge 1,\ N:\ \forall n \ge N,\ n \in A \iff n + p \in A\bigr) \ \Longrightarrow\ \sum_{n\in A}\frac{1}{2^n-1} \ \text{ is irrational}.$

variant-5274cf38--h1derived by the compileropen2 attemptsWork on this →$\forall B \subseteq \mathbb{N},\ \bigl(B \neq \emptyset \wedge \exists p \ge 1\ \forall n,\ (n \in B \iff n + p \in B)\bigr) \Rightarrow \sum_{n \in B} \frac{1}{2^n - 1} \notin \mathbb{Q}$

variant-5c939e77a related variantproved0 attemptsView proof →$\Bigl\{\, A \subseteq \mathbb{N} \ :\ 0 \notin A,\ \ \sum_{n\in A}\frac{1}{2^n-1} \in \mathbb{Q} \,\Bigr\} \ \text{ is countable}.$

variant-6b364d2ba partial route to the problemopen3 attemptsWork on this →$\sum_{p \text{ prime}}\frac{1}{2^p-1} \ \text{ is irrational}.$

variant-6b364d2b--h1derived by the compileropen2 attemptsWork on this →$\forall q \ge 1\ \exists c_0 > 0\ \forall \delta > 0:\ \text{a prime cube } p_\varepsilon = p_0 + \textstyle\sum_k \varepsilon_k v_k, \text{ a finite set of } n \text{ obeying (5.5)--(5.6), a split } S_0 \sqcup S_1 \sqcup S_2 \text{ of the primes} \le B \text{ with } X_p \text{ constant on } S_0,\ |X_p| \le \delta \text{ on } S_1,\ M \text{ even},\ \kappa_1, \dots, \kappa_5 \le \delta,\ \sum_{p \in S_1} \operatorname{Var} X_p \ge c_0$

variant-6b364d2b--h1--h1derived by the compileropen0 attemptsWork on this →$\forall q \ge 1,\ T,\ \delta > 0,\ P_0\ \ \exists P \ge P_0,\ 2^K \le (\log P)^{2/3},\ H \le (\log P)^{2/3}\ \ \forall (p_0, v)\ \ \exists (N_s, S_1, S_2, M, \eta, w, R):\ \kappa_2, \kappa_3, \kappa_4, \kappa_5 \le \delta,\ \sum_{\varepsilon} \frac{1+\eta}{p_\varepsilon} \le \delta,\ \frac{q}{2^{K+1}} \le \delta,\ 2^K T \le \log\log R - \log\log w$

variant-77c0756ea partial route to the problemproved0 attemptsView proof →$\forall\, x, y : \mathbb{N} \to \mathbb{N},\quad \Big(x_0, y_0 > 0,\ \ x_j \mid x_{j+1},\ y_j \mid y_{j+1},\ 3x_j \le x_{j+1},\ 3y_j \le y_{j+1}\ \text{for all } j\Big) \;\Longrightarrow\; \sum_{n \in \{x_j\} \cup \{y_j\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-7a0f5735a partial route to the problemproved0 attemptsView proof →$\forall\, k \ge 1:\qquad \sum_{m \in \{n^k \,:\, n \in \mathbb{N}\}} \frac{1}{2^m-1} \ \text{ is irrational}.$

variant-886b66daa partial route to the problemproved0 attemptsView proof →$\forall\, a, d \in \mathbb{N},\ d \ge 1:\qquad \sum_{m \in \{a + dn \,:\, n \ge 0\}} \frac{1}{2^m-1} \ \text{ is irrational}.$

variant-90827f46a partial route to the problemproved0 attemptsView proof →$\forall\, r \ge 1,\ \forall\, c_0, \dots, c_{r-1} : \mathbb{N} \to \mathbb{N},\quad \Big(c_i(0) > 0,\ \ (2r+1)^{r+1}\, c_i(j) \le c_i(j+1)\ \text{for all } i, j\Big) \;\Longrightarrow\; \sum_{n \in \bigcup_i \{c_i(j) : j \in \mathbb{N}\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-970a2ffaa partial route to the problemproved0 attemptsView proof →$\sum_{n \ \text{squarefree}} \frac{1}{2^n-1} \ \text{ is irrational}.$

variant-c91009b9a partial route to the problemproved0 attemptsView proof →$\forall\, A \subseteq \mathbb{N} \text{ infinite, pairwise coprime, with } \sum_{n\in A}\frac1n < \infty:\qquad \sum_{n\in A}\frac{1}{2^n-1} \ \text{ is irrational}.$

variant-d08712d9a partial route to the problemproved0 attemptsView proof →$\sum_{m \,\in\, \{a^2+b^2 \,:\, a,\, b \in \mathbb{N}\}} \frac{1}{2^m-1} \ \text{ is irrational}.$

variant-d144ccc1a partial route to the problemproved0 attemptsView proof →$\forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \bigl(\exists N\ \forall m, n \in A:\ N \le n < m \Rightarrow 2n \le m\bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-f93b89d8a partial route to the problemproved0 attemptsView proof →$\forall\, a, b \in \mathbb{N},\quad 2 \le a < b \;\Longrightarrow\; \sum_{n \in \{a^k : k \in \mathbb{N}\} \cup \{b^k : k \in \mathbb{N}\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

variant-f9c7b81ba related variantproved0 attemptsView proof →$\lambda\left(\left\{\, \sum_{n \in A} \frac{1}{2^n - 1} \;:\; A \subseteq \mathbb{N} \,\right\}\right) = 1$

erdos-324openstatement unchecked

Does there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/324

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-324the problem's statementopen0 attemptsWork on this →

erdos-376openstatement unchecked

Whether infinitely many n have the central binomial coefficient C(2n, n) coprime to 105.

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/376

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-376the problem's statementopen1 attemptWork on this →

erdos-402openstatement unchecked

Prove that, for any finite set $A\subset\mathbb{N}$, there exist $a, b\in A$ such that $$ \gcd(a, b)\leq a/|A|. $$

Statement from formal-conjectures (FormalConjectures/ErdosProblems/402.lean) · erdosproblems.com/402; the record lists no licensed source text.

ProvedExplainedWritten up Calibration target, no steward needed 91 files need words View problem →

erdos-402the problem's statementopen2 attemptsWork on this →

Show 35 more statements, 7 open

erdos-402--h1derived by the compilerproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite},\ \forall m \in \mathbb{N}:\ 0 \notin A,\ \bigl(\forall a, b \in A,\ a \le m \cdot \gcd(a,b)\bigr) \Rightarrow \forall a, b \in A\ \exists\, u, v \in \mathbb{N}:\ 0 < u \le m,\ 0 < v \le m,\ \gcd(u,v) = 1,\ a v = b u$

erdos-402--h2derived by the compilersuperseded0 attemptsBlocked$\Bigl(\forall B \subset \mathbb{N}\ \text{finite}:\ 0 \notin B,\ |B| = |A|,\ \gcd(B) = 1 \Rightarrow \exists\, a, b \in B:\ \gcd(a,b) \le \bigl\lfloor \tfrac{a}{|B|} \bigr\rfloor\Bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \Bigl\lfloor \frac{a}{|A|} \Bigr\rfloor$

erdos-402--h2-v2derived by the compilerproved0 attemptsView proof →$\Bigl(\forall B \subset \mathbb{N}\ \text{finite}:\ 0 \notin B,\ |B| = |A|,\ \gcd(B) = 1 \Rightarrow \exists\, a, b \in B:\ \gcd(a,b) \le \tfrac{a}{|B|}\Bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

erdos-402--h3derived by the compilersuperseded0 attemptsBlocked$0 \notin A,\ A \ne \emptyset,\ \gcd(A) = 1,\ \bigl(\forall a, b \in A\ \exists\, u, v:\ 0 < u \le |A|,\ 0 < v \le |A|,\ \gcd(u,v) = 1,\ a v = b u\bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \Bigl\lfloor \frac{a}{|A|} \Bigr\rfloor$

erdos-402--h3-v2derived by the compileropen1 attemptWork on this →$0 \notin A,\ A \ne \emptyset,\ \gcd(A) = 1,\ \bigl(\forall a, b \in A\ \exists\, u, v:\ 0 < u \le |A|,\ 0 < v \le |A|,\ \gcd(u,v) = 1,\ a v = b u\bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

erdos-402--h3-v2--h1derived by the compileropen1 attemptWork on this →$\begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\end{aligned}$

erdos-402--h3-v2--h1--h1derived by the compileropen1 attemptWork on this →$\begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \bigl(\exists\, p\ \text{prime}:\ |B| \le 2p,\ \exists\, a \in B,\ p \mid a\bigr)\end{aligned}$

erdos-402--h3-v2--h1--h1--h1derived by the compileropen2 attemptsWork on this →$\begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \bigl(\exists\, p\ \text{prime}:\ |B| \le 3p,\ \exists\, a \in B,\ p \mid a\bigr)\end{aligned}$

erdos-402--h3-v2--h1--h1--h1--h1derived by the compileropen0 attemptsWork on this →$\begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \bigl(\exists\, p\ \text{prime}:\ |B| < p < 2|B|,\ (2|B| - p)(2|B| - p) \le |B|\bigr)\end{aligned}$

erdos-402--h3-v2--h1--h1--h1--h2derived by the compileropen1 attemptWork on this →$n = |B|:\quad \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \Bigl(\exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)\Bigr)$

erdos-402--h3-v2--h1--h1--h1--h2--h1derived by the compilerproved0 attemptsView proof →$\forall n \in \mathbb{N},\ 10 \le n \le 228:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$

erdos-402--h3-v2--h1--h1--h1--h2--h2derived by the compilerproved0 attemptsView proof →$\forall n \in \mathbb{N},\ 229 \le n \le 200014:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$

erdos-402--h3-v2--h1--h1--h1--h2--h3derived by the compileropen0 attemptsWork on this →$n = |B| > 200014:\quad \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \Bigl(\exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)\Bigr)$

spec-48bd0126 Opn.erdos_402_max_fraction_formproposed by a contributorproved0 attemptsView proof →$\forall n \in \mathbb{N},\ \forall A \subset \mathbb{N}\ \text{finite}\ \text{nonempty},\ M = \max A:\ 0 \notin A,\ \bigl(\forall x \in A,\ M < \gcd(M, x) \cdot n\bigr) \Rightarrow \forall x \in A \setminus \{M\}\ \exists\, j, k \in \mathbb{N}:\ 1 \le j < k < n,\ k x = j M$

spec-fa8046e4 Opn.erdos_402_card_of_colouringproposed by a contributorproved0 attemptsView proof →$\begin{aligned}&n \ge 2,\ L > 0,\ S \subset \mathbb{N}\ \text{finite},\ c : \mathbb{N} \to \mathbb{N},\\&\forall k < n,\ \forall j < k,\ j > 0:\ k \mid L j\ \wedge\ L j / k \in S,\qquad \forall a \in S:\ c(a) + 2 < n,\\&\forall a, b \in S,\ a \ne b,\ c(a) = c(b):\ n \cdot \gcd(a,b) \le a\ \vee\ n \cdot \gcd(a,b) \le b\\&\Longrightarrow\ \forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = n \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}\end{aligned}$

variant-11152e83a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 12 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-29101bbca partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 25 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-3377fd96a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A \Rightarrow \forall x \in A,\ |A| \le \operatorname{minFac}(x) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-4ad214d0definitionproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 15 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-64035064a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 16 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-6bb50ad7a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 8 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-6bd06d63a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 3 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-77918742a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ A \ne \emptyset,\ |A| \le 24 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-780e7adea partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 4 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-7a4bb0cda partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 11 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-892f5809a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 9 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-950630b9a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ \bigl(\exists\, m \in A,\ \exists\, b \in A:\ (\forall c \in A,\ c \le m) \wedge \gcd(m, b) = 1\bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-9724698ea partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 13 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-a3b3cb8fa partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 7 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-a5969ff3a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 10 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-a874fe93a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A \Rightarrow \forall p \in A,\ p\ \text{prime},\ |A| \le p \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-b89de5c4a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 18 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-bc28297ca partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 5 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-d865c9c6a partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 2 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

variant-e6d83e6da partial route to the problemproved0 attemptsView proof →$\forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 6 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

erdos-406openstatement unchecked

Whether only finitely many powers of two have base-three expansions using only the digits 0 and 1.

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/406

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-406the problem's statementopen0 attemptsWork on this →

erdos-410openstatement unchecked

Let $σ_1(n) = σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$. Is it true that $\lim_{k → ∞} σ_k(n)^{\frac 1 k} = ∞$? This is problem (iii) from Erdos, Granville, Pomerance, Spiro "On the normal behavior of the iterates of some arithmetical functions" (page 169 of the book "Analytic Number Theory", 1990).

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/410

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-410the problem's statementopen0 attemptsWork on this →

erdos-412openstatement unchecked

Let $σ_1(n)=σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$. Is it true that, for every $m, n ≥ 2$, there exist some $i, j$ such that $σ_i(m) = σ_j(n)$?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/412

ProvedExplainedWritten up Needs a steward 4 files need words View problem →

erdos-412the problem's statementopen1 attemptWork on this →

Show 2 more statements, 1 open

erdos-412--h1left open by a proof skeletonsuperseded0 attemptsBlocked$\forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$

erdos-412--h1-v2left open by a proof skeletonneeds a witness0 attemptsSupply a witness →$\forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$

erdos-417openstatement unchecked

Let$$V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$$and$$V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$$ Does $\lim V(x)/V'(x)$ exist?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/417

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-417the problem's statementopen0 attemptsWork on this →

erdos-51openstatement unchecked

Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac{n_a}{a} → \infty$ as $a → ∞$?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/51

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-51the problem's statementopen0 attemptsWork on this →

erdos-52openstatement unchecked

Whether for every ε>0 a finite set of integers has either its sumset or its product set of size at least a constant times |A|^(2−ε).

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/52

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-52the problem's statementopen0 attemptsWork on this →

erdos-68openstatement unchecked

Whether the series summing 1/(n!-1) over n at least 2 has an irrational value.

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/68

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-68the problem's statementopen0 attemptsWork on this →

erdos-69openstatement unchecked

Is $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} $$ irrational? (Here $\omega(n)$ counts the number of distinct prime divisors of $n$.)

Statement from formal-conjectures (FormalConjectures/ErdosProblems/69.lean) · erdosproblems.com/69; the record lists no licensed source text.

ProvedExplainedWritten up Calibration target, no steward needed 46 files need words View problem →

erdos-69the problem's statementopen2 attemptsWork on this →

Show 22 more statements, 3 open

erdos-69--h1left open by a proof skeletonsuperseded0 attemptsBlocked$\sum_{n=0}^{\infty}\frac{\uparrow\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{\uparrow p}-1}$

erdos-69--h1-v2left open by a proof skeletonproved0 attemptsView proof →$\sum_{n=0}^{\infty}\frac{\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}$

erdos-69--h2left open by a proof skeletonsuperseded0 attemptsBlocked$\Bigl(\sum_{n=0}^{\infty}\frac{\uparrow\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{\uparrow p}-1}\Bigr) \;\Rightarrow\; \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\notin\mathbb{Q}$

erdos-69--h2-v2left open by a proof skeletonopen1 attemptWork on this →$\Bigl(\sum_{n=0}^{\infty}\frac{\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\Bigr) \;\Rightarrow\; \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\notin\mathbb{Q}$

erdos-69--h2-v2--h1derived by the compilersuperseded0 attemptsBlocked$\Bigl(\sum_{n=0}^{\infty}\frac{\uparrow\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{\uparrow p}-1}\Bigr) \Rightarrow \forall b\in\mathbb{N},\ b>0\ \ \exists N\in\mathbb{N}\ \ \forall z\in\mathbb{Z}:\ \uparrow b\cdot\sum_{j=0}^{\infty}\frac{\uparrow\omega(N+1+j)}{2^{j+1}} \ne \uparrow z$

erdos-69--h2-v2--h1-v2derived by the compileropen2 attemptsWork on this →$\Bigl(\sum_{n=0}^{\infty}\frac{\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\Bigr) \Rightarrow \forall b\in\mathbb{N},\ b>0\ \ \exists N\in\mathbb{N}\ \ \forall z\in\mathbb{Z}:\ b\cdot\sum_{j=0}^{\infty}\frac{\omega(N+1+j)}{2^{j+1}} \ne z$

erdos-69--h2-v2--h1-v2--h1left open by a proof skeletonproved0 attemptsView proof →$\forall N,k\in\mathbb{N}:\quad \sum_{j=0}^{\infty}\frac{\omega(N+1+j)}{2^{j+1}} = \sum_{j=0}^{k-1}\frac{\omega(N+1+j)}{2^{j+1}} + \frac{1}{2^{k}}\sum_{j=0}^{\infty}\frac{\omega(N+k+1+j)}{2^{j+1}}$

erdos-69--h2-v2--h1-v2--h2left open by a proof skeletonproved0 attemptsView proof →$\forall M\in\mathbb{N}:\quad 0 < \sum_{j=0}^{\infty}\frac{\omega(M+1+j)}{2^{j+1}}$

erdos-69--h2-v2--h1-v2--h3left open by a proof skeletonproved0 attemptsView proof →$\forall M\in\mathbb{N}:\quad \sum_{j=0}^{\infty}\frac{\omega(M+1+j)}{2^{j+1}} \le \log_{2}(M+1) + 1$

erdos-69--h2-v2--h1-v2--h4left open by a proof skeletonopen1 attemptWork on this →$\forall b\in\mathbb{N},\ b>0\ \ \exists N,k\in\mathbb{N}:\quad \Bigl(b\sum_{j=0}^{k-1}\omega(N+1+j)\,2^{\,k-1-j}\Bigr)\bmod 2^{k} \;+\; b\bigl(\log_{2}(N+k+1)+1\bigr) < 2^{k}$

spec-13f68833 Opn.erdos_69_tail_le_of_linear_boundproposed by a contributorproved0 attemptsView proof →$\forall n\in\mathbb{N},\ C\in\mathbb{R}:\quad \Bigl(\forall k\in\mathbb{N},\ \omega(n+1+k) \le C\,(k+1)\Bigr) \Rightarrow \sum_{j=0}^{\infty}\frac{\omega(n+1+j)}{2^{j+1}} \le 2C$

spec-2e765953 Opn.erdos_69_summable_prime_reciprocalproposed by a contributorproved0 attemptsView proof →$\sum_{p\ \text{prime}}\frac{1}{2^{p}-1} < \infty$

spec-7d098d5c Opn.erdos_69_mertens_reciprocal_primesproposed by a contributorproved0 attemptsView proof →$\exists C\ge 0\ \ \forall x\in\mathbb{N},\ x\ge 2:\quad \Bigl\lvert \sum_{p\le x,\ p\ \text{prime}}\frac{1}{p} - \log\log x \Bigr\rvert \le C$

spec-7f0efe19 Opn.erdos_69_omega_windowproposed by a contributorproved0 attemptsView proof →$\forall k\in\mathbb{N},\ \forall c:\mathbb{N}\to\mathbb{N}\ \ \exists N\in\mathbb{N}\ \ \forall j<k:\quad c(j) \le \omega(N+1+j)$

spec-84446025 Opn.erdos_69_rational_dilated_tails_near_integersproposed by a contributorproved0 attemptsView proof →$\frac{1}{T}\sum_{t=0}^{T-1}\Bigl\lvert q\,D_a(b+Qt) - \operatorname{round}\bigl(q\,D_a(b+Qt)\bigr)\Bigr\rvert \le q\sum_{p\mid a}\Bigl(\frac{1}{p}+\frac{1}{T}\Bigr),\qquad D_a(m) = \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}}$

spec-9f8cb4ea Opn.erdos_69_dilated_tail_closedproposed by a contributorproved0 attemptsView proof →$\forall a,m\in\mathbb{N},\ a\ne 0:\quad \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}} = \sum_{k=0}^{\infty}\frac{\omega(m+k+1)}{2^{k+1}} + \omega(a) - \sum_{p\mid a}\frac{2^{\,m \bmod p}}{2^{p}-1}$

spec-c390279b Opn.erdos_69_rational_tails_periodicproposed by a contributorproved0 attemptsView proof →$\exists p>0,\ N_0\ \ \forall n,n'\ge N_0,\ n\equiv n' \pmod p\ \ \exists z\in\mathbb{Z}:\quad \sum_{j=0}^{\infty}\frac{f(n+1+j)}{2^{j+1}} - \sum_{j=0}^{\infty}\frac{f(n'+1+j)}{2^{j+1}} = z$

spec-e0b917d1 Opn.erdos_69_rough_dilation_reciprocalproposed by a contributorproved0 attemptsView proof →$\forall P,j\in\mathbb{N},\ 2\le P,\ j\le P:\quad \sum_{p\mid 1+P\#\,(1+j)}\frac{1}{p} \le \frac{5}{\log P}$

variant-09e95e7aa related variantproved0 attemptsView proof →$\sum_{n=0}^{\infty}\bigl[n\ \text{prime}\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

variant-14c6c771a related variantproved0 attemptsView proof →$\forall m\in\mathbb{N},\ m\ge 1:\quad \sum_{n=0}^{\infty}\bigl[\omega(n)=m\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

variant-3a1bcb9aa related variantproved0 attemptsView proof →$\sum_{n=0}^{\infty}\frac{\omega(n)}{n!} \notin\mathbb{Q}$

variant-f592e3aba related variantproved0 attemptsView proof →$\forall b\in\mathbb{N},\ b\ge 2:\quad \sum_{p\ \text{prime}}\frac{1}{b^{p}} \notin\mathbb{Q}$

erdos-727openstatement unchecked

Let $k ≥ 2$. Does $((n+k)!)^2∣(2n)!$ hold for infinitely many $n$?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/727

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-727the problem's statementopen0 attemptsWork on this →

erdos-849openstatement unchecked

Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/849

ProvedExplainedWritten up Steward · WilliamVerreault self-admitted 16 files need words View problem →

erdos-849the problem's statementopen0 attemptsWork on this →

Show 6 more statements, 6 open

spec-12191c69 Opn.erdos_849_rows_eq_pairsproposed by a contributoropen0 attemptsWork on this →

spec-38faff03 Opn.erdos_849_rows_leproposed by a contributoropen0 attemptsWork on this →

variant-0691f5bba partial route to the problemopen0 attemptsWork on this →

variant-293c7f51a partial route to the problemopen0 attemptsWork on this →

variant-3d9db4a5a partial route to the problemopen0 attemptsWork on this →

variant-c9253839a partial route to the problemopen0 attemptsWork on this →

erdos-850openstatement unchecked

Can there exist two distinct integers $x$ and $y$ such that $x,y$ have the same prime factors, $x+1,y+1$ have the same prime factors, and $x+2,y+2$ also have the same prime factors?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/850

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-850the problem's statementopen0 attemptsWork on this →

erdos-931openstatement unchecked

Let $k_1 \geq k_2 \geq 3$. Are there only finitely many $n_2\geq n_1 + k_1$ such that $$ \prod_{1\leq i\leq k_1}(n_1 + i)\ \text{and}\ \prod_{1\leq j\leq k_2} (n_2 + j) $$ have the same prime factors?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/931

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-931the problem's statementopen0 attemptsWork on this →

erdos-952openstatement unchecked

Is there an infinite sequence of distinct Gaussian primes $x_1,x_2,\ldots$ such that $\lvert x_{n+1}-x_n\rvert \ll 1$?

Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/952

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

erdos-952the problem's statementopen0 attemptsWork on this →

euclid-primesprovedstatement unchecked

For every natural number n there is a prime greater than n.

Statement from Euclid, Elements IX.20; the record lists no licensed source text.

ProvedExplainedWritten up Steward wanted for write-up 29 files need words View the graph →

infinitude-of-primesthe problem's statementproved2 attemptsView proof →

Show 12 more statements

infinitude-of-primes--h1left open by a proof skeletonproved0 attemptsView proof →For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$.

infinitude-of-primes--h2left open by a proof skeletonproved0 attemptsView proof →The theorem infinitude_of_primes__h2 asserts the following.

infinitude-of-primes--h3left open by a proof skeletonproved0 attemptsView proof →$\forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\ \forall d,m\in\mathbb{N},\ d\mid m\ \wedge\ d\mid m+1\ \Rightarrow\ d=1$

infinitude-of-primes--h4left open by a proof skeletonproved0 attemptsView proof →$\forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\bigl(\forall d,m,\ d\mid m\wedge d\mid m+1\Rightarrow d=1\bigr)\Rightarrow\ \forall k\in\mathbb{N},\ 0<k!$

variant-2a7919a9a related variantproved1 attemptView proof →$\forall\, l\in\operatorname{List}(\mathbb{N})\ \ \exists p\in\mathbb{N}:\quad p\ \text{prime}\ \wedge\ p\notin l$

variant-2a7919a9--h1left open by a proof skeletonproved0 attemptsView proof →$\forall\, l\in\operatorname{List}(\mathbb{N}),\ \forall x\in l:\quad x\le \sum l$

variant-2a7919a9--h2left open by a proof skeletonproved0 attemptsView proof →$\forall\, l\in\operatorname{List}(\mathbb{N}):\quad \bigl(\forall x\in l,\ x\le \textstyle\sum l\bigr)\ \Rightarrow\ \exists p\in\mathbb{N},\ \textstyle\sum l<p\ \wedge\ p\ \text{prime}$

variant-4cb87a03a variant that resolves the problemproved0 attemptsView proof →$\forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\le n!+1\ \wedge\ p\ \text{prime}$

variant-6e71b160a related variantabandoned0 attemptsBlocked$\forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ \bigl(\exists k\in\mathbb{N},\ p=100+k\bigr)\ \wedge\ p\ \text{prime}$

variant-aceabdc4a related variantproved1 attemptView proof →$\forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ 100\le p\ \wedge\ p\ \text{prime}$

variant-dea95969a variant that resolves the problemproved0 attemptsView proof →$\forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\ \text{prime}\ \wedge\ p \bmod 4 = 3$

variant-f15ce396a variant that resolves the problemproved0 attemptsView proof →$\{\,p\in\mathbb{N}\ :\ p\ \text{prime}\,\}\ \text{is infinite}$

riemann-hypothesisopenstatement unchecked

The Riemann Hypothesis: all non-trivial zeros of the Riemann zeta function have real part $\frac{1}{2}$. That is, if $\zeta(s) = 0$, $s \neq 1$, and $s$ is not a trivial zero $-2(n+1)$ for some $n \in \mathbb{N}$, then $\operatorname{Re}(s) = \frac{1}{2}$. This is the official Millennium Prize Problem as posed by the Clay Mathematics Institute. This uses the RiemannHypothesis type from Mathlib, which is defined as ∀ (s : ℂ), riemannZeta s = 0 → (¬∃ n : ℕ, s = -2 * (n + 1)) → s ≠ 1 → s.re = 1 / 2.

Imported from formal-conjectures (Apache-2.0)

ProvedExplainedWritten up Needs a steward 1 file needs words View problem →

riemann-hypothesisthe problem's statementopen0 attemptsWork on this →

tutorialprovedstatement unchecked

No informal statement is recorded for this problem yet.

No curated record yet.

ProvedExplainedWritten up Steward wanted for write-up 7 files need words View the graph →

tutorial-and-swapthe tutorial statementproved0 attemptsView proof →

Show 3 more statements, 3 open

variant-93e79cb5a related variantopen1 attemptWork on this →$\forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ p$

variant-93e79cb5--h1left open by a proof skeletonneeds a witness0 attemptsSupply a witness →$\forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p$

variant-93e79cb5--h2left open by a proof skeletonneeds a witness0 attemptsSupply a witness →$\forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p\ \Rightarrow\ q\wedge p\ \Rightarrow\ p$