Every finite connected simple graph that is neither complete nor an odd cycle can be vertex-colored using at most its maximum degree many colors.
Scope: Every finite connected simple graph that is neither complete nor an odd cycle is vertex-colorable with its maximum degree many colors.
Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Starting pointConnected graph, not complete or an odd cycle
→
RelationStructural decomposition and greedy extension
→
ConclusionColorable with Δ colors
Exact scope: Every finite connected simple graph that is neither complete nor an odd cycle is vertex-colorable with its maximum degree many colors.
Exact formal proposition
Hypotheses and conclusion
theorem brooksTheorem : BrooksTheoremStatement
Proof route
How Brooks's Theorem is proved
7 proof stages
Follow the retained proof from the low-degree branches through the nonseparating-path construction to the final regular-graph coloring.
These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.
Forests, a path, and an even cycle stay inside the two-color palette; the separate odd cycle exposes the closing conflict.
01
Start with forests and degree two
Three acyclic components, a seven-vertex path, and an eight-vertex cycle use only alternating cobalt and gold vertex classes, with distinct internal marks so color is not the sole cue. Every path vertex has degree at most two and every even-cycle vertex has degree two. A separate five-cycle alternates the same classes until its muted-vermilion closing edge connects two cobalt vertices, showing the excluded odd-cycle obstruction.
Component attachments constrain the possible two-vertex cut.
04
Resolve the two-vertex-cut structure
The proof analyzes how components attach to a candidate cut pair, narrowing the hard case to two nonadjacent components under the minimum-degree conditions.
The surviving route proves the required pair deletion remains connected.
05
A nearer path survives the farther deletion
A shortest-path choice reaches the nearer side without using the farther deleted point, then joins the component regions in the final pair-deleted graph.
The recurring graph is colored with the middle vertex hollow and its nonadjacent neighbors equal gold.
06
Color the two nonadjacent ends alike
color(u)=color(v)
With w omitted, connectivity supplies an ordering of the remaining graph; u and v receive the same color while every visible edge remains properly colored.
Outside complete graphs and odd cycles, local degree controls the global palette.
Accessible transcript
χ(G) ≤ Δ(G)
The maximum-degree coloring bound, its two exception families, and the proof's forest, greedy, and regular-graph branches are gathered in one reference.
Read the complete poster transcript
GRAPH THEORY · VERTEX COLORING
BROOKS'S THEOREM
LOCAL DEGREE CONTROLS THE GLOBAL PALETTE
FINITE · CONNECTED · SIMPLE
χ(G) ≤ Δ(G)
Adjacent vertices receive different colors.
EXCEPTIONS
Complete graphs · Odd cycles
THE CHECKED ENDPOINT
G is colorable with Δ(G) colors.
HOW THE PROOF MOVES
COLOR FORESTS · RESOLVE MAXIMUM DEGREE TWO · GREEDY-COLOR THE NONREGULAR CASE · FIND A NONSEPARATING TWO-EDGE PATH · COLOR TWO ENDS ALIKE, THEN THE MIDDLE
EXACT SCOPE
An upper bound for finite connected simple graphs that are neither complete nor odd cycles. It does not assert χ(G)=Δ(G).
Theorem schematic
Maximum degree supplies the palette
A connected graph is properly colored within its maximum-degree bound.
χ(G) ≤ Δ(G)
For a finite connected simple graph outside the complete and odd-cycle exceptions, Brooks's theorem constructs a proper coloring with at most the maximum-degree palette.
Result boundary
What this theorem does—and does not—establish
Every finite connected simple graph that is neither complete nor an odd cycle is vertex-colorable with its maximum degree many colors.
The theorem excludes complete graphs and odd cycles rather than classifying their chromatic numbers.
It does not cover disconnected or infinite graphs.
About these visual explanations
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
Open questions and extensions
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
01
Formal evidence
The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
02
Statement alignment
The formal declaration was accepted against the named theorem and its exact variant.
03
Result boundary
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
04
Public wording
The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
05
Canonical source
The first-party source link is pinned to the checked package commit and exact Lean file.
06
Accepted result
A validated accepted-result record binds the four reviews to the checked formalization.
