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

36 declarations, 13 contain sorry, 0 declared as axioms

Erdős Problem 36

References:

Imports (1)

FormalConjecturesUtil

Imported by 3 files

def Erdos36.Overlap The number of solutions to the equation $a - b = k$, for $a \in A$ and $b \in B$ line 38 source
Source documentation
The number of solutions to the equation $a - b = k$, for $a \in A$ and $b \in B$. This represents the "overlap" between sets $A$ and $B$ for a given difference $k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int, Nat
Proof uses: Finset.card, Prod, Finset.filter, Erdos36.Overlap.match_1, Eq, HSub.hSub, Prod.fst, Prod.snd, Finset.product
3 instances, coercions and auxiliary constants left out.
```
def Overlap (A B : Finset ℤ) (k : ℤ) : ℕ := ((A.product B).filter <| fun (a, b) => a - b = k).card
```
def Erdos36.MaxOverlap The maximum overlap for a given pair of sets $A$ and $B$, taken over all possible integer differences $k$ line 44 source
Source documentation
The maximum overlap for a given pair of sets $A$ and $B$, taken over all possible integer differences $k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int, Nat
Proof uses: iSup, Erdos36.Overlap
1 instances, coercions and auxiliary constants left out.
```
noncomputable def MaxOverlap (A B : Finset ℤ) : ℕ := iSup <| Overlap A B
```
Mentions: Erdos36.Overlap
def Erdos36.M Let $A$ and $B$ be two complementary subsets, a splitting of the numbers $\{1, 2, \dots, 2n\}$, such that both have the same cardinality $n$ line 52 source
Source documentation
Let $A$ and $B$ be two complementary subsets, a splitting of the numbers $\{1, 2, \dots, 2n\}$, such that both have the same cardinality $n$. Define $M(n)$ to be the minimum MaxOverlap that can be achieved, ranging over all such partitions $(A, B)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, Int, Disjoint, Eq, Union.union, Finset.Icc, OfNat.ofNat, HMul.hMul, Finset.card, Erdos36.MaxOverlap
17 instances, coercions and auxiliary constants left out.
```
noncomputable def M (n : ℕ) : ℕ :=
…
```
lemma Erdos36.one_le_overlap A small API lemma: every pair (a, b) ∈ A × B contributes to Overlap A B (a - b) line 60 source
Source documentation
A small API lemma: every pair (a, b) ∈ A × B contributes to Overlap A B (a - b).
```
private lemma one_le_overlap {A B : Finset ℤ} {a b : ℤ}
    (ha : a ∈ A) (hb : b ∈ B) : 1 ≤ Overlap A B (a - b) :=
…
```
Mentions: Erdos36.Overlap
lemma Erdos36.overlap_le_card_left For a fixed difference k, the first coordinate determines the second, so an overlap is never larger than either side line 68 source
Source documentation
For a fixed difference k, the first coordinate determines the second, so an overlap is never larger than either side. This is what makes MaxOverlap a supremum of a bounded set.
```
private lemma overlap_le_card_left (A B : Finset ℤ) (k : ℤ) : Overlap A B k ≤ A.card := by
…
```
Mentions: Erdos36.Overlap
lemma Erdos36.bddAbove_range_overlap The range of Overlap A B is bounded, so MaxOverlap is a genuine supremum rather than the junk value sSup returns on an unbounded set line 78 source
Source documentation
The range of Overlap A B is bounded, so MaxOverlap is a genuine supremum rather than the junk value sSup returns on an unbounded set.
```
private lemma bddAbove_range_overlap (A B : Finset ℤ) :
    BddAbove (Set.range (Overlap A B)) := by
…
```
Mentions: Erdos36.Overlap
lemma Erdos36.maxOverlap_le_card_left line 85 source
lemma Erdos36.overlap_eq_zero_of_notMem_sub An overlap can only be nonzero for a difference that is actually realised, which confines the search for MaxOverlap to a finite set line 91 source
Source documentation
An overlap can only be nonzero for a difference that is actually realised, which confines the search for MaxOverlap to a finite set.
```
private lemma overlap_eq_zero_of_notMem_sub (A B : Finset ℤ) {k : ℤ}
    (hk : k ∉ (A ×ˢ B).image fun p => p.1 - p.2) : Overlap A B k = 0 := by
…
```
Mentions: Erdos36.Overlap
lemma Erdos36.maxOverlap_eq_sup MaxOverlap as a supremum over a finite set of differences line 101 source
Source documentation
MaxOverlap as a supremum over a finite set of differences. This is the form that makes it possible to evaluate: the iSup in the definition ranges over all of ℤ, but every difference outside A - B contributes 0.
```
private lemma maxOverlap_eq_sup (A B : Finset ℤ) :
    MaxOverlap A B = ((A ×ˢ B).image fun p => p.1 - p.2).sup (Overlap A B) := by
…
```
Mentions: Erdos36.MaxOverlap, Erdos36.Overlap
lemma Erdos36.M_eq_image The pairs M n ranges over are exactly the n-element subsets of {1, …, 2n}, each paired with its complement line 113 source
Source documentation
The pairs M n ranges over are exactly the n-element subsets of {1, …, 2n}, each paired with its complement. This turns the sInf over an unbounded family of Finset ℤ into an infimum over a Finset.
```
private lemma M_eq_image (n : ℕ) :
    M n = sInf ((fun A : Finset ℤ => MaxOverlap A (Finset.Icc (1 : ℤ) (2 * n) \ A)) ''
      {A | A ⊆ Finset.Icc (1 : ℤ) (2 * n) ∧ A.card = n}) := by
…
```
Mentions: Erdos36.M, Erdos36.MaxOverlap
def Erdos36.maxOverlapC A computable stand-in for MaxOverlap line 138 source
Source documentation
A computable stand-in for MaxOverlap. Overlap is already computable; the only obstacle is the iSup, and maxOverlap_eq_sup says it agrees with this Finset.sup.
```
private def maxOverlapC (A B : Finset ℤ) : ℕ :=
…
```
lemma Erdos36.maxOverlap_eq_maxOverlapC line 142 source
def Erdos36.parts The n-element subsets of {1, …, 2n} line 146 source
Source documentation
The n-element subsets of {1, …, 2n}.
```
private def parts (n : ℕ) : Finset (Finset ℤ) :=
…
```
lemma Erdos36.mem_parts line 151 source
lemma Erdos36.parts_nonempty line 156 source
lemma Erdos36.M_eq_min' M n as the minimum of a Finset of naturals, which is what makes it evaluable line 163 source
Source documentation
M n as the minimum of a Finset of naturals, which is what makes it evaluable.
```
private lemma M_eq_min' (n : ℕ) :
    M n = ((parts n).image fun A => maxOverlapC A (Finset.Icc (1 : ℤ) (2 * n) \ A)).min'
      ((parts_nonempty n).image _) := by
…
```
Mentions: Erdos36.M, Erdos36.parts, Erdos36.maxOverlapC, Erdos36.parts_nonempty
lemma Erdos36.maxOverlap_singleton_one_two MaxOverlap {1} {2} = 1: the only nonzero overlap is at k = -1 line 175 source
Source documentation
MaxOverlap {1} {2} = 1: the only nonzero overlap is at k = -1.
```
private lemma maxOverlap_singleton_one_two :
    MaxOverlap ({1} : Finset ℤ) ({2} : Finset ℤ) = 1 := by
…
```
Mentions: Erdos36.MaxOverlap
theorem Erdos36.M_one This example calculates the value of $M 1$ line 201 source
Source documentation
This example calculates the value of $M 1$. The set is $\{1, 2\}$, so the only partition is $A = \{1\}, B = \{2\}$ (or vice versa). The possible differences are $1 - 2 = -1$ and $2 - 1 = 1$. The Overlap for $k=-1$ is 1 (if $A=\{1\}, B=\{2\}$) and for $k=1$ also 1 (if $A=\{2\}, B=\{1\}$ ). The MaxOverlap is $1$, since the Overlap is $0$ for other $k$. Thus, $M 1 = 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos36.M, OfNat.ofNat
Proof uses: le_antisymm, Nat.sInf_le, Set.ofPred, Exists, Finset, Int, Disjoint, Union.union, Finset.Icc, HMul.hMul, Finset.card, Erdos36.MaxOverlap, Exists.intro, Singleton.singleton, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl and 34 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
theorem M_one : M 1 = 1 := by
…
```
Mentions: Erdos36.M
theorem Erdos36.M_two For $n = 2$, the set is $\{1, 2, 3, 4\}$ line 232 source
Source documentation
For $n = 2$, the set is $\{1, 2, 3, 4\}$. The balanced partition $A = \{1, 4\}, B = \{2, 3\}$ has all four pairwise differences ($\pm 1, \pm 2$) distinct, so MaxOverlap = 1. Any balanced partition has both pieces nonempty, so MaxOverlap \geq 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos36.M, OfNat.ofNat
Proof uses: Eq.mpr, Finset.min', Finset.image, Finset, Int, SDiff.sdiff, Finset.Icc, HMul.hMul, Finset.Nonempty.image, id, congrArg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem M_two : M 2 = 1 := by
…
```
Mentions: Erdos36.M
theorem Erdos36.M_three For n = 3 the best splitting of {1, …, 6} has maximum overlap 2 line 238 source
Source documentation
For n = 3 the best splitting of {1, …, 6} has maximum overlap 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos36.M, OfNat.ofNat
Proof uses: Eq.mpr, Finset.min', Finset.image, Finset, Int, SDiff.sdiff, Finset.Icc, HMul.hMul, Finset.Nonempty.image, id, congrArg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem M_three : M 3 = 2 := by
…
```
Mentions: Erdos36.M
theorem Erdos36.M_four For n = 4 the best splitting of {1, …, 8} still has maximum overlap 2 line 245 source
Source documentation
For n = 4 the best splitting of {1, …, 8} still has maximum overlap 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos36.M, OfNat.ofNat
Proof uses: Eq.mpr, Finset.min', Finset.image, Finset, Int, SDiff.sdiff, Finset.Icc, HMul.hMul, Finset.Nonempty.image, id, congrArg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem M_four : M 4 = 2 := by
…
```
Mentions: Erdos36.M
theorem Erdos36.M_five For n = 5 the best splitting of {1, …, 10} has maximum overlap 3 line 252 source
Source documentation
For n = 5 the best splitting of {1, …, 10} has maximum overlap 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos36.M, OfNat.ofNat
Proof uses: Eq.mpr, Finset.min', Finset.image, Finset, Int, SDiff.sdiff, Finset.Icc, HMul.hMul, Finset.Nonempty.image, id, congrArg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem M_five : M 5 = 3 := by
…
```
Mentions: Erdos36.M
def Erdos36.MinOverlapQuotient The quotient of the minimum maximum overlap $M(N)$ by $N$ line 260 source
Source documentation
The quotient of the minimum maximum overlap $M(N)$ by $N$. The central question of the minimum overlap problem is to determine the asymptotic behavior of this quotient as $N \to \infty$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, Erdos36.M
5 instances, coercions and auxiliary constants left out.
```
noncomputable def MinOverlapQuotient (N : ℕ) := (M N : ℝ) / N
…
```
Mentions: Erdos36.M
theorem Erdos36.minimum_overlap.variants.lower.erdos_1955 A lower bound of $\frac 1 4$ sorry line 268 source
Source documentation
A lower bound of $\frac 1 4$. See Some remarks on number theory (in Hebrew) by Paul Erdős, Riveon Lematematika 9, p.45-48,1955

L4DEL explanation
A lower bound of $\frac 1 4$. See Some remarks on number theory (in Hebrew) by Paul Erdős, Riveon Lematematika 9, p.45-48,1955
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LE.le, Real, HDiv.hDiv, OfNat.ofNat, Nat, Filter.liminf, Erdos36.MinOverlapQuotient, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.lower.erdos_1955 :
    (1 : ℝ) / 4 ≤ atTop.liminf MinOverlapQuotient := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.lower.scherk_1955 A lower bound of $1 - frac{1}{\sqrt 2}$ sorry line 279 source
Source documentation
A lower bound of $1 - frac{1}{\sqrt 2}$. Scherk (written communication), see On the minimal overlap problem of Erdös by Leo Moser, Аста Аrithmetica V, p. 117-119, 1959

L4DEL explanation
A lower bound of $1 - frac{1}{\sqrt 2}$. Scherk (written communication), see On the minimal overlap problem of Erdös by Leo Moser, Аста Аrithmetica V, p. 117-119, 1959
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LT.lt, Real, HSub.hSub, OfNat.ofNat, Inv.inv, Real.sqrt, Nat, Filter.liminf, Erdos36.MinOverlapQuotient, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.lower.scherk_1955 :
    1 - (√2)⁻¹ < atTop.liminf MinOverlapQuotient := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.lower.swierczkowski_1958 A lower bound of $\frac{4 - \sqrt{6}}{5}$ sorry line 290 source
Source documentation
A lower bound of $\frac{4 - \sqrt{6}}{5}$. See On the intersection of a linear set with the translation of its complement by Stanisław Świerczkowski1, Colloquium Mathematicum 5(2), p. 185-197, 1958

L4DEL explanation
A lower bound of $\frac{4 - \sqrt{6}}{5}$. See On the intersection of a linear set with the translation of its complement by Stanisław Świerczkowski1, Colloquium Mathematicum 5(2), p. 185-197, 1958
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LT.lt, Real, HDiv.hDiv, HSub.hSub, OfNat.ofNat, Nat, HPow.hPow, Filter.liminf, Erdos36.MinOverlapQuotient, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.lower.swierczkowski_1958 :
    (4 - 6 ^ ((1 : ℝ) / 2)) / 5 < atTop.liminf MinOverlapQuotient := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.lower.haugland_1996 A lower bound of $\sqrt{4 - \sqrt{15}}$ sorry line 298 source
Source documentation
A lower bound of $\sqrt{4 - \sqrt{15}}$.

depends on sorry what this means
Statement uses: LT.lt, Real, HPow.hPow, HSub.hSub, OfNat.ofNat, Nat, HDiv.hDiv, Filter.liminf, Erdos36.MinOverlapQuotient, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.lower.haugland_1996 :
    (4 - 15 ^((1 : ℝ) / 2)) ^ ((1 : ℝ) / 2) < atTop.liminf MinOverlapQuotient := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.lower.white_2022 A lower bound of $0.379005$: the minimum overlap constant is at least $0.379005$ sorry line 308 source
Source documentation
A lower bound of $0.379005$: the minimum overlap constant is at least $0.379005$. See Erdős' minimum overlap problem by Ethan Patrick White, 2022

L4DEL explanation
A lower bound of $0.379005$: the minimum overlap constant is at least $0.379005$. See Erdős' minimum overlap problem by Ethan Patrick White, 2022
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LE.le, Real, OfScientific.ofScientific, Bool.true, Filter.liminf, Nat, Erdos36.MinOverlapQuotient, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.lower.white_2022 :
    0.379005 ≤ atTop.liminf MinOverlapQuotient := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.upper.erdos_1955 The example (with $N$ even), $A = \{\frac N 2 + 1, \dots, \frac{3N}{2}\}$ shows an upper bound of $\frac 1 2$ sorry line 317 source
Source documentation
The example (with $N$ even), $A = \{\frac N 2 + 1, \dots, \frac{3N}{2}\}$ shows an upper bound of $\frac 1 2$.

depends on sorry what this means
Statement uses: LE.le, Real, Filter.limsup, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.upper.erdos_1955 :
    atTop.limsup MinOverlapQuotient ≤ (1 : ℝ) / 2 := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.upper.MRS_1956 An upper bound of $\frac 2 5$ sorry line 328 source
Source documentation
An upper bound of $\frac 2 5$. See Minimal overlapping under translation. by T. S. Motzkin, K. E. Ralston and J. L. Selfridge, in "The summer meeting in Seattle" by V. L. Klee Jr., Bull. Amer. Math. Soc.62, p. 558, 1956

L4DEL explanation
An upper bound of $\frac 2 5$. See Minimal overlapping under translation. by T. S. Motzkin, K. E. Ralston and J. L. Selfridge, in "The summer meeting in Seattle" by V. L. Klee Jr., Bull. Amer. Math. Soc.62, p. 558, 1956
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LE.le, Real, Filter.limsup, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.upper.MRS_1956 :
    atTop.limsup MinOverlapQuotient ≤ (2 : ℝ) / 5 := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.upper.haugland_1996 An upper bound of $0.38200298812318988$ sorry line 338 source
Source documentation
An upper bound of $0.38200298812318988$. See Advances in the Minimum Overlap Problem by Jan Kristian Haugland, Journal of Number Theory Volume 58, Issue 1, p 71-78, 1996

L4DEL explanation
An upper bound of $0.38200298812318988$. See Advances in the Minimum Overlap Problem by Jan Kristian Haugland, Journal of Number Theory Volume 58, Issue 1, p 71-78, 1996
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LE.le, Real, Filter.limsup, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.upper.haugland_1996 :
    atTop.limsup MinOverlapQuotient ≤ 0.38200298812318988 := by
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.minimum_overlap.variants.upper.haugland_2022 An upper bound of $0.3809268534330870$ sorry line 348 source
Source documentation
An upper bound of $0.3809268534330870$. See The minimum overlap problem by Jan Kristian Haugland

L4DEL explanation
An upper bound of $0.3809268534330870$. See The minimum overlap problem by Jan Kristian Haugland
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LE.le, Real, Filter.limsup, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minimum_overlap.variants.upper.haugland_2022 :
    atTop.limsup MinOverlapQuotient ≤ 0.3809268534330870 := by sorry
…
```
Mentions: Erdos36.MinOverlapQuotient
theorem Erdos36.erdos_36.variants.lower Find a better lower bound! sorry line 355 source
Source documentation
Find a better lower bound!

depends on sorry what this means
Statement uses: Exists, Real, And, LT.lt, OfScientific.ofScientific, Bool.true, LE.le, Filter.liminf, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, Eq, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_36.variants.lower:
    ∃ (c : ℝ), 0.379005 < c ∧ c ≤ atTop.liminf MinOverlapQuotient ∧ c = answer(sorry) := by
…
```
Mentions: c, Erdos36.MinOverlapQuotient
theorem Erdos36.erdos_36.variants.upper Find a better upper bound! sorry line 363 source
Source documentation
Find a better upper bound!

depends on sorry what this means
Statement uses: Exists, Real, And, LT.lt, OfScientific.ofScientific, Bool.true, LE.le, Filter.limsup, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, Eq, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_36.variants.upper :
    ∃ (c : ℝ), c < 0.380926853433087 ∧ atTop.limsup MinOverlapQuotient ≤ c ∧ c = answer(sorry) := by
…
```
Mentions: c, Erdos36.MinOverlapQuotient
theorem Erdos36.erdos_36.variants.exists The limit of MinOverlapQuotient exists and it is less than $0.385694$ sorry line 371 source
Source documentation
The limit of MinOverlapQuotient exists and it is less than $0.385694$.

depends on sorry what this means
Statement uses: Exists, Real, And, Filter.Tendsto, Nat, Erdos36.MinOverlapQuotient, Filter.atTop, nhds, LT.lt, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_36.variants.exists : ∃ c, atTop.Tendsto MinOverlapQuotient (𝓝 c) ∧ c < 0.385694 := by
…
```
Mentions: c, Erdos36.MinOverlapQuotient
theorem Erdos36.erdos_36 Find the value of the limit of MinOverlapQuotient! sorry line 378 source
Source documentation
Find the value of the limit of MinOverlapQuotient!

depends on sorry what this means
Statement uses: Filter.Tendsto, Nat, Real, Erdos36.MinOverlapQuotient, Filter.atTop, nhds, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_36 : atTop.Tendsto MinOverlapQuotient (𝓝 answer(sorry)) := by
…
```
Mentions: Erdos36.MinOverlapQuotient