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

10 declarations, 7 contain sorry, 0 declared as axioms

Erdős Problem 78

References:

erdosproblems.com/78
[Co15] Cohen, Gil, Two-source dispersers for polylogarithmic entropy and improved Ramsey graphs. arXiv:1506.04428 (2015).
[Er47] Erdős, P., Some remarks on the theory of graphs. Bull. Amer. Math. Soc. (1947), 292-294.
[Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
[Er88] Erdős, P, Problems and results in combinatorial analysis and graph theory. Discrete Math. (1988), 81-92.
[Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350.
[Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[Li23b] Li, Xin, Two source extractors for asymptotically optimal entropy, and (many) more. arXiv:2303.06802 (2023).
[Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).

Imports (1)

FormalConjecturesUtil

def Erdos78.explicitGraph The graph on Fin n described by an adjacency oracle adj line 60 source
Source documentation
The graph on Fin n described by an adjacency oracle adj. Two distinct vertices u and v are adjacent if adj (1ⁿ, u, v) or adj (1ⁿ, v, u) is true.
The number of vertices is given in unary, as the list List.replicate n true. So if adj is computable in polynomial time, then the whole graph on n vertices is computable in time polynomial in n. This is the notion of a weakly explicit family of graphs; compare stronglyExplicitGraph.

standard axioms: Quot.sound, propext what this means
Statement uses: Prod, List, Bool, Nat, SimpleGraph, Fin
Proof uses: SimpleGraph.fromRel, Eq, Prod.mk, List.replicate, Bool.true
1 instances, coercions and auxiliary constants left out.
```
def explicitGraph (adj : List Bool × ℕ × ℕ → Bool) (n : ℕ) : SimpleGraph (Fin n) :=
…
```
def Erdos78.stronglyExplicitGraph The graph on Fin n described by an adjacency oracle adj which receives n in binary line 72 source
Source documentation
The graph on Fin n described by an adjacency oracle adj which receives n in binary. Two distinct vertices u and v are adjacent if adj (n, u, v) or adj (n, v, u) is true.
If adj is computable in polynomial time, then each adjacency query is answered in time polynomial in $\log n$. This is the notion of a strongly explicit family of graphs, which is what "explicit Ramsey graph" usually means in the literature (e.g. [Co15], [Li23b]). Compare explicitGraph, where only time polynomial in $n$ is allowed.

standard axioms: Quot.sound, propext what this means
Statement uses: Prod, Nat, Bool, SimpleGraph, Fin
Proof uses: SimpleGraph.fromRel, Eq, Prod.mk, Bool.true
1 instances, coercions and auxiliary constants left out.
```
def stronglyExplicitGraph (adj : ℕ × ℕ × ℕ → Bool) (n : ℕ) : SimpleGraph (Fin n) :=
…
```
def Erdos78.NoHomogeneousSet The graph G has no clique and no independent set with m vertices line 78 source
Source documentation
The graph G has no clique and no independent set with m vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: And, SimpleGraph.CliqueFree, Compl.compl
1 instances, coercions and auxiliary constants left out.
```
def NoHomogeneousSet {V : Type*} (G : SimpleGraph V) (m : ℕ) : Prop :=
…
```
theorem Erdos78.erdos_78 Let $R(k)$ be the Ramsey number for $K_k$ sorry line 96 source
Source documentation
Let $R(k)$ be the Ramsey number for $K_k$. Give a constructive proof that $R(k) > C^k$ for some constant $C > 1$.
Equivalently, give an explicit construction of graphs on $n$ vertices which contain no clique and no independent set of size $\geq c \log n$, for some constant $c > 0$.
We formalise "explicit" as: the adjacency relation of the graph on $n$ vertices is decided by a single algorithm that runs in time polynomial in $n$ (see explicitGraph). This is the weakest reasonable notion ("weakly explicit"); even this is open. The strongly explicit version, with time polynomial in $\log n$, is erdos_78.variants.strongly_explicit.
This problem is #4 in Ramsey Theory in the graphs problem collection.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Prod, List, Bool, Nat, ComplexityTheory.IsPolyTime, Filter.Eventually, Erdos78.NoHomogeneousSet, Fin, Erdos78.explicitGraph, Nat.ceil, HMul.hMul, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_78 :
    ∃ c > (0 : ℝ), ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
      ∀ᶠ n in atTop, NoHomogeneousSet (explicitGraph adj n) ⌈c * log n⌉₊ := by
…
```
Mentions: c, Erdos78.NoHomogeneousSet, Erdos78.explicitGraph
theorem Erdos78.erdos_78.variants.nonconstructive Erdős [Er47] gave a simple probabilistic, non-constructive proof that $R(k) > C^k$ for some constant $C > 1$ sorry line 106 source
Source documentation
Erdős [Er47] gave a simple probabilistic, non-constructive proof that $R(k) > C^k$ for some constant $C > 1$. In fact $R(k) > 2^{k/2}$ for all $k \geq 3$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LT.lt, HPow.hPow, SimpleGraph.diagonalRamsey, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_78.variants.nonconstructive :
    ∃ C > (1 : ℝ), ∀ᶠ k in atTop, C ^ k < (SimpleGraph.diagonalRamsey k : ℝ) := by
…
```
Mentions: SimpleGraph.diagonalRamsey
theorem Erdos78.erdos_78.variants.little_o_sqrt Erdős also asked for an explicit construction of graphs on $n$ vertices whose largest clique and independent set have size $o(n^{1/2})$ sorry line 116 source
Source documentation
Erdős also asked for an explicit construction of graphs on $n$ vertices whose largest clique and independent set have size $o(n^{1/2})$. Such constructions are now known; see [Co15] for the history.

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, Real.sqrt, Prod, List, Bool, ComplexityTheory.IsPolyTime, Filter.Eventually, Erdos78.NoHomogeneousSet, Fin, Erdos78.explicitGraph, Nat.ceil
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 erdos_78.variants.little_o_sqrt :
    ∃ f : ℕ → ℝ, f =o[atTop] (fun n ↦ √(n : ℝ)) ∧
      ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
        ∀ᶠ n in atTop, NoHomogeneousSet (explicitGraph adj n) ⌈f n⌉₊ := by
…
```
Mentions: Erdos78.NoHomogeneousSet, Erdos78.explicitGraph
theorem Erdos78.erdos_78.variants.cohen Cohen [Co15] constructed explicit graphs on $n$ vertices with no clique and no independent set of size $2^{(\log \log n)^C}$, for some constant $C > 0$ sorry line 127 source
Source documentation
Cohen [Co15] constructed explicit graphs on $n$ vertices with no clique and no independent set of size $2^{(\log \log n)^C}$, for some constant $C > 0$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Prod, List, Bool, Nat, ComplexityTheory.IsPolyTime, Filter.Eventually, Erdos78.NoHomogeneousSet, Fin, Erdos78.explicitGraph, Nat.ceil, HPow.hPow, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_78.variants.cohen :
    ∃ C > (0 : ℝ), ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
      ∀ᶠ n in atTop,
        NoHomogeneousSet (explicitGraph adj n) ⌈(2 : ℝ) ^ (log (log n)) ^ C⌉₊ := by
…
```
Mentions: Erdos78.NoHomogeneousSet, Erdos78.explicitGraph
theorem Erdos78.erdos_78.variants.li Li [Li23b] improved this to explicit graphs on $n$ vertices with no clique and no independent set of size $(\log n)^C$, for some constant $C > 0$ sorry line 138 source
Source documentation
Li [Li23b] improved this to explicit graphs on $n$ vertices with no clique and no independent set of size $(\log n)^C$, for some constant $C > 0$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Prod, List, Bool, Nat, ComplexityTheory.IsPolyTime, Filter.Eventually, Erdos78.NoHomogeneousSet, Fin, Erdos78.explicitGraph, Nat.ceil, HPow.hPow, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_78.variants.li :
    ∃ C > (0 : ℝ), ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
      ∀ᶠ n in atTop, NoHomogeneousSet (explicitGraph adj n) ⌈(log n) ^ C⌉₊ := by
…
```
Mentions: Erdos78.NoHomogeneousSet, Erdos78.explicitGraph
theorem Erdos78.erdos_78.variants.strongly_explicit Documented declaration: strongly_explicit sorry line 149 source
Source documentation
The strongly explicit version of erdos_78: an explicit family of graphs on $n$ vertices with no clique and no independent set of size $\geq c \log n$, where each adjacency query is answered in time polynomial in $\log n$ (see stronglyExplicitGraph).

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Prod, Nat, Bool, ComplexityTheory.IsPolyTime, Filter.Eventually, Erdos78.NoHomogeneousSet, Fin, Erdos78.stronglyExplicitGraph, Nat.ceil, HMul.hMul, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_78.variants.strongly_explicit :
    ∃ c > (0 : ℝ), ∃ adj : ℕ × ℕ × ℕ → Bool, IsPolyTime adj ∧
      ∀ᶠ n in atTop, NoHomogeneousSet (stronglyExplicitGraph adj n) ⌈c * log n⌉₊ := by
…
```
Mentions: c, Erdos78.NoHomogeneousSet, Erdos78.stronglyExplicitGraph
theorem Erdos78.erdos_78.variants.li_strongly_explicit Documented declaration: li_strongly_explicit sorry line 160 source
Source documentation
The construction of Li [Li23b] is strongly explicit: there are graphs on $n$ vertices with no clique and no independent set of size $(\log n)^C$, for some constant $C > 0$, whose adjacency queries are answered in time polynomial in $\log n$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Prod, Nat, Bool, ComplexityTheory.IsPolyTime, Filter.Eventually, Erdos78.NoHomogeneousSet, Fin, Erdos78.stronglyExplicitGraph, Nat.ceil, HPow.hPow, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_78.variants.li_strongly_explicit :
    ∃ C > (0 : ℝ), ∃ adj : ℕ × ℕ × ℕ → Bool, IsPolyTime adj ∧
      ∀ᶠ n in atTop, NoHomogeneousSet (stronglyExplicitGraph adj n) ⌈(log n) ^ C⌉₊ := by
…
```
Mentions: Erdos78.NoHomogeneousSet, Erdos78.stronglyExplicitGraph