627.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, 9 contain sorry, 0 declared as axioms

Erdős Problem 627

References:

erdosproblems.com/627
[AFM25] Araujo, I. and Filipe, R. and Miyazaki, R., A note on the maximum ratio between chromatic number and clique number. arXiv:2512.16062 (2025).
[Er61d] Erdős, P., Graph theory and probability. II. Canadian J. Math. (1961), 346-352.
[Er67c] Erdős, P., Some remarks on chromatic graphs. Colloq. Math. (1967), 253-256.
[Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35.
[Zy52] Zykov, A. A., On some properties of linear complexes. Amer. Math. Soc. Translation (1952), 33.

Imports (1)

FormalConjecturesUtil

def Erdos627.maxChromaticCliqueRatio maxChromaticCliqueRatio n is $f(n)$, the maximum of $\chi(G)/\omega(G)$ over all graphs $G$ on $n$ vertices line 51 source
Source documentation
maxChromaticCliqueRatio n is $f(n)$, the maximum of $\chi(G)/\omega(G)$ over all graphs $G$ on $n$ vertices.
A graph on Fin n is finite, so its chromatic number (an element of ℕ∞) is finite and ENat.toNat returns it. The maximum is taken over the finitely many graphs on Fin n, so the supremum is attained. For $n = 0$ the only graph is empty, with $\chi = \omega = 0$, and the convention $0 / 0 = 0$ gives $f(0) = 0$; this does not affect any asymptotic statement below.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: iSup, SimpleGraph, Fin, HDiv.hDiv, ENat.toNat, SimpleGraph.chromaticNumber, SimpleGraph.cliqueNum
6 instances, coercions and auxiliary constants left out.
```
noncomputable def maxChromaticCliqueRatio (n : ℕ) : ℝ :=
…
```
theorem Erdos627.erdos_627 Let $\omega(G)$ denote the clique number of $G$ and $\chi(G)$ the chromatic number sorry line 65 source
Source documentation
Let $\omega(G)$ denote the clique number of $G$ and $\chi(G)$ the chromatic number. If $f(n)$ is the maximum value of $\chi(G)/\omega(G)$, as $G$ ranges over all graphs on $n$ vertices, then does $$\lim_{n\to\infty}\frac{f(n)}{n/(\log_2n)^2}$$ exist?
Since $f(n) \asymp n/(\log_2 n)^2$ (see Erdos627.erdos_627.variants.theta), the limit, if it exists, is a finite real number.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, Filter.Tendsto, Nat, HDiv.hDiv, Erdos627.maxChromaticCliqueRatio, HPow.hPow, Real.logb, OfNat.ofNat, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_627 : answer(sorry) ↔
    ∃ L : ℝ, Tendsto (fun n : ℕ ↦ maxChromaticCliqueRatio n / ((n : ℝ) / Real.logb 2 n ^ 2))
      atTop (𝓝 L) := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.theta Erdős [Er67c] proved that $$f(n) \asymp \frac{n}{(\log_2 n)^2}.$$ sorry line 75 source
Source documentation
Erdős [Er67c] proved that $$f(n) \asymp \frac{n}{(\log_2 n)^2}.$$

depends on sorry what this means
Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos627.maxChromaticCliqueRatio, HDiv.hDiv, HPow.hPow, Real.logb, OfNat.ofNat
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_627.variants.theta :
    (fun n : ℕ ↦ maxChromaticCliqueRatio n) =Θ[atTop]
      (fun n : ℕ ↦ (n : ℝ) / Real.logb 2 n ^ 2) := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.lower Erdős [Er67c] proved the lower bound $$f(n) \geq \left(\frac{1}{4} + o(1)\right) \frac{n}{(\log_2 n)^2}.$$ sorry line 85 source
Source documentation
Erdős [Er67c] proved the lower bound $$f(n) \geq \left(\frac{1}{4} + o(1)\right) \frac{n}{(\log_2 n)^2}.$$

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, Real.logb, Erdos627.maxChromaticCliqueRatio, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_627.variants.lower :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (1 / 4 - ε) * ((n : ℝ) / Real.logb 2 n ^ 2) ≤ maxChromaticCliqueRatio n := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.upper The method of Erdős [Er67c] gives the upper bound sorry line 97 source
Source documentation
The method of Erdős [Er67c] gives the upper bound $$f(n) \leq (4 + o(1)) \frac{n}{(\log_2 n)^2}.$$ Erdős states the constant as $1$, but Araujo, Filipe, and Miyazaki [AFM25] note that his method gives $4$.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, Erdos627.maxChromaticCliqueRatio, HMul.hMul, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Real.logb, 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_627.variants.upper :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      maxChromaticCliqueRatio n ≤ (4 + ε) * ((n : ℝ) / Real.logb 2 n ^ 2) := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.limit_bounds Consequently, if the limit in Erdos627.erdos_627 exists, it lies in $[1/4, 4]$ [Er67c] (with the correction of the upper constant from $1$ to $4$ noted in [AFM25]) sorry line 107 source
Source documentation
Consequently, if the limit in Erdos627.erdos_627 exists, it lies in $[1/4, 4]$ [Er67c] (with the correction of the upper constant from $1$ to $4$ noted in [AFM25]).

depends on sorry what this means
Statement uses: Real, Filter.Tendsto, Nat, HDiv.hDiv, Erdos627.maxChromaticCliqueRatio, HPow.hPow, Real.logb, OfNat.ofNat, Filter.atTop, nhds, And, LE.le
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_627.variants.limit_bounds :
    ∀ L : ℝ, Tendsto (fun n : ℕ ↦ maxChromaticCliqueRatio n / ((n : ℝ) / Real.logb 2 n ^ 2))
      atTop (𝓝 L) → 1 / 4 ≤ L ∧ L ≤ 4 := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.afm_upper Documented declaration: afm_upper sorry line 118 source
Source documentation
Araujo, Filipe, and Miyazaki [AFM25, Theorem 1.3] improved the upper bound to $$f(n) \leq (3.71943 + o(1)) \frac{n}{(\log_2 n)^2},$$ using recent improvements in the asymptotics of Ramsey numbers. [AFM25] is an arXiv preprint.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, Erdos627.maxChromaticCliqueRatio, HMul.hMul, HAdd.hAdd, OfScientific.ofScientific, Bool.true, HDiv.hDiv, HPow.hPow, Real.logb, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_627.variants.afm_upper :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      maxChromaticCliqueRatio n ≤ (3.71943 + ε) * ((n : ℝ) / Real.logb 2 n ^ 2) := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.conditional Documented declaration: conditional sorry line 132 source
Source documentation
Araujo, Filipe, and Miyazaki [AFM25, Theorem 1.2]: suppose that $R(s,t) \leq R(k)$ for all $s, t, k \in \mathbb{N}$ with $st \leq k^2$ (their Conjecture 1.1), and that $\lim_{k \to \infty} \frac{\log_2 R(k)}{k}$ exists and equals $\ell$. Then $$f(n) = (\ell^2 + o(1)) \frac{n}{(\log_2 n)^2},$$ so the limit in Erdos627.erdos_627 exists and equals $\ell^2$. Here $R(s,t)$ is the two-colour Ramsey number and $R(k) = R(k,k)$ (see [77]). [AFM25] is an arXiv preprint.

depends on sorry what this means
Statement uses: Real, Nat, LE.le, HMul.hMul, HPow.hPow, OfNat.ofNat, SimpleGraph.classicalRamsey, SimpleGraph.diagonalRamsey, Filter.Tendsto, HDiv.hDiv, Real.logb, Filter.atTop, nhds, Erdos627.maxChromaticCliqueRatio
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_627.variants.conditional (ℓ : ℝ)
    (hR : ∀ s t k : ℕ, s * t ≤ k ^ 2 → classicalRamsey s t ≤ diagonalRamsey k)
    (hlim : Tendsto (fun k : ℕ ↦ Real.logb 2 (diagonalRamsey k : ℝ) / (k : ℝ)) atTop (𝓝 ℓ)) :
    Tendsto (fun n : ℕ ↦ maxChromaticCliqueRatio n / ((n : ℝ) / Real.logb 2 n ^ 2))
      atTop (𝓝 (ℓ ^ 2)) := by
…
```
Mentions: Erdos627.maxChromaticCliqueRatio
theorem Erdos627.erdos_627.variants.tutte_zykov Tutte and Zykov [Zy52] independently proved that for every $k$ there is a graph with $\omega(G) = 2$ and $\chi(G) = k$ sorry line 146 source
Source documentation
Tutte and Zykov [Zy52] independently proved that for every $k$ there is a graph with $\omega(G) = 2$ and $\chi(G) = k$.
We require $k \geq 2$: a graph with $\omega(G) = 2$ has an edge, so $\chi(G) \geq 2$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, SimpleGraph, Fin, And, Eq, SimpleGraph.cliqueNum, ENat, SimpleGraph.chromaticNumber
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 erdos_627.variants.tutte_zykov :
    ∀ k : ℕ, 2 ≤ k → ∃ (n : ℕ) (G : SimpleGraph (Fin n)),
      G.cliqueNum = 2 ∧ G.chromaticNumber = (k : ℕ∞) := by
…
```
theorem Erdos627.erdos_627.variants.erdos_1961 Erdős [Er61d] proved that for every (large) $n$ there is a graph on $n$ vertices with $\omega(G) = 2$ and $$\chi(G) \gg \frac{n^{1/2}}{\log n},$$ whence $f(n) \gg n^{1/2}/\log n$ sorry line 158 source
Source documentation
Erdős [Er61d] proved that for every (large) $n$ there is a graph on $n$ vertices with $\omega(G) = 2$ and $$\chi(G) \gg \frac{n^{1/2}}{\log n},$$ whence $f(n) \gg n^{1/2}/\log n$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, SimpleGraph, Fin, Eq, SimpleGraph.cliqueNum, LE.le, HDiv.hDiv, HMul.hMul, Real.sqrt, Real.log, ENat.toNat, SimpleGraph.chromaticNumber, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_627.variants.erdos_1961 :
    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
      G.cliqueNum = 2 ∧
        c * Real.sqrt (n : ℝ) / Real.log (n : ℝ) ≤ (G.chromaticNumber.toNat : ℝ) := by
…
```
Mentions: c