Questions, not proof records

Open-problem statements, with their sources attached.

Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.

“Open” is a dated source assertion. In these pinned sources, sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.
All topics

3 of 1194 statement records

17 source collections · 43 mathematical fields

Clear filters
Source labels openErdős Problems · Sequences and series

Erdős Problem 243

Let a1<a2<a_1 < a_2 < \dots be a sequence of integers such that limnanan12=1\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1 and 1anQ\sum \frac{1}{a_n} \in \mathbb{Q}.

Then, for all sufficiently large n1n \ge 1, an=an12an1+1a_n = a_{n-1}^2 - a_{n-1} + 1.

Source checked Jul 26, 20261 pinned Lean statementInspect problem
Source labels openWikipedia · Sequences and series

Convergence of the Flint Hills and Cookson Hills series

The Flint Hills series summing csc(n)2/n3csc(n)^2 / n^3 from n=1n=1 to \infty converges. (Note that we 0-index the series below.)

Source checked Jul 26, 20261 pinned Lean statementInspect problem
Source labels openWikipedia · Sequences and series

Convergence of the Flint Hills and Cookson Hills series

The Cookson Hills series summing sec(n)2/n3sec(n)^2 / n^3 from n=1n=1 to \infty converges.

Source checked Jul 26, 20261 pinned Lean statementInspect problem