464.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 464

References:

erdosproblems.com/464
[Er75i] Erdős, P., Répartition modulo $1$. (1975), iv+258.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980).
[Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79.
[AkMo04] Akhunzhanov, R. K. and Moshchevitin, N. G., On the chromatic number of a distance graph associated with a lacunary sequence. Dokl. Akad. Nauk (2004), 295-296.
[Du06] Dubickas, Artūras, On the fractional parts of lacunary sequences. Math. Scand. (2006), 136-146.
[Ka01] Katznelson, Y., Chromatic numbers of Cayley graphs on $\mathbb{Z}$ and recurrence. Combinatorica (2001), 211-219.
[PeSc10] Peres, Yuval and Schlag, Wilhelm, Two Erdős problems on lacunary sequences: chromatic number and Diophantine approximation. Bull. Lond. Math. Soc. (2010), 295-300.
[Po79b] Pollington, A. D., On the density of sequence $\{n_k\xi\}$. Illinois J. Math. (1979), 511-515.
[dM80] de Mathan, B., Numbers contravening a condition in density modulo $1$. Acta Math. Acad. Sci. Hungar. (1980), 237-241 (1981).

Imports (1)

FormalConjecturesUtil

theorem Erdos464.erdos_464 Let $A=\{n_10$ with $n_{k+1}\geq (1+\epsilon)n_k$ for all $k$) sorry line 84 source
Source documentation
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)?
Solved independently by de Mathan [dM80] and Pollington [Po79b], who showed that, given any such $A$, there exists such a $\theta$, with $$\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon^4}{\log(1/\epsilon)}.$$ This bound was improved by Katznelson [Ka01], Akhunzhanov and Moshchevitin [AkMo04], and Dubickas [Du06], before Peres and Schlag [PeSc10] improved it to $$\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon}{\log(1/\epsilon)},$$ and note that the best bound possible here would be $\gg \epsilon$.
This problem has consequences for 894.
The conclusion "$\{\|\theta n_k\|\}$ is not dense in $[0,1]$" is formalized as the sequence $(\theta n_k)$ not being dense modulo one; see the formalization notes above.

L4DEL explanation
Let $A=\{n_10$ 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)? Solved independently by de Mathan [dM80] and Pollington [Po79b], who showed that, given any such $A$, there exists such a $\theta$, with $$\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon^4}{\log(1/\epsilon)}.$$ This bound was improved by Katznelson [Ka01], Akhunzhanov and Moshchevitin [AkMo04], and Dubickas [Du06], before Peres and Schlag [PeSc10] improved it to $$\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon}{\log(1/\epsilon)},$$ and note that the best bound possible here would be $\gg \epsilon$. This problem has consequences for 894. The conclusion "$\{\|\theta n_k\|\}$ is not dense in $[0,1]$" is formalized as the sequence $(\theta n_k)$ not being dense modulo one; see the formalization notes above.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Nat, StrictMono, LT.lt, OfNat.ofNat, IsLacunary, Exists, Real, And, Irrational, Not, Dense, HasQuotient.Quotient, AddSubgroup, AddSubgroup.zmultiples, Set.range, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_464 : answer(True) ↔
    ∀ n : ℕ → ℕ, StrictMono n → (∀ k, 0 < n k) → IsLacunary n →
      ∃ θ : ℝ, Irrational θ ∧
        ¬ Dense (Set.range fun k => (↑(θ * n k) : AddCircle (1 : ℝ))) := by
…
```
Mentions: IsLacunary