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

7 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 23

References:

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

theorem Erdos23.erdos_23.variants.n1 Every triangle-free graph on $5$ vertices can be made bipartite by removing at most $1$ edge sorry line 42 source
Source documentation
Every triangle-free graph on $5$ vertices can be made bipartite by removing at most $1$ edge. This is the $n = 1$ case of Erdős Problem 23.

depends on sorry what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, SimpleGraph.CliqueFree, Exists, And, LE.le, SimpleGraph.IsBipartite, Finset.card, Sym2, SDiff.sdiff, Finset, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_23.variants.n1 :
    ∀ (G : SimpleGraph (Fin 5)), G.CliqueFree 3 → ∃ (H : SimpleGraph (Fin 5)),
        H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 1 := by
…
```
theorem Erdos23.erdos_23.variants.n1_tight There exists a triangle-free graph on $5$ vertices such that at least $1$ edge must be removed to make it bipartite line 53 source
Source documentation
There exists a triangle-free graph on $5$ vertices such that at least $1$ edge must be removed to make it bipartite. This shows the bound in erdos_23_n1 is tight.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, SimpleGraph, Fin, OfNat.ofNat, Nat, And, SimpleGraph.CliqueFree, LE.le, SimpleGraph.IsBipartite, Finset.card, Sym2, SDiff.sdiff, Finset, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj
Proof uses: Exists.intro, SimpleGraph.cycleGraph, And.intro, id, Decidable.byContradiction, Not, Eq, EmptyCollection.emptyCollection, Iff.mp, Finset.card_eq_zero, LT.lt, Nat.lt_one_iff, not_le, Finset.sdiff_eq_empty_iff_subset, Set, SimpleGraph.edgeSet, SimpleGraph.edgeSet_subset_edgeSet, Membership.mem, Eq.mp, forall_congr and 20 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_23.variants.n1_tight :
    ∃ (G : SimpleGraph (Fin 5)), G.CliqueFree 3 ∧ ∀ (H : SimpleGraph (Fin 5)),
        H ≤ G → H.IsBipartite → 1 ≤ (G.edgeFinset \ H.edgeFinset).card := by
…
```
theorem Erdos23.erdos_23.variants.n5 Every triangle-free graph on $25$ vertices can be made bipartite by removing at most $25$ edges sorry line 80 source
Source documentation
Every triangle-free graph on $25$ vertices can be made bipartite by removing at most $25$ edges.
This is the $n = 5$ case of Erdős Problem 23. It follows from the high-density range of Balogh-Clemen-Lidicky together with McKay's complete catalogue of the 23-vertex extremal graphs for bipartization of triangle-free graphs.

depends on sorry what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, SimpleGraph.CliqueFree, Exists, And, LE.le, SimpleGraph.IsBipartite, Finset.card, Sym2, SDiff.sdiff, Finset, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_23.variants.n5 :
    ∀ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 → ∃ (H : SimpleGraph (Fin 25)),
        H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 25 := by
…
```
theorem Erdos23.erdos_23.variants.n5_tight There exists a triangle-free graph on $25$ vertices such that at least $25$ edges must be removed to make it bipartite sorry line 92 source
Source documentation
There exists a triangle-free graph on $25$ vertices such that at least $25$ edges must be removed to make it bipartite. The balanced blow-up of $C_5$ with five parts of size $5$ witnesses this.

depends on sorry what this means
Statement uses: Exists, SimpleGraph, Fin, OfNat.ofNat, Nat, And, SimpleGraph.CliqueFree, LE.le, SimpleGraph.IsBipartite, Finset.card, Sym2, SDiff.sdiff, Finset, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_23.variants.n5_tight :
    ∃ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 ∧ ∀ (H : SimpleGraph (Fin 25)),
        H ≤ G → H.IsBipartite → 25 ≤ (G.edgeFinset \ H.edgeFinset).card := by
…
```
def Erdos23.blowupC5 The blow-up of the 5-cycle line 103 source
Source documentation
The blow-up of the 5-cycle $C_5$: replace each vertex of $C_5$ with an independent set of $n$ vertices, and connect two vertices iff their corresponding vertices in $C_5$ are adjacent. The vertex set is $\mathbb{Z}/5\mathbb{Z} \times \{0, \ldots, n-1\}$, where $(i, a)$ and $(j, b)$ are adjacent iff $j = i + 1$ or $i = j + 1$ in $\mathbb{Z}/5\mathbb{Z}$.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Prod, ZMod, OfNat.ofNat, Fin
Proof uses: SimpleGraph.fromRel, Erdos23.blowupC5.match_1, Or, Eq, HAdd.hAdd
13 instances, coercions and auxiliary constants left out.
```
def blowupC5 (n : ℕ) : SimpleGraph (ZMod 5 × Fin n) :=
…
```
theorem Erdos23.blowupC5_tight The blow-up of $C_5$ shows that the bound $n^2$ in Erdős Problem 23 is tight: any bipartite subgraph must omit at least $n^2$ edges sorry line 112 source
Source documentation
The blow-up of $C_5$ shows that the bound $n^2$ in Erdős Problem 23 is tight: any bipartite subgraph must omit at least $n^2$ edges.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, SimpleGraph, Prod, ZMod, Fin, LE.le, Erdos23.blowupC5, SimpleGraph.IsBipartite, HPow.hPow, Finset.card, Sym2, SDiff.sdiff, Finset, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj
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 blowupC5_tight (n : ℕ) (_hn : 0 < n) (H : SimpleGraph (ZMod 5 × Fin n))
    (hH : H ≤ blowupC5 n) (hBip : H.IsBipartite) :
    n ^ 2 ≤ ((blowupC5 n).edgeFinset \ H.edgeFinset).card := by
…
```
Mentions: Erdos23.blowupC5
theorem Erdos23.erdos_23 Can every triangle-free graph on $5n$ vertices be made bipartite by deleting at most $n^2$ edges? sorry line 122 source
Source documentation
Can every triangle-free graph on $5n$ vertices be made bipartite by deleting at most $n^2$ edges?

depends on sorry what this means
Statement uses: Iff, True, Nat, Fintype, Eq, Fintype.card, HMul.hMul, OfNat.ofNat, SimpleGraph, SimpleGraph.CliqueFree, Exists, And, LE.le, SimpleGraph.IsBipartite, Finset.card, Sym2, SDiff.sdiff, Finset, Classical.propDecidable, SimpleGraph.edgeFinset and 2 more
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_23 : answer(sorry) ↔
    ∀ (n : ℕ) (V : Type) [Fintype V], Fintype.card V = 5 * n →
      ∀ (G : SimpleGraph V), G.CliqueFree 3 →
        ∃ (H : SimpleGraph V),
          H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ n^2 := by
…
```