What is proved

Thirteen results, each stated exactly in the verification section below. Two are unconditional:

• High-degree total coloring, TotalColoring.exists_valid_assignment_of_highDegree. Let be a finite simple graph with decidable adjacency and . Then has a valid total coloring with palette ExtensionPalette (G.maxDegree + 1), that is, with colors. The empty vertex type is included and there is no parity hypothesis.
• Auxiliary rainbow edge coloring, TotalColoring.MinimalExtraction.hasValidRainbowColoring_of_inAuxiliaryClass. For every and every finite with InAuxiliaryClass D H J, the graph has a proper edge coloring with palette Fin (D + 2) that is rainbow on . It is derived from TotalColoring.IsOutsideEdgeMinimalNoncolorable.false_of_critical_allD: no member is noncolorable and minimal in the number of edges outside .

The other results take their inputs as hypotheses:

• reusable steps: the decoder TotalColoring.Auxiliary.Extension.decode_valid (a proper, selector-rainbow edge coloring of decodes through a supplied extension datum to a valid total coloring of ), the matching bound TotalColoring.MatchingLowerBound.exists_matchingGraph_edgeFinset_card_ge (minimum degree and give a matching with at least edges), the membership theorem TotalColoring.Auxiliary.PairSingletonWitness.isAuxiliaryClassMember_of_highDegree (for a supplied pair/singleton witness with and ), the partial-edge selector decoder TotalColoring.partialEdgeSelectorAssignment_valid, and the checker soundness theorem TotalColoring.Certificate.checkExtension_sound;
• conditional endpoints: the transfer TotalColoring.Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass ( colors from a supplied extension into an auxiliary-class member whose selectors lie in ), the partition entry point TotalColoring.Auxiliary.EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition ( colors from a supplied equitable independent partition into classes, nonempty ), and three -color endpoints, each from a supplied proper -edge coloring and supplied certificates: TotalColoring.exists_valid_assignment_of_independentSeedPeel (independent seed and peel order, ), TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel (selector, core coloring and core peel order) and TotalColoring.exists_valid_assignment_of_alternatingRainbowPathSelector (alternating rainbow-path certificate). With these give colors only once all of those inputs are supplied.

The verification page shows each Lean statement beside its statement in words; the same page is rendered below. The exact proof status gives the full account, including the provenance of each layer, and docs/claim-boundary.json is its machine-readable mirror.

[!IMPORTANT] Not proved here. The current default branch, including the adapted-spare endpoint, does not establish:

