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

4 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 191

References:

erdosproblems.com/191
[ErGr79] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics. Enseign. Math. (1979), 325-344.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
[Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79.
[Ro03] Rödl, Vojtěch, On homogeneous sets of positive integers. J. Combin. Theory Ser. A (2003), 229-240.
[CFS13] Conlon, David and Fox, Jacob and Sudakov, Benny, Two extensions of Ramsey's theorem. Duke Math. J. (2013), 2903-2927.

Imports (1)

FormalConjecturesUtil

theorem Erdos191.erdos_191 sorry line 68 source
depends on sorry what this means
Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, SimpleGraph, Subtype, Membership.mem, Finset, Finset.Icc, Exists, And, Or, SimpleGraph.IsClique, SimpleGraph.IsIndepSet, LE.le, Finset.sum, HDiv.hDiv and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos191.erdos_191.variants.conlon_fox_sudakov Documented declaration: conlon_fox_sudakov sorry line 80 source
Source documentation
Conlon, Fox, and Sudakov [CFS13] proved that, if $n$ is sufficiently large, then in any $2$-colouring of $\binom{\{2,\ldots,n\}}{2}$ there exists some $X\subseteq \{2,\ldots,n\}$ such that $\binom{X}{2}$ is monochromatic and $$\sum_{x\in X}\frac{1}{\log x}\geq 2^{-8}\log\log\log n.$$

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, SimpleGraph, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Exists, And, Or, SimpleGraph.IsClique, SimpleGraph.IsIndepSet, LE.le, Real, HMul.hMul, HPow.hPow, Int, Neg.neg, Real.log and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_191.variants.conlon_fox_sudakov : ∀ᶠ n : ℕ in atTop,
    ∀ G : SimpleGraph (Finset.Icc 2 n), ∃ X : Finset (Finset.Icc 2 n),
      (G.IsClique X ∨ G.IsIndepSet X) ∧
        2 ^ (-8 : ℤ) * Real.log (Real.log (Real.log n)) ≤ ∑ x ∈ X, 1 / Real.log (x : ℕ) := by
…
```
theorem Erdos191.erdos_191.variants.rodl_upper Rödl [Ro03] constructed, for all sorry line 92 source
Source documentation
Rödl [Ro03] constructed, for all $n$, a $2$-colouring of $\binom{\{2,\ldots,n\}}{2}$ such that if $X\subseteq \{2,\ldots,n\}$ is such that $\binom{X}{2}$ is monochromatic then $$\sum_{x\in X}\frac{1}{\log x}\ll \log\log\log n.$$

depends on sorry what this means
Statement uses: Exists, Real, Filter.Eventually, Nat, SimpleGraph, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Or, SimpleGraph.IsClique, SimpleGraph.IsIndepSet, LE.le, Finset.sum, HDiv.hDiv, Real.log, HMul.hMul, 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 erdos_191.variants.rodl_upper : ∃ c : ℝ, ∀ᶠ n : ℕ in atTop,
    ∃ G : SimpleGraph (Finset.Icc 2 n), ∀ X : Finset (Finset.Icc 2 n),
      G.IsClique X ∨ G.IsIndepSet X →
        ∑ x ∈ X, 1 / Real.log (x : ℕ) ≤ c * Real.log (Real.log (Real.log n)) := by
…
```
Mentions: c
theorem Erdos191.erdos_191.variants.three_colours Rödl [Ro03] proved that the answer to erdős_191 is negative if we consider sorry line 105 source
Source documentation
Rödl [Ro03] proved that the answer to erdős_191 is negative if we consider $3$-colourings: there is a constant $C$ such that for every $n$ some $3$-colouring of $\binom{\{2,\ldots,n\}}{2}$ has $\sum_{x\in X}\frac{1}{\log x} < C$ for every monochromatic $X$.

L4DEL explanation
Rödl [Ro03] proved that the answer to erdős_191 is negative if we consider $3$-colourings: there is a constant $C$ such that for every $n$ some $3$-colouring of $\binom{\{2,\ldots,n\}}{2}$ has $\sum_{x\in X}\frac{1}{\log x} < C$ for every monochromatic $X$.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Exists, Real, Nat, Sym2, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin, Ne, Eq, Sym2.mk, LT.lt, Finset.sum, HDiv.hDiv, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_191.variants.three_colours : ∃ C : ℝ, ∀ n : ℕ,
    ∃ c : Sym2 (Finset.Icc 2 n) → Fin 3, ∀ X : Finset (Finset.Icc 2 n),
      (∃ i : Fin 3, ∀ x ∈ X, ∀ y ∈ X, x ≠ y → c s(x, y) = i) →
        ∑ x ∈ X, 1 / Real.log (x : ℕ) < C := by
…
```
Mentions: c