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

9 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 521

Reference: erdosproblems.com/521

Imports (1)

FormalConjecturesUtil

def Erdos521.sign true encodes the sign +1, false the sign -1 line 34 source
Source documentation
true encodes the sign +1, false the sign -1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Real
Proof uses: ite, Eq, Bool.true, OfNat.ofNat, Neg.neg
4 instances, coercions and auxiliary constants left out.
```
def sign (b : Bool) : ℝ := if b then 1 else -1
```
def Erdos521.fairCoin One fair coin: the uniform probability measure on Bool line 37 source
Source documentation
One fair coin: the uniform probability measure on Bool.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.Measure, Bool
Proof uses: HSMul.hSMul, ENNReal, Inv.inv, OfNat.ofNat, HAdd.hAdd, MeasureTheory.Measure.dirac, Bool.true, Bool.false
18 instances, coercions and auxiliary constants left out.
```
noncomputable def fairCoin : Measure Bool :=
…
```
theorem Erdos521.fairCoin_apply fairCoin gives each of the two signs mass 1/2 line 44 source
Source documentation
fairCoin gives each of the two signs mass 1/2. Together with fairCoin_isProbabilityMeasure this pins the definition down, so a proof stating the same problem with a Bernoulli(1/2) measure is stating the same thing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Eq, ENNReal, MeasureTheory.Measure, Set, Erdos521.fairCoin, Singleton.singleton, Inv.inv, OfNat.ofNat, Nat
Proof uses: Bool.false, of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, HSMul.hSMul, MeasureTheory.Measure.dirac, Bool.true, smul_add, congr, Set.indicator, MeasureTheory.Measure.dirac_apply', MeasurableSet, Top.top, MeasurableSpace, Set.indicator_of_notMem, Not, Membership.mem and 12 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem fairCoin_apply (b : Bool) : fairCoin {b} = 2⁻¹ := by
…
```
Mentions: Erdos521.fairCoin
theorem Erdos521.fairCoin_isProbabilityMeasure fairCoin is a probability measure line 49 source
Source documentation
fairCoin is a probability measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.IsProbabilityMeasure, Bool, Erdos521.fairCoin
Proof uses: MeasureTheory.IsProbabilityMeasure.mk, Eq.mpr, Eq, ENNReal, MeasureTheory.Measure, Set, Set.univ, OfNat.ofNat, HAdd.hAdd, Inv.inv, id, congrFun', congrArg, Eq.trans, HSMul.hSMul, MeasureTheory.Measure.dirac, Bool.true, Bool.false, Insert.insert, Singleton.singleton and 23 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem fairCoin_isProbabilityMeasure : IsProbabilityMeasure fairCoin := by
…
```
Mentions: Erdos521.fairCoin
def Erdos521.rademacherMeasure The law of an infinite sequence of independent fair coins (ε_k)_{k ≥ 0}, each uniform on {-1, +1} line 56 source
Source documentation
The law of an infinite sequence of independent fair coins (ε_k)_{k ≥ 0}, each uniform on {-1, +1}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.Measure, Nat, Bool
Proof uses: MeasureTheory.Measure.infinitePi, Erdos521.fairCoin
3 instances, coercions and auxiliary constants left out.
```
noncomputable def rademacherMeasure : Measure (ℕ → Bool) :=
…
```
def Erdos521.littlewoodPolynomial The degree-n Littlewood polynomial f_n(z) = ∑_{0 ≤ k ≤ n} ε_k z^k line 60 source
Source documentation
The degree-n Littlewood polynomial f_n(z) = ∑_{0 ≤ k ≤ n} ε_k z^k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Polynomial, Real
Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, LinearMap, RingHom.id, Polynomial.monomial, Erdos521.sign
12 instances, coercions and auxiliary constants left out.
```
noncomputable def littlewoodPolynomial (ω : ℕ → Bool) (n : ℕ) : ℝ[X] :=
…
```
def Erdos521.realRootCount R_n: the number of distinct real roots of f_n line 64 source
Source documentation
R_n: the number of distinct real roots of f_n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool
Proof uses: Set.ncard, Real, Polynomial.rootSet, Erdos521.littlewoodPolynomial
4 instances, coercions and auxiliary constants left out.
```
noncomputable def realRootCount (ω : ℕ → Bool) (n : ℕ) : ℕ :=
…
```
def Erdos521.Claim The assertion asked about in Problem 521: almost surely R_n / log n → 2/π line 68 source
Source documentation
The assertion asked about in Problem 521: almost surely R_n / log n → 2/π.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Filter.Eventually, Nat, Bool, Filter.Tendsto, Real, HDiv.hDiv, Erdos521.realRootCount, Real.log, Filter.atTop, nhds, OfNat.ofNat, Real.pi, MeasureTheory.ae, MeasureTheory.Measure, Erdos521.rademacherMeasure
15 instances, coercions and auxiliary constants left out.
```
def Claim : Prop :=
…
```
theorem Erdos521.erdos_521 Let $(\epsilon_k)_{k\geq 0}$ be independently uniformly chosen at random from $\{-1,1\}$ sorry line 84 source
Source documentation
Let $(\epsilon_k)_{k\geq 0}$ be independently uniformly chosen at random from $\{-1,1\}$. If $R_n$ counts the number of real roots of $f_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k$ then is it true that, almost surely, $$\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?$$
The answer is no: this almost-sure limit fails. This result was obtained first by others, who deserve the credit for the problem; the link is to an independent machine-checked proof by Star Fleet Math.

depends on sorry what this means
Statement uses: Iff, False, Erdos521.Claim
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_521 : answer(False) ↔ Claim := by
…
```
Mentions: Erdos521.Claim