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

19 declarations, 9 contain sorry, 0 declared as axioms

Ben Green's Open Problem 40

References:

[Gr24] Ben Green's Open Problem 40
[Da90] Davydov, Alexander Abramovich. "Construction of linear covering codes." Problemy Peredachi Informatsii 26.4 (1990): 38-55.
[CHL97] Cohen, G., Honkala, I., Litsyn, S., & Lobstein, A. (1997). Covering codes (Vol. 54). Elsevier.
[St94] R. Struik, Covering codes, PhD Thesis, Eindhoven University of Technology, the Netherlands, 106 pp, 1994.

Imports (1)

FormalConjecturesUtil

def Green40.hammingBall The Hamming ball of radius $r$ in $\mathbb{F}_2^n$ line 41 source
Source documentation
The Hamming ball of radius $r$ in $\mathbb{F}_2^n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, 𝔽₂
Proof uses: Set.ofPred, LE.le, hammingNorm, Fin, ZMod, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
```
def hammingBall (n r : ℕ) : Set (𝔽₂ n) :=
…
```
Mentions: 𝔽₂
def Green40.IsCoveringSubspace $V$ is a covering subspace of $\mathbb{F}_2^n$ by $H(r)$ if $V + H(r) = \mathbb{F}_2^n$ line 45 source
Source documentation
$V$ is a covering subspace of $\mathbb{F}_2^n$ by $H(r)$ if $V + H(r) = \mathbb{F}_2^n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Submodule, ZMod, OfNat.ofNat, 𝔽₂, Fin
Proof uses: Eq, Set, HAdd.hAdd, Green40.hammingBall, Set.univ
27 instances, coercions and auxiliary constants left out.
```
def IsCoveringSubspace (n r : ℕ) (V : Submodule (ZMod 2) (𝔽₂ n)) : Prop :=
…
```
Mentions: 𝔽₂
def Green40.minDensity The minimal covering density over all covering subspaces for a given n and r line 50 source
Source documentation
The minimal covering density over all covering subspaces for a given n and r. We compute in ℝ≥0∞ (ENNReal) to gracefully handle any potential divergence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ENNReal
Proof uses: iInf, Submodule, ZMod, OfNat.ofNat, 𝔽₂, Fin, Green40.IsCoveringSubspace, HDiv.hDiv, HMul.hMul, Nat.card, Subtype, Membership.mem, Green40.hammingBall, HPow.hPow
38 instances, coercions and auxiliary constants left out.
```
noncomputable def minDensity (n r : ℕ) : ℝ≥0∞ :=
…
```
def Green40.f Documented declaration: f line 59 source
Source documentation
Let $f(r)$ be the smallest constant such that there exists an infinite sequence of $n$'s together with subspaces $V_n \leq \mathbb{F}_2^n$ with $V_n + H(r) = \mathbb{F}_2^n$ and $|V_n| = \left(f(r) + o(1)\right) \frac{2^n}{|H(r)|}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ENNReal
Proof uses: Filter.liminf, Green40.minDensity, Filter.atTop
5 instances, coercions and auxiliary constants left out.
```
noncomputable def f (r : ℕ) : ℝ≥0∞ :=
…
```
theorem Green40.green_40 Does $f(r) \to \infty$? sorry line 64 source
Source documentation
Does $f(r) \to \infty$? [Gr24]

depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, ENNReal, Green40.f, Filter.atTop, nhds, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40 : answer(sorry) ↔ Tendsto f atTop (𝓝 ⊤) := by
…
```
Mentions: Green40.f
theorem Green40.green_40.sanity_f_one The only value known is $f(1) = 1$, which follows from the existence of the Hamming code [Gr24] sorry line 69 source
Source documentation
The only value known is $f(1) = 1$, which follows from the existence of the Hamming code [Gr24].

depends on sorry what this means
Statement uses: Eq, ENNReal, Green40.f, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.sanity_f_one : f 1 = 1 := by
…
```
Mentions: Green40.f
theorem Green40.green_40.upper_bound $f(r) \le r^r / r! \sim e^r$ [Gr24] sorry line 74 source
Source documentation
$f(r) \le r^r / r! \sim e^r$ [Gr24].

depends on sorry what this means
Statement uses: Nat, LE.le, ENNReal, Green40.f, HDiv.hDiv, HPow.hPow, Nat.factorial
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.upper_bound (r : ℕ) : f r ≤ (r ^ r : ℝ≥0∞) / (r.factorial : ℝ≥0∞) := by
…
```
Mentions: Green40.f
theorem Green40.green_40.f_eq_one_for_all The possibility that f(r) = 1 for all r has not been ruled out [Gr24] sorry line 79 source
Source documentation
The possibility that f(r) = 1 for all r has not been ruled out [Gr24]

depends on sorry what this means
Statement uses: Iff, True, Nat, Eq, ENNReal, Green40.f, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.f_eq_one_for_all : answer(sorry) ↔ ∀ r, f r = 1 := by
…
```
Mentions: Green40.f
theorem Green40.green_40.f_two_eq_one It is not known whether f(2) = 1 [Gr24] sorry line 84 source
Source documentation
It is not known whether f(2) = 1 [Gr24]

depends on sorry what this means
Statement uses: Iff, True, Eq, ENNReal, Green40.f, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.f_two_eq_one : answer(sorry) ↔ f 2 = 1 := by
…
```
Mentions: Green40.f
theorem Green40.green_40.upper_bound_f_two The best-known upper bound for $f(2)$ is $1.4238$ [CHL97] sorry line 89 source
Source documentation
The best-known upper bound for $f(2)$ is $1.4238$ [CHL97].

depends on sorry what this means
Statement uses: LE.le, ENNReal, Green40.f, OfNat.ofNat, Nat, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.upper_bound_f_two : f 2 ≤ (1.4238 : ℝ≥0∞) := by
…
```
Mentions: Green40.f
def Green40.hammingBallFinset line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, 𝔽₂
Proof uses: Finset.filter, LE.le, hammingNorm, Fin, ZMod, OfNat.ofNat, Finset.univ
16 instances, coercions and auxiliary constants left out.
def Green40.IsCoveringFinset line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, 𝔽₂
Proof uses: Eq, HAdd.hAdd, Fin, ZMod, OfNat.ofNat, Green40.hammingBallFinset, Finset.univ
18 instances, coercions and auxiliary constants left out.
def Green40.minDensityFinset line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ENNReal
Proof uses: iInf, Finset, 𝔽₂, Green40.IsCoveringFinset, HDiv.hDiv, HMul.hMul, Finset.card, Nat.card, Green40.hammingBall, HPow.hPow, OfNat.ofNat
26 instances, coercions and auxiliary constants left out.
def Green40.f_tilde line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ENNReal
Proof uses: Filter.liminf, Green40.minDensityFinset, Filter.atTop
5 instances, coercions and auxiliary constants left out.
theorem Green40.green_40.variants.arbitrary_subsets Does $\tilde{f}(r) \to \infty$? sorry line 111 source
Source documentation
Does $\tilde{f}(r) \to \infty$? [Gr24]

depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, ENNReal, Green40.f_tilde, Filter.atTop, nhds, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.variants.arbitrary_subsets : answer(sorry) ↔ Tendsto f_tilde atTop (𝓝 ⊤) := by
…
```
Mentions: Green40.f_tilde
theorem Green40.green_40.variants.arbitrary_subsets_sanity_f_tilde_two It is known that $\tilde{f}(2) = 1$ [St94] sorry line 116 source
Source documentation
It is known that $\tilde{f}(2) = 1$ [St94].

depends on sorry what this means
Statement uses: Eq, ENNReal, Green40.f_tilde, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.variants.arbitrary_subsets_sanity_f_tilde_two : f_tilde 2 = 1 := by
…
```
Mentions: Green40.f_tilde
theorem Green40.green_40.f_tilde_le_f We evidently have $\tilde{f}(r) \le f(r)$ [Gr24] line 121 source
Source documentation
We evidently have $\tilde{f}(r) \le f(r)$ [Gr24].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, ENNReal, Green40.f_tilde, Green40.f
Proof uses: Filter.liminf_le_liminf, Filter.atTop, Green40.minDensityFinset, Green40.minDensity, Filter.Eventually.of_forall, le_iInf₂, Submodule, ZMod, OfNat.ofNat, 𝔽₂, Fin, Green40.IsCoveringSubspace, HDiv.hDiv, HMul.hMul, Nat.card, Subtype, Membership.mem, Green40.hammingBall, HPow.hPow, Set.Finite and 44 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.f_tilde_le_f (r : ℕ) : f_tilde r ≤ f r := by
…
```
Mentions: Green40.f_tilde, Green40.f
def Green40.f_all line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ENNReal
Proof uses: Filter.limsup, Green40.minDensity, Filter.atTop
5 instances, coercions and auxiliary constants left out.
theorem Green40.green_40.variants.all_n Does $f_{\text{all}}(r) \to \infty$? sorry line 159 source
Source documentation
Does $f_{\text{all}}(r) \to \infty$? [Gr24]
The target filter is 𝓝 ⊤, as in green_40 and green_40.variants.arbitrary_subsets. On ℝ≥0∞, atTop is the principal ultrafilter at ⊤, so Tendsto f_all atTop atTop would say that f_all r = ⊤ for all large r rather than that f_all r → ∞.

depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, ENNReal, Green40.f_all, Filter.atTop, nhds, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_40.variants.all_n : answer(sorry) ↔ Tendsto f_all atTop (𝓝 ⊤) := by
…
```
Mentions: Green40.f_all