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

Dean's conjecture on cycles of length divisible by `k`

References:

arxiv/2605.02731 Existence of cycles of length divisible by 3 or 4 by Ilkyoo Choi, Hojin Chu, Ringi Kim, Boram Park, where this is Conjecture 1.1.
[De88] Dean, N., Open problem, in Cycles and Rays. (1988).
[DeLeSa93] Dean, N. and Lesniak, L. and Saito, A., Cycles of length 0 modulo 4 in graphs. Discrete Math. (1993), 133--139.
[ChSa94] Chen, G. and Saito, A., Graphs with a cycle of length divisible by three. J. Combin. Theory Ser. B (1994), 277--292.
[LuMaZh26] Luo, Yufan and Ma, Jie and Zhao, Ziyuan, Dean's conjecture and cycles modulo k. arXiv:2601.13552 (2026).

Imports (1)

FormalConjecturesUtil

theorem Arxiv.«2605.02731».dean_conjecture Conjecture 1.1 (Dean, 1988) sorry line 51 source
Source documentation
Conjecture 1.1 (Dean, 1988). For every integer $k \geq 3$, every finite simple graph with minimum degree at least $k$ contains a cycle whose length is divisible by $k$.
A cycle has length at least 3, so the divisor is never 0 and the statement is not satisfied for a trivial reason. SimpleGraph.minDegree is 0 on a graph with no vertices and on a graph with no edges, so the hypothesis excludes both.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.minDegree, Exists, And, Membership.mem, Set, SimpleGraph.cycleLengths, Dvd.dvd
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 dean_conjecture :
    answer(sorry) ↔ ∀ (k : ℕ), 3 ≤ k → ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], k ≤ G.minDegree →
        ∃ m ∈ G.cycleLengths, k ∣ m := by
…
```
theorem Arxiv.«2605.02731».dean_conjecture.variants.five The case $k = 5$ sorry line 61 source
Source documentation
The case $k = 5$. This is the only case of the conjecture that is still open.

depends on sorry what this means
Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Nat, OfNat.ofNat, SimpleGraph.minDegree, Exists, And, Membership.mem, Set, SimpleGraph.cycleLengths, Dvd.dvd
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 dean_conjecture.variants.five :
    answer(sorry) ↔ ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
      [DecidableRel G.Adj], 5 ≤ G.minDegree → ∃ m ∈ G.cycleLengths, 5 ∣ m := by
…
```
theorem Arxiv.«2605.02731».dean_conjecture.variants.three The case $k = 3$, proved by Chen and Saito [ChSa94] sorry line 70 source
Source documentation
The case $k = 3$, proved by Chen and Saito [ChSa94].

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Nat, OfNat.ofNat, SimpleGraph.minDegree, Exists, And, Membership.mem, Set, SimpleGraph.cycleLengths, Dvd.dvd
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 dean_conjecture.variants.three {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : 3 ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, 3 ∣ m := by
…
```
theorem Arxiv.«2605.02731».dean_conjecture.variants.four The case $k = 4$, proved by Dean, Lesniak and Saito [DeLeSa93] sorry line 79 source
Source documentation
The case $k = 4$, proved by Dean, Lesniak and Saito [DeLeSa93].

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Nat, OfNat.ofNat, SimpleGraph.minDegree, Exists, And, Membership.mem, Set, SimpleGraph.cycleLengths, Dvd.dvd
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 dean_conjecture.variants.four {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : 4 ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, 4 ∣ m := by
…
```
theorem Arxiv.«2605.02731».dean_conjecture.variants.six_le The cases $k \geq 6$, proved by Luo, Ma and Zhao [LuMaZh26] sorry line 89 source
Source documentation
The cases $k \geq 6$, proved by Luo, Ma and Zhao [LuMaZh26]. With [ChSa94] and [DeLeSa93] this leaves dean_conjecture.variants.five as the only open case.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nat, LE.le, OfNat.ofNat, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.minDegree, Exists, And, Membership.mem, Set, SimpleGraph.cycleLengths, Dvd.dvd
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 dean_conjecture.variants.six_le {V : Type} [Fintype V] [DecidableEq V] {k : ℕ}
    (hk : 6 ≤ k) (G : SimpleGraph V) [DecidableRel G.Adj] (hG : k ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, k ∣ m := by
…
```
theorem Arxiv.«2605.02731».minDegree_bot_eq_zero A graph with no edges has minimum degree 0, so the hypothesis of the conjecture rules it out line 97 source
Source documentation
A graph with no edges has minimum degree 0, so the hypothesis of the conjecture rules it out. This is a check that the hypothesis carries weight.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Fin, OfNat.ofNat, Bot.bot, SimpleGraph
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minDegree_bot_eq_zero : (⊥ : SimpleGraph (Fin 5)).minDegree = 0 := by
…
```
theorem Arxiv.«2605.02731».minDegree_top_fin_four The complete graph on four vertices has minimum degree 3, so it is one of the graphs the case k = 3 applies to line 103 source
Source documentation
The complete graph on four vertices has minimum degree 3, so it is one of the graphs the case k = 3 applies to.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Fin, OfNat.ofNat, Top.top, SimpleGraph
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem minDegree_top_fin_four : (⊤ : SimpleGraph (Fin 4)).minDegree = 3 := by
…
```

FormalConjectures/Arxiv/2605.02731/DeanCycles.lean

Dean's conjecture on cycles of length divisible by k

`FormalConjectures/Arxiv/2605.02731/DeanCycles.lean`

Dean's conjecture on cycles of length divisible by `k`