994.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

3 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 994

References:

erdosproblems.com/994
[Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65.
[Kh23] Khintchine, A., Ein Satz über Kettenbrüche, mit arithmetischen Anwendungen. Math. Z. (1923), 289--306.
[Ma70] Marstrand, J. M., On Khinchin's conjecture about strong uniform distribution. Proc. London Math. Soc. (3) (1970), 540--556.

Imports (1)

FormalConjecturesUtil

def Erdos994.visitAverage The proportion $\frac{1}{n}\sum_{1\leq k\leq n}1_{\{k\alpha \}\in E}$ of the fractional parts $\{k\alpha\}$, $1\leq k\leq n$, which lie in E line 42 source
Source documentation
The proportion $\frac{1}{n}\sum_{1\leq k\leq n}1_{\{k\alpha \}\in E}$ of the fractional parts $\{k\alpha\}$, $1\leq k\leq n$, which lie in E.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real, Nat
Proof uses: HDiv.hDiv, Finset.sum, Finset.Icc, OfNat.ofNat, ite, Membership.mem, Int.fract, HMul.hMul, Classical.propDecidable
19 instances, coercions and auxiliary constants left out.
```
noncomputable def visitAverage (E : Set ℝ) (α : ℝ) (n : ℕ) : ℝ :=
…
```
theorem Erdos994.erdos_994 Let $E\subseteq (0,1)$ be a meaurable subset with Lebesgue measure $\lambda(E)$ sorry line 55 source
Source documentation
Let $E\subseteq (0,1)$ be a meaurable subset with Lebesgue measure $\lambda(E)$. Is it true that, for almost all $\alpha$, $$\lim_{n\to \infty}\frac{1}{n}\sum_{1\leq k\leq n}1_{\{k\alpha \}\in E}=\lambda(E)$$ for all $E$?
This is a conjecture of Khintchine [Kh23] (with the exceptional null set of $\alpha$ allowed to depend on $E$). It is false, and was disproved by Marstrand [Ma70].

depends on sorry what this means
Statement uses: Iff, False, Set, Real, LE.le, Set.Ioo, OfNat.ofNat, MeasurableSet, Filter.Eventually, Filter.Tendsto, Nat, Erdos994.visitAverage, Filter.atTop, nhds, ENNReal.toReal, MeasureTheory.Measure, ENNReal, MeasureTheory.MeasureSpace.volume, MeasureTheory.ae
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_994 : answer(False) ↔
    ∀ E ⊆ Ioo (0 : ℝ) 1, MeasurableSet E →
      ∀ᵐ α : ℝ, Tendsto (visitAverage E α) atTop (nhds (volume E).toReal) := by
…
```
Mentions: Erdos994.visitAverage
theorem Erdos994.erdos_994.variants.simultaneous Read literally, with "for almost all line 66 source
Source documentation
Read literally, with "for almost all $\alpha$" placed before "for all $E$", the statement is trivially false: for any $\alpha$, removing the countable orbit $\{\{k\alpha\} : k\geq 1\}$ from $(0,1)$ gives a measurable set of measure $1$ which is never visited.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Filter.Eventually, Real, Set, LE.le, Set.Ioo, OfNat.ofNat, MeasurableSet, Filter.Tendsto, Nat, Erdos994.visitAverage, Filter.atTop, nhds, ENNReal.toReal, MeasureTheory.Measure, ENNReal, MeasureTheory.MeasureSpace.volume, MeasureTheory.ae
Proof uses: Exists, False, Filter.Eventually.exists, Set.range, Int.fract, HMul.hMul, HAdd.hAdd, Eq, rfl, Set.Countable.measure_zero, Set.countable_range, SDiff.sdiff, Set.sdiff_subset, MeasurableSet.diff, measurableSet_Ioo, Set.Countable.measurableSet, Eq.mpr, id, congrArg, MeasureTheory.measure_sdiff_null and 33 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_994.variants.simultaneous :
    ¬ ∀ᵐ α : ℝ, ∀ E ⊆ Ioo (0 : ℝ) 1, MeasurableSet E →
      Tendsto (visitAverage E α) atTop (nhds (volume E).toReal) := by
…
```
Mentions: Erdos994.visitAverage