Erdős Problems

1,217 source-owned questions · 604 with a formal statement · searchable by statement, number, topic and source status.

Full distribution

Collection coverage

Source status, exact formal material, and reviewed Results are separate signals.

Exact formal statement available604 / 1,217

With Repository-reviewed evidence2 / 1,217

7 Problems

Number	Question	Source says	Formal	Result here
#495	Let $\alpha,\beta \in \mathbb{R}$ . Is it true that $\liminf_{n\to \infty} n \\| n\alpha \\| \\| n\beta\\| =0$ ? This is also known as the Littlewood conjecture.Source says openFormalized	open	In Lean	No Result decision
#496	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#998	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#999	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1000	Let $A=\{n_1<n_2<\cdots\}$ be an infinite sequence of integers, and let $\phi_A(k)$ count the number of $1\leq m\leq n_k$ such that the fraction $\frac{m}{n_k}$ does not have denominator $n_j$ for $j<k$ when written in lowest form; equivalently, $\frac{n_k}{(m,n_k)}\neq n_j$ for all $1\leq j<k$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1001	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1002	For any $0<\alpha<1$ , let $f(\alpha,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}- \{ \alpha k\})$ . Does $f(\alpha,n)$ have an asymptotic distribution function?Source says openFormalized	open	In Lean	No Result decision