• the Total Coloring Conjecture;
• an unconditional high-degree or all-graphs Delta + 2 total-coloring conclusion;
• an unconditional total-coloring conclusion from graph hypotheses alone for graphs outside the explicit high-degree regime Fintype.card V ≤ 2 * G.maxDegree;
• Vizing's theorem or existence of the proper edge-coloring witness required by the conditional independent-seed endpoint;
• existence of an independent seed and peel certificate for every graph;
• existence of a total-independent selector, an actual-list coloring of its core, a core-relative peel certificate, or the alternating rainbow-path certificate used by the newer decoder;
• construction of the adapted-spare sets, a physical donor matching, compatible seed or matching data, missing/head labels, or a proper edge coloring needed before the vertex endpoint can apply;
• the stronger auxiliary D + 1 palette;
• an identification of the checked declaration with a final, author-approved manuscript theorem (the manuscript's main theorem is still unlocked); or
• a novelty claim.

The generic transfer does not construct the extension from an arbitrary graph or relate D to that graph's maximum degree. The high-degree Delta + 3 theorem must not be broadened into an unconditional Delta + 2 result, the Total Coloring Conjecture, or an author-approved manuscript or novelty claim.

Paper and references

Manuscript in preparation.

The software itself is archived on Zenodo: release v0.2.0 is doi:10.5281/zenodo.23452514 (all versions: doi:10.5281/zenodo.23452513). Cite the exact release or commit you used; GitHub reads CITATION.cff and offers a Cite this repository menu, and the citation guide lists the commit that first contains each result (release v0.1.0 predates them).

Companion repositories:

• total-coloring-toolkit owns search algorithms, external schemas, and certificate generation.
• total-coloring-data owns reviewed finite artifacts and release manifests.

Raw runs, private drafts, manuscript source, and generated census output do not belong in this repository.

Build and verify

Toolchain Lean v4.32.0 (lean-toolchain); Mathlib v4.32.0, commit 81a5d257c8e410db227a6665ed08f64fea08e997 (lake-manifest.json). On a fresh machine, first install elan.

git clone https://github.com/chenle02/total-coloring-lean.git
cd total-coloring-lean
lake exe cache get
lake build
lake env lean docs/examples/Quickstart.lean

The complete repository gate (including lake env leanchecker and the placeholder scan) is in Trust and reproduction and AGENTS.md; the getting-started guide covers downstream imports and documentation builds.

To use it from another Lake project:

[[require]]
name = "TotalColoring"
git = "https://github.com/chenle02/total-coloring-lean.git"
rev = "v0.2.0"

then import TotalColoring. The comparator statements are the Challenge.lean files under Audit/ (see Audit/README.md); their sorry is intentional and the Audit library is not part of the default build target.

Trust and axioms

The build check at commit c025d20a1826 recorded sorry count 0 and the axioms propext, Classical.choice and Quot.sound only, read for all 13 claims. For 8 of the 13 results the comparator confirmed that the proof proves exactly the statement in the corresponding Audit/*/Challenge.lean, with only those axioms, and independent kernels replayed it; the other 5 are checked by the build only. The build ran on Lean v4.32.0, which carries lean-pkg toolchain advisories (listed in the generated section). The receipts of release v0.2.0 (lower tier and comparator) were produced on a lab workstation. Details and receipts: What the checks establish; the full gate and the parser boundary: Trust and reproduction.

Built with lean-pkg

Developed and verified with lean-pkg (doi:10.5281/zenodo.23272098). The receipts under .lean-receipts/ bind the checks to a source commit, and the verification section below is rendered by lean-pkg page from coverage.yaml, claims.yaml and those receipts; lean-pkg page total-coloring-lean --check confirms it is current.

Authors and AI disclosure

Le Chen, Associate Professor, Department of Mathematics and Statistics, Auburn University, and Songling Shan (see CITATION.cff). Copyright © 2026 Le Chen and contributors; every Lean file carries the standard Apache header, contributions are accepted under the same license, and Mathlib retains its own notices (see NOTICE).

Parts of the Lean development and its documentation were written with AI coding assistance; the commits concerned name it in their Co-Authored-By lines. AI assistance is not human mathematical review: Lean compilation and the comparator check the stated theorems only.

GitHub Sponsors supports formalization maintenance, documentation, CI and cluster verification, and reproducible releases. Sponsorship does not affect theorem claims or proof-review standards.

Find your way

If you want to…	Start here
understand exactly what is proved	Exact proof status and Verification
use a declaration in Lean	Theorem index
audit the module-level proof	Proof architecture (with the proof route at a glance)
contribute a proof or checker	CONTRIBUTING.md and AGENTS.md
use a coding agent safely	Agent guide and llms.txt
cite the software precisely	Citation guide and CITATION.cff

Small, reviewable contributions are welcome. Open an issue before changing a mathematical interface or theorem claim, preserve the trust boundary, and run the complete gate in AGENTS.md.

Verification at a glance

How to read this page. Lean has checked every step of the proofs listed here. Each result is exactly its Lean statement: read the statements below to see what is proved. The titles, the words and the notes are the authors' description, which Lean does not check.

Unconditionally, every finite graph with |V| <= 2 * maxDegree has a total coloring with maxDegree + 3 colors, and every finite auxiliary-class member has a (D + 2)-edge coloring rainbow on J; the D + 2 transfer, the partition entry point and the (q + 1)-color endpoints are conditional on supplied inputs, and the Total Coloring Conjecture is not proved.

• Main results: 13; verified: 13 of 13 (for 8 of them a second checker also compared the statement).

Main results

Total coloring with maxDegree + 3 colors when |V| <= 2 * maxDegree

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $G$ be a finite simple graph on the vertex set $V$ with
$|V| \le 2\Delta(G)$. Then $G$ has a total coloring with the
$\Delta(G)+3$ colors $\{0,1,\dots,\Delta(G)+2\}$: adjacent vertices get
distinct colors, two distinct edges sharing an endpoint get distinct
colors, and every vertex gets a color different from each edge
incident with it.

In Lean. TotalColoringAudit.HighDegree.exists_total_coloring_of_card_le_two_mul_maxDegree in Audit/HighDegree/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem exists_total_coloring_of_card_le_two_mul_maxDegree
    {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hdense : Fintype.card V ≤ 2 * G.maxDegree) :
    ∃ (vertexColor : V → Fin (G.maxDegree + 1 + 2))
      (edgeColor : G.edgeSet → Fin (G.maxDegree + 1 + 2)),
      (∀ v w, G.Adj v w → vertexColor v ≠ vertexColor w) ∧
      (∀ e f, G.lineGraph.Adj e f → edgeColor e ≠ edgeColor f) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) → vertexColor v ≠ edgeColor e)

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Unconditional: the only hypotheses are a finite vertex type, decidable adjacency and the order bound; the empty vertex type is included and there is no parity hypothesis. ExtensionPalette (maxDegree + 1) is Fin (maxDegree + 3).

Every finite auxiliary-class member has a (D + 2)-edge coloring rainbow on its distinguished set

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $H$ be a finite simple graph and $J$ a finite set of unordered pairs
of vertices such that $(H,J)$ is in the auxiliary class
$\mathcal{A}_D$: there are a vertex $x$ and a set $M$ of pairwise
disjoint pairs with $J = M \cup \{\text{edges of } H \text{ at } x\}$,
every pair of $J$ an edge of $H$, no pair of $M$ containing $x$ or a
neighbor of $x$, every vertex other than $x$ in exactly one pair of $J$,
$|J| = D$, $\Delta(H) \le D$ and $2 \le \deg_H(x) \le D$. Then $H$ has a
proper edge coloring with $D+2$ colors in which the edges of $J$ get
pairwise distinct colors.

In Lean. TotalColoringAudit.AuxiliaryClass.exists_rainbow_edge_coloring_of_auxiliaryClass in Audit/AuxiliaryClass/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem exists_rainbow_edge_coloring_of_auxiliaryClass
    {V : Type*} [Fintype V] [DecidableEq V]
    (D : ℕ) (H : SimpleGraph V) [DecidableRel H.Adj]
    (J : Finset (Sym2 V)) (x : V) (M : Finset (Sym2 V))
    (distinguished_edges : ∀ ⦃e⦄, e ∈ J → e ∈ H.edgeSet)
    (matching : ∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f)
    (matching_off_center : ∀ ⦃e⦄, e ∈ M → x ∉ e)
    (matching_avoids_center_neighbors : ∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬H.Adj x v)
    (decomposition : J = M ∪ H.incidenceFinset x)
    (exact_coverage : ∀ v, v ≠ x → ∃! e : Sym2 V, e ∈ J ∧ v ∈ e)
    (card_distinguished : J.card = D)
    (maxDegree_bound : H.maxDegree ≤ D)
    (center_degree : 2 ≤ H.degree x ∧ H.degree x ≤ D) :
    ∃ color : H.edgeSet → Fin (D + 2),
      (∀ e f, H.lineGraph.Adj e f → color e ≠ color f) ∧
      (∀ e f : H.edgeSet, (e : Sym2 V) ∈ J → (f : Sym2 V) ∈ J → e ≠ f →
        color e ≠ color f)

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Unconditional for every D and every finite member; proved by contradiction from the minimal-counterexample theorem below.

No auxiliary-class member is noncolorable and minimal in the number of edges outside J

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

There is no finite $(H,J) \in \mathcal{A}_D$ such that $H$ has no proper
$(D+2)$-edge coloring rainbow on $J$, while every $(H',J) \in
\mathcal{A}_D$ on the same vertex set, with the same $J$ and with no such
coloring, has at least as many edges outside $J$ as $H$.

In Lean. TotalColoringAudit.CriticalAllD.false_of_critical_allD in Audit/CriticalAllD/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem false_of_critical_allD
    {V : Type*} [Fintype V] [DecidableEq V]
    (D : ℕ) (H : SimpleGraph V) [DecidableRel H.Adj] (J : Finset (Sym2 V))
    (member : ∃ (x : V) (M : Finset (Sym2 V)),
      (∀ ⦃e⦄, e ∈ J → e ∈ H.edgeSet) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f) ∧
      (∀ ⦃e⦄, e ∈ M → x ∉ e) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬H.Adj x v) ∧
      J = M ∪ H.incidenceFinset x ∧
      (∀ v, v ≠ x → ∃! e : Sym2 V, e ∈ J ∧ v ∈ e) ∧
      J.card = D ∧
      H.maxDegree ≤ D ∧
      (2 ≤ H.degree x ∧ H.degree x ≤ D))
    (noncolorable : ¬∃ color : H.edgeSet → Fin (D + 2),
      (∀ e f, H.lineGraph.Adj e f → color e ≠ color f) ∧
      (∀ e f : H.edgeSet, (e : Sym2 V) ∈ J → (f : Sym2 V) ∈ J → e ≠ f →
        color e ≠ color f))
    (minimal : ∀ (H₁ : SimpleGraph V) [DecidableRel H₁.Adj],
      (∃ (x : V) (M : Finset (Sym2 V)),
        (∀ ⦃e⦄, e ∈ J → e ∈ H₁.edgeSet) ∧
        (∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f) ∧
        (∀ ⦃e⦄, e ∈ M → x ∉ e) ∧
        (∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬H₁.Adj x v) ∧
        J = M ∪ H₁.incidenceFinset x ∧
        (∀ v, v ≠ x → ∃! e : Sym2 V, e ∈ J ∧ v ∈ e) ∧
        J.card = D ∧
        H₁.maxDegree ≤ D ∧
        (2 ≤ H₁.degree x ∧ H₁.degree x ≤ D)) →
      (¬∃ color : H₁.edgeSet → Fin (D + 2),
        (∀ e f, H₁.lineGraph.Adj e f → color e ≠ color f) ∧
        (∀ e f : H₁.edgeSet, (e : Sym2 V) ∈ J → (f : Sym2 V) ∈ J → e ≠ f →
          color e ≠ color f)) →
      (H.edgeSet \ (J : Set (Sym2 V))).ncard ≤ (H₁.edgeSet \ (J : Set (Sym2 V))).ncard) :
    False

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. The minimal-counterexample step behind the rainbow theorem above; the minimality ranges over members on the same vertex type with the same J.

A proper selector-rainbow auxiliary edge coloring decodes to a valid total coloring

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $G$ and $H$ be simple graphs with an extension datum: a selector
edge $s(v)$ of $H$ for each vertex $v$ of $G$ and an edge $\iota(e)$ of
$H$ for each edge $e$ of $G$, such that adjacent vertices have distinct
selectors, distinct edges of $G$ sharing an endpoint go to distinct edges
of $H$ sharing an endpoint, and $s(v)$ and $\iota(e)$ are distinct and
share an endpoint whenever $v$ is an endpoint of $e$. If $c$ is a proper
edge coloring of $H$ that gives distinct selector edges distinct colors,
then coloring each vertex $v$ by $c(s(v))$ and each edge $e$ by
$c(\iota(e))$ is a valid total coloring of $G$.

In Lean. TotalColoringAudit.Decode.decode_valid in Audit/Decode/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem decode_valid
    {V : Type*} {W : Type*} {C : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (classEdge : V → H.edgeSet) (originalEdge : G.edgeSet → H.edgeSet)
    (classEdge_ne_of_adj : ∀ {v w : V}, G.Adj v w → classEdge v ≠ classEdge w)
    (originalEdge_adj : ∀ {e f : G.edgeSet}, G.lineGraph.Adj e f →
      H.lineGraph.Adj (originalEdge e) (originalEdge f))
    (classEdge_adj_original : ∀ {v : V} {e : G.edgeSet}, v ∈ (e : Sym2 V) →
      H.lineGraph.Adj (classEdge v) (originalEdge e))
    (color : H.edgeSet → C)
    (hvalid : ∀ e f, H.lineGraph.Adj e f → color e ≠ color f)
    (hrainbow : ∀ v w, classEdge v ≠ classEdge w →
      color (classEdge v) ≠ color (classEdge w)) :
    (∀ v w, G.Adj v w → color (classEdge v) ≠ color (classEdge w)) ∧
      (∀ e f, G.lineGraph.Adj e f → color (originalEdge e) ≠ color (originalEdge f)) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) →
        color (classEdge v) ≠ color (originalEdge e))

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. No finiteness and any color type; the extension data are hypotheses.

Conditional transfer: a supplied extension into an auxiliary-class member gives a total coloring with D + 2 colors

Verified. Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

In words.

Let $G$ be a simple graph and $H$ a finite simple graph with
$(H,J) \in \mathcal{A}_D$. If there is an extension datum from $G$ to $H$
(as in the decoding theorem) every selector edge of which belongs to
$J$, then $G$ has a valid total coloring with $D+2$ colors.

In Lean. TotalColoring.Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass in TotalColoring/AuxiliaryTransfer.lean.

theorem exists_valid_decode_of_inAuxiliaryClass
    [Fintype W] [DecidableEq W]
    (D : ℕ) (X : Extension G H) [DecidableRel H.Adj]
    (J : Finset (Sym2 W))
    (hclassEdge : ∀ vertex, X.classEdge vertex ∈ distinguishedEdgeSet H J)
    (hmember : InAuxiliaryClass D H J) :
    ∃ assignment : Assignment G (ExtensionPalette D), assignment.Valid

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Conditional on the supplied extension datum, selector membership in J and the auxiliary-class membership; nothing relates D to the maximum degree of G.

A matching with at least k edges from minimum degree k and order at least 2k

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $H$ be a finite simple graph on $V$ and $k \ge 0$. If every vertex
has degree at least $k$ in $H$ and $2k \le |V|$, then $H$ has a subgraph
in which every vertex has at most one neighbor (a matching) with at
least $k$ edges.

In Lean. TotalColoringAudit.MatchingLowerBound.exists_matchingGraph_edgeFinset_card_ge in Audit/MatchingLowerBound/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem exists_matchingGraph_edgeFinset_card_ge
    {V : Type*} [Fintype V]
    (H : SimpleGraph V) [DecidableRel H.Adj] (k : ℕ)
    (hdegree : ∀ v, k ≤ H.degree v) (horder : 2 * k ≤ Fintype.card V) :
    ∃ (M : SimpleGraph V) (_ : DecidableRel M.Adj),
      M ≤ H ∧ (∀ v, (M.neighborSet v).Subsingleton) ∧ k ≤ M.edgeFinset.card

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

A pair/singleton partition with maxDegree + 1 classes gives auxiliary-class membership when |V| <= 2 * maxDegree

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $G$ be a finite simple graph on $V$ and fix a partition of $V$ into
singletons and pairs of nonadjacent vertices. On $V \cup \{\ast\}$ take
a copy of $G$ together with one selector edge per class: $\ast v$ for a
singleton $\{v\}$ and $vw$ for a pair $\{v,w\}$. Let $J$ be the set of
selector edges and $M$ the pair selectors. If $|J| = \Delta(G)+1$ and
$|V| \le 2\Delta(G)$, then this graph is a member of
$\mathcal{A}_{\Delta(G)+1}$ with center $\ast$, distinguished set $J$
and matching part $M$.

In Lean. TotalColoringAudit.PairSingleton.isAuxiliaryClassMember_of_highDegree in Audit/PairSingleton/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem isAuxiliaryClassMember_of_highDegree
    {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V}
    (partner : V → Option V)
    (partner_ne : ∀ {v w : V}, partner v = some w → v ≠ w)
    (partner_symm : ∀ {v w : V}, partner v = some w → partner w = some v)
    (partner_nonadjacent : ∀ {v w : V}, partner v = some w → ¬G.Adj v w)
    (selector : V → Sym2 (Option V))
    (hselector : ∀ v, selector v = (partner v).elim s(none, some v) (fun w ↦ s(some v, some w)))
    (J : Finset (Sym2 (Option V))) (hJ : J = Finset.univ.image selector)
    (M : Finset (Sym2 (Option V))) (hM : M = J.filter (fun e ↦ (none : Option V) ∉ e))
    (A : SimpleGraph (Option V))
    (hA : A = G.map Function.Embedding.some ⊔ SimpleGraph.fromEdgeSet (J : Set (Sym2 (Option V))))
    [DecidableRel G.Adj] [DecidableRel A.Adj]
    (hclasses : J.card = G.maxDegree + 1)
    (hdense : Fintype.card V ≤ 2 * G.maxDegree) :
    (∀ ⦃e⦄, e ∈ J → e ∈ A.edgeSet) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f) ∧
      (∀ ⦃e⦄, e ∈ M → (none : Option V) ∉ e) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬A.Adj none v) ∧
      J = M ∪ A.incidenceFinset none ∧
      (∀ v, v ≠ none → ∃! e : Sym2 (Option V), e ∈ J ∧ v ∈ e) ∧
      J.card = G.maxDegree + 1 ∧
      A.maxDegree ≤ G.maxDegree + 1 ∧
      (2 ≤ A.degree none ∧ A.degree none ≤ G.maxDegree + 1)

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. The pair/singleton witness is a hypothesis here; the high-degree theorem above constructs one from a matching in the complement of G.

Conditional: a supplied equitable independent partition gives a total coloring with maxDegree + 3 colors

Verified. Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

In words.

Let $G$ be a finite simple graph on a nonempty vertex set $V$ with
$|V| \le 2\Delta(G)$. If $V$ is partitioned into exactly $\Delta(G)+1$
nonempty independent sets whose sizes differ by at most one, then $G$
has a valid total coloring with $\Delta(G)+3$ colors.

In Lean. TotalColoring.Auxiliary.EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition in TotalColoring/EquitablePairSingleton.lean.

theorem exists_valid_assignment_of_highDegreePartition
    (Q : EquitableIndependentPartition G (G.maxDegree + 1))
    (hdense : Fintype.card V ≤ 2 * G.maxDegree) :
    ∃ assignment : Assignment G (ExtensionPalette (G.maxDegree + 1)),
      assignment.Valid

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Conditional on the supplied partition and a nonempty vertex type; retained as an alternate entry point. The high-degree theorem above assumes no partition.

Conditional independent-seed endpoint: q + 1 colors from a proper q-edge coloring, an independent seed and a peel order

Verified. Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

In words.

Let $G$ be a finite simple graph and $q > 0$. Suppose $G$ has a proper
edge coloring with $q$ colors, $A$ is an independent set of vertices,
and the vertices outside $A$ are listed without repetition as
$v_1,\dots,v_m$ (exactly the vertices outside $A$) so that for every $i$
the number of neighbors of $v_i$ among $v_{i+1},\dots,v_m$ is less than
$q - \deg_G(v_i)$ (truncated subtraction). Then $G$ has a valid total
coloring with $q+1$ colors. For $q = \Delta(G)+1$ this is
$\Delta(G)+2$ colors.

In Lean. TotalColoring.exists_valid_assignment_of_independentSeedPeel in TotalColoring/IndependentSeed.lean.

theorem exists_valid_assignment_of_independentSeedPeel {q : ℕ}
    (hq : 0 < q) (phi : EdgeAssignment G (Fin q)) (hphi : phi.Valid)
    (A : Finset V) (hA : G.IsIndepSet (A : Set V))
    (cert : IndependentSeedPeelCertificate G A q) :
    ∃ a : Assignment G (Fin (q + 1)), a.Valid

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Conditional: the edge coloring, the seed and the peel order are hypotheses. Vizing's theorem and the existence of the seed and order are not proved, so the maxDegree + 2 case is not the Total Coloring Conjecture.

Conditional selector decoder: a fresh-color independent set and matching with a peeled core coloring give q + 1 colors

Verified. Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

In words.

Let $G$ be a finite simple graph with a proper edge coloring $\varphi$
with $q$ colors. Let $S$ be an independent set, $F$ a matching none of
whose edges has an endpoint in $S$, and $K \supseteq S$ a vertex set
with $g_0 \colon V \to \{0,\dots,q-1\}$ such that for all
$v, w \in K \setminus S$: $g_0(v) \ne \varphi(e)$ for every edge
$e \notin F$ at $v$, and $g_0(v) \ne g_0(w)$ when $v$ and $w$ are
adjacent. Suppose the vertices outside $K$ are listed without repetition
as $v_1,\dots,v_m$ (exactly the vertices outside $K$) so that
$|N(v_i) \cap ((K \setminus S) \cup \{v_{i+1},\dots,v_m\})| <
q - \deg_G(v_i)$ (truncated subtraction) for every $i$. Then $G$ has a
valid total coloring with $q+1$ colors.

In Lean. TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel in TotalColoring/TotalIndependentSelector.lean.

theorem exists_valid_assignment_of_totalIndependentSelectorPeel
    (phi : EdgeAssignment G (Fin q)) (hphi : phi.Valid)
    (S : Finset V) (hS : G.IsIndepSet (S : Set V))
    (F : Finset G.edgeSet) (hF : EdgeFinsetIsMatching (G := G) F)
    (havoid : EdgeFinsetAvoids (G := G) F S)
    (K : Finset V) (g₀ : V → Fin q)
    (hcore : SelectorOldColoringGoodOn G phi S F K g₀)
    (cert : SelectorCorePeelCertificate G S K q) :
    ∃ a : Assignment G (Fin (q + 1)), a.Valid

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Conditional: the edge coloring, S, F, the core K, the core coloring g0 and the peel order are hypotheses; none of them is constructed.

Partial-edge selector decoder: old edge colors need only be proper outside the fresh matching

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $G$ be a simple graph, $f \in \{0,\dots,q\}$ a fresh color, $S$
an independent set, $F$ a matching none of whose edges has an endpoint
in $S$, and $\varphi$ an edge coloring with $q$ colors in which two
distinct edges outside $F$ sharing an endpoint get distinct colors. Let
$g \colon V \to \{0,\dots,q-1\}$ satisfy, for $v, w \notin S$:
$g(v) \ne \varphi(e)$ for every edge $e \notin F$ at $v$, and
$g(v) \ne g(w)$ when $v$ and $w$ are adjacent. Color the vertices of $S$
and the edges of $F$ with $f$, and every other vertex $v$ and edge $e$
with the image of $g(v)$, resp. $\varphi(e)$, under the order-preserving
bijection from $q$ colors onto the $q+1$ colors other than $f$. This is
a valid total coloring with $q+1$ colors.

In Lean. TotalColoringAudit.PartialEdgeSelector.partialEdgeSelectorAssignment_valid in Audit/PartialEdgeSelector/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem partialEdgeSelectorAssignment_valid
    {V : Type*} [DecidableEq V] {G : SimpleGraph V} {q : ℕ}
    (fresh : Fin (q + 1)) (phi : G.edgeSet → Fin q)
    (S : Finset V) (F : Finset G.edgeSet) (g : V → Fin q)
    (hphi : ∀ e f : G.edgeSet, e ∉ F → f ∉ F → G.lineGraph.Adj e f → phi e ≠ phi f)
    (hS : G.IsIndepSet (S : Set V))
    (hF : ∀ ⦃e f : G.edgeSet⦄, e ∈ F → f ∈ F → ¬G.lineGraph.Adj e f)
    (havoid : ∀ ⦃v : V⦄, v ∈ S → ∀ ⦃e : G.edgeSet⦄, e ∈ F → v ∉ (e : Sym2 V))
    (hallowed : ∀ v, v ∉ S → ∀ e : G.edgeSet, v ∈ (e : Sym2 V) → e ∉ F → phi e ≠ g v)
    (hproper : ∀ v, v ∉ S → ∀ w, w ∉ S → G.Adj v w → g v ≠ g w) :
    (∀ v w, G.Adj v w →
        (if v ∈ S then fresh else fresh.succAbove (g v)) ≠
          (if w ∈ S then fresh else fresh.succAbove (g w))) ∧
      (∀ e f, G.lineGraph.Adj e f →
        (if e ∈ F then fresh else fresh.succAbove (phi e)) ≠
          (if f ∈ F then fresh else fresh.succAbove (phi f))) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) →
        (if v ∈ S then fresh else fresh.succAbove (g v)) ≠
          (if e ∈ F then fresh else fresh.succAbove (phi e)))

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Every input is a hypothesis; no finiteness is assumed.

Conditional alternating rainbow-path selector: a supplied path certificate gives q + 1 colors

Verified. Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

In words.

Let $G$ be a finite simple graph with a proper edge coloring $\varphi_0$
with $q$ colors, and $K$ a vertex set. Suppose there are distinct
vertices $u_0,\dots,u_k$, exactly the vertices of $K$, with path edges
$e_i = u_i u_{i+1}$ ($0 \le i < k$) whose $\varphi_0$-colors are pairwise
distinct; a color $\sigma \in \{0,\dots,q-1\}$ of the same palette
that no edge receives under $\varphi_0$; edge sets $L$ and $F$ of $G$,
each a matching, such that the path edge $e_i$ lies in $L$ exactly for
even $i$ and in $F$ exactly for odd $i$ ($L$ and $F$ may also contain
edges off the path), with no edge of $F$ at $u_0$; a function
$c \colon V \to \{0,\dots,q-1\}$ with $c(u_{i+1}) = \varphi_0(e_i)$;
and a list without repetition of exactly
the vertices outside $K$ satisfying the core peel inequality of the
selector decoder for $S = \{u_0\}$ and $K$. Then $G$ has a valid total
coloring with $q+1$ colors.

In Lean. TotalColoring.exists_valid_assignment_of_alternatingRainbowPathSelector in TotalColoring/TotalIndependentSelector.lean.

theorem exists_valid_assignment_of_alternatingRainbowPathSelector
    (phi₀ : EdgeAssignment G (Fin q)) (hphi₀ : phi₀.Valid)
    (K : Finset V) (k : ℕ)
    (cert : AlternatingRainbowPathSelectorCertificate G phi₀ K k) :
    ∃ a : Assignment G (Fin (q + 1)), a.Valid

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Conditional: the proper edge coloring and the whole certificate (path, rainbow, spare color, matchings, core colors, peel order) are hypotheses; the existence of the path is not proved.

Soundness of the executable extension checker

Verified. Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

In words.

Let $X$ be an extension datum from a finite graph $G$ to a finite graph
$H$ and $c$ an edge coloring of $H$ with a color type with decidable
equality. If the Boolean checker checkExtension accepts $(X, c)$, then
decoding $c$ through $X$ gives a valid total coloring of $G$. (The
checker accepts exactly when $c$ is proper and gives distinct selector
edges distinct colors; that equivalence is the separate lemma
checkExtension_eq_true_iff, not part of this claim.)

In Lean. TotalColoringAudit.Certificate.checkExtension_sound in Audit/Certificate/Challenge.lean: the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

theorem checkExtension_sound
    {V : Type*} {W : Type*} {C : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (classEdge : V → H.edgeSet) (originalEdge : G.edgeSet → H.edgeSet)
    (classEdge_ne_of_adj : ∀ {v w : V}, G.Adj v w → classEdge v ≠ classEdge w)
    (originalEdge_adj : ∀ {e f : G.edgeSet}, G.lineGraph.Adj e f →
      H.lineGraph.Adj (originalEdge e) (originalEdge f))
    (classEdge_adj_original : ∀ {v : V} {e : G.edgeSet}, v ∈ (e : Sym2 V) →
      H.lineGraph.Adj (classEdge v) (originalEdge e))
    (color : H.edgeSet → C)
    [Fintype V] [Fintype W] [DecidableEq W] [DecidableRel H.Adj] [DecidableEq C]
    (h : (decide (∀ e f : H.edgeSet,
            (e ≠ f ∧ ∃ x : W, x ∈ (e : Sym2 W) ∧ x ∈ (f : Sym2 W)) → color e ≠ color f) &&
          decide (∀ v w : V, classEdge v ≠ classEdge w →
            color (classEdge v) ≠ color (classEdge w))) = true) :
    (∀ v w, G.Adj v w → color (classEdge v) ≠ color (classEdge w)) ∧
      (∀ e f, G.lineGraph.Adj e f → color (originalEdge e) ≠ color (originalEdge f)) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) →
        color (classEdge v) ≠ color (originalEdge e))

Axioms. At most Classical.choice, Quot.sound, propext (what the build check records for the whole package).

Note. Concerns well-typed Lean values only; parsing external data is outside the theorem.

What the checks establish

• Every proof is checked by Lean. The package builds; no sorry (an unfinished proof) remains; the only axioms used are Classical.choice, Quot.sound, propext (allowed: propext, Quot.sound, Classical.choice).
• The statements shown are the ones proved. For 8 statement(s), a second checker (comparator) confirmed that the proof proves exactly the statement shown, with only the permitted axioms, and independent Lean kernels replayed the proof.
• Not checked by any tool: that a title or note describes its Lean statement. A definition listed under Definitions checked by a person is compared by name and type only.

The full account of what each check covers and what it takes on trust is lean-pkg's trust model.

How this was checked

• lean-pkg's claims ledger: ready, every required claim is closed by the recorded receipts; 8 of 8 required claim(s) verified (sha256:23f4baa46a3fc93d…).
• Build check (lean-pkg gate) at commit c025d20a1826: sorry count 0; axioms used: Classical.choice, Quot.sound, propext.
• Axioms of every claim: read from the built environment (Lean's collectAxioms) for all 13 claim(s) in claims.yaml, not only the theorems the build prints; none uses an axiom beyond propext, Quot.sound and Classical.choice.
• Toolchain advisory: the build check ran on Lean leanprover/lean4:v4.32.0, which has a known soundness bug fixed in v4.32.1 (lean-v4.32.1-kernel-opaque-fvars; lean-pkg's toolchain advisories).
• Toolchain advisory: the build check ran on Lean leanprover/lean4:v4.32.0, which has a known soundness bug fixed in v4.32.2 (lean-v4.32.2-kernel-nested-inductive; lean-pkg's toolchain advisories).
• Toolchain advisory: the build check ran on Lean leanprover/lean4:v4.32.0, which has a known soundness bug fixed in v4.33.1 (lean-v4.33.1-kernel-and-runtime; lean-pkg's toolchain advisories).
• Toolchain advisory: the build check ran on Lean leanprover/lean4:v4.32.0, which has a known soundness bug fixed in v4.34.1 (lean-v4.34.1-runtime-refcounts; lean-pkg's toolchain advisories).
• Statement comparison (comparator) at commit c025d20a1826: 8 configuration(s), 8 theorem(s) compared (each Challenge statement against its Solution proof); permitted axioms: Classical.choice, Quot.sound, propext; definitions compared by name only: none.

Receipts

Receipt	Check	Commit	Date	Job	SHA-256
.lean-receipts/3f364b51d2c7-comparator.json	statement comparison	3f364b51d2c7	2026-10-18	—	a248b4d7ceeb034d0fb0a3700670e7b59ca7574aa84287f0e2d1589ddd2eeb1e
.lean-receipts/3f364b51d2c7-systemd-user-total-coloring-lean-verify.service-26f87e9fdae2438cb4ab302aa085cb30-h-2db2e0fa6029.json	build	3f364b51d2c7	2026-10-18	—	732ee12803528338b33d21df1482fdc51fd2ed169b579a61b589e5e9e0e0ba84
.lean-receipts/533f9430cb45-comparator.json	statement comparison	533f9430cb45	2026-10-08	—	c3c1f5d65707f99f56a870714d12541fb7b7c1abd60f3358d4f25bd0bbf907bd
.lean-receipts/533f9430cb45-home-workstation-2026-10-08-total-coloring.json	build	533f9430cb45	2026-10-08	—	4ea44f7efdc1ba712e79bf2e9d5f6f2f0e41a350f4c5920197f43e91a16dc966
.lean-receipts/55edc8145228-home-workstation-2026-10-06-total-coloring.json	build	55edc8145228	2026-10-06	—	14d42549e43e9fc24cd17655f207a60a901ed0c4e31ec83c379fe871cbb3b66d
.lean-receipts/c025d20a1826-comparator.json (used here)	statement comparison	c025d20a1826	2026-10-18	—	120f4a7878339120dbb684b778daa944e2c7241d48d0fee3c99b0fde2f28f09b
.lean-receipts/c025d20a1826-systemd-user-total-coloring-lean-verify.service-eff861bf68744993b3eaff1c5e6b37fc-h-2db2e0fa6029.json (used here)	build	c025d20a1826	2026-10-18	—	586b45670d5cfb97a03fa573d036b1c7b2f1bb03d0dd09d5d24488fa1df1d4cd

(used here): the receipt the lean-pkg registry holds for this package, which the lines above read. SHA-256 is of the file as committed.

Reproduce

• Lean toolchain: leanprover/lean4:v4.32.0.
• Mathlib: 81a5d257c8e410db227a6665ed08f64fea08e997 (lake-manifest.json).

git clone https://github.com/chenle02/total-coloring-lean
cd total-coloring-lean
git checkout c025d20a182644bbacdd96165c93e1b8b2a403c6   # the commit the build check binds
lake exe cache get
lake build

Expected: #print axioms on any declaration above reports a subset of {Classical.choice, Quot.sound, propext} (the union the build check records); sorryAx never appears.

Citation

Le Chen and Songling Shan. Total Coloring Lean. Version 0.2.0. doi:10.5281/zenodo.23452513.

See CITATION.cff.

License

Released under Apache-2.0; see LICENSE.

Acknowledgments

Developed and verified with lean-pkg (doi:10.5281/zenodo.23272098).