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

9 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 80

References:

erdosproblems.com/80
erdosproblems.com/600, stated in FormalConjectures/ErdosProblems/600.lean
[FoLo12] Fox, Jacob and Loh, Po-Shen, On a problem of Erdős and Rothschild on edges in triangles. Combinatorica (2012), 619--628.

600 asks the same question from the other side. Erdos600.eFunction n r is the least edge count forcing some edge into r triangles; f c n here is the largest book forced once the edge count is at least $cn^2$. So r ≤ f c n and Erdos600.eFunction n r ≤ c * n^2 say the same thing, and the two functions are inverse to each other in that sense. Both are built on SimpleGraph.trianglesContaining, which 600 introduced.

Imports (1)

FormalConjecturesUtil

def Erdos80.bookNumber The size of the largest book in G: the greatest number of triangles sharing a single edge line 49 source
Source documentation
The size of the largest book in G: the greatest number of triangles sharing a single edge. Finset.sup gives 0 on a graph with no edges, which is the right answer there.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: Finset.sup, Sym2, SimpleGraph.edgeFinset, Finset.card, Finset, SimpleGraph.trianglesContaining
5 instances, coercions and auxiliary constants left out.
```
noncomputable def bookNumber : ℕ :=
…
```
def Erdos80.EveryEdgeInTriangle Every edge of G lies in at least one triangle line 53 source
Source documentation
Every edge of G lies in at least one triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj
Proof uses: Sym2, Membership.mem, Finset, SimpleGraph.edgeFinset, Finset.Nonempty, SimpleGraph.trianglesContaining
4 instances, coercions and auxiliary constants left out.
```
def EveryEdgeInTriangle : Prop :=
…
```
def Erdos80.Admissible The graphs the problem quantifies over: n vertices, at least $cn^2$ edges, and every edge in a triangle line 58 source
Source documentation
The graphs the problem quantifies over: n vertices, at least $cn^2$ edges, and every edge in a triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj
Proof uses: And, LE.le, HMul.hMul, HPow.hPow, OfNat.ofNat, Finset.card, Sym2, SimpleGraph.edgeFinset, Erdos80.EveryEdgeInTriangle
13 instances, coercions and auxiliary constants left out.
```
def Admissible (c : ℝ) {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : Prop :=
…
```
Mentions: c
def Erdos80.f $f_c(n)$, the largest book size forced on every admissible graph, which is the least book number among them line 69 source
Source documentation
$f_c(n)$, the largest book size forced on every admissible graph, which is the least book number among them.
sInf of the empty set is 0, so f c n = 0 when no graph on n vertices has $cn^2$ edges at all. A simple graph has at most $n(n-1)/2$ edges, so that happens for every n once $c \geq 1/2$. The statements below therefore restrict c to the feasible range; without that they are false at, say, c = 2 for reasons unrelated to the question.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, SimpleGraph, Fin, And, Erdos80.Admissible, Classical.propDecidable, SimpleGraph.Adj, Eq, Erdos80.bookNumber
2 instances, coercions and auxiliary constants left out.
```
noncomputable def f (c : ℝ) (n : ℕ) : ℕ :=
…
```
Mentions: c
theorem Erdos80.erdos_80.parts.i Documented declaration: i sorry line 86 source
Source documentation
Let $c>0$ and let $f_c(n)$ be the maximal $m$ such that every graph $G$ with $n$ vertices and at least $cn^2$ edges, where each edge is contained in at least one triangle, must contain a book of size $m$, that is, an edge shared by at least $m$ different triangles. Estimate $f_c(n)$. In particular, is it true that $f_c(n)>n^\epsilon$ for some $\epsilon>0$?
The answer is no. Fox and Loh [FoLo12] proved that $f_c(n) \leq n^{O(1/\log\log n)}$ for every fixed $c < 1/4$, so no $\epsilon > 0$ works for, say, $c = 1/8$. For $c > 1/4$ the situation is different: $f_c(n) \geq n/6$, see erdosproblems.com/80.
The bound $c < 1/2$ is what makes the hypothesis satisfiable: a simple graph on $n$ vertices has at most $n(n-1)/2$ edges, so no graph has $cn^2$ of them once $c \geq 1/2$.

L4DEL explanation
Let $c>0$ and let $f_c(n)$ be the maximal $m$ such that every graph $G$ with $n$ vertices and at least $cn^2$ edges, where each edge is contained in at least one triangle, must contain a book of size $m$, that is, an edge shared by at least $m$ different triangles. Estimate $f_c(n)$. In particular, is it true that $f_c(n)>n^\epsilon$ for some $\epsilon>0$? The answer is no. Fox and Loh [FoLo12] proved that $f_c(n) \leq n^{O(1/\log\log n)}$ for every fixed $c < 1/4$, so no $\epsilon > 0$ works for, say, $c = 1/8$. For $c > 1/4$ the situation is different: $f_c(n) \geq n/6$, see erdosproblems.com/80. The bound $c < 1/2$ is what makes the hypothesis satisfiable: a simple graph on $n$ vertices has at most $n(n-1)/2$ edges, so no graph has $cn^2$ of them once $c \geq 1/2$.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, False, Real, LT.lt, OfNat.ofNat, HDiv.hDiv, Nat, Exists, And, GT.gt, Filter.Eventually, HPow.hPow, Erdos80.f, Filter.atTop
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_80.parts.i :
    answer(False) ↔ ∀ c : ℝ, 0 < c → c < 1 / 2 →
      ∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ ε < f c n := by
…
```
Mentions: c, Erdos80.f
theorem Erdos80.erdos_80.parts.ii The weaker question from the same problem: is $f_c(n) \gg \log n$? sorry line 97 source
Source documentation
The weaker question from the same problem: is $f_c(n) \gg \log n$?
Same feasibility bound on c as above.

depends on sorry what this means
Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, HDiv.hDiv, Nat, Asymptotics.IsBigO, Filter.atTop, Real.log, Erdos80.f
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_80.parts.ii :
    answer(sorry) ↔ ∀ c : ℝ, 0 < c → c < 1 / 2 →
      (fun n : ℕ ↦ (f c n : ℝ)) ≫ (fun n : ℕ ↦ Real.log n) := by
…
```
Mentions: c, Erdos80.f
theorem Erdos80.bookNumber_eq_zero_iff A book is counted by triangles, so bookNumber is 0 exactly when no edge lies in one line 105 source
Source documentation
A book is counted by triangles, so bookNumber is 0 exactly when no edge lies in one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Iff, Eq, Nat, Erdos80.bookNumber, OfNat.ofNat, Sym2, Membership.mem, Finset, SimpleGraph.edgeFinset, SimpleGraph.trianglesContaining, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, Set, SimpleGraph.edgeSet, True, congr, congrArg, Finset.sup, Finset.card, forall_congr, implies_congr, Eq.refl, iff_self
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bookNumber_eq_zero_iff :
    bookNumber G = 0 ↔ ∀ e ∈ G.edgeFinset, G.trianglesContaining e = ∅ := by
…
```
Mentions: Erdos80.bookNumber
theorem Erdos80.bookNumber_bot On a graph with no edges there is no book line 111 source
Source documentation
On a graph with no edges there is no book.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos80.bookNumber, Fin, Bot.bot, SimpleGraph, OfNat.ofNat
Proof uses: of_eq_true, Finset.sup, Sym2, SimpleGraph.edgeFinset, Finset.card, Finset, SimpleGraph.trianglesContaining, Eq.trans, Membership.mem, True, forall_congr, False, EmptyCollection.emptyCollection, implies_congr, Set, SimpleGraph.edgeSet, congrFun', congrArg, SimpleGraph.edgeSet_bot, implies_true
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bookNumber_bot {n : ℕ} : bookNumber (⊥ : SimpleGraph (Fin n)) = 0 := by
…
```
Mentions: Erdos80.bookNumber
theorem Erdos80.everyEdgeInTriangle_bot EveryEdgeInTriangle holds vacuously on a graph with no edges, so the admissible set is nonempty only through the edge count line 117 source
Source documentation
EveryEdgeInTriangle holds vacuously on a graph with no edges, so the admissible set is nonempty only through the edge count.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos80.EveryEdgeInTriangle, Fin, Bot.bot, SimpleGraph
Proof uses: of_eq_true, Sym2, Membership.mem, Finset, SimpleGraph.edgeFinset, Finset.Nonempty, SimpleGraph.trianglesContaining, Eq.trans, True, forall_congr, False, implies_congr, Set, SimpleGraph.edgeSet, EmptyCollection.emptyCollection, congrFun', congrArg, SimpleGraph.edgeSet_bot, Eq.refl, implies_true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem everyEdgeInTriangle_bot {n : ℕ} :
    EveryEdgeInTriangle (⊥ : SimpleGraph (Fin n)) := by
…
```
Mentions: Erdos80.EveryEdgeInTriangle