Skip to content

Getting started

Prerequisites

Install elan, Git, and a C/C++ toolchain suitable for Lean. The repository pins Lean and mathlib to version v4.32.0; do not substitute a floating toolchain.

Clone and build

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

lake exe cache get downloads compatible mathlib build artifacts. The first build without a useful cache can take substantially longer.

Confirm the public entrypoints

The following file is compiled by CI, so the example cannot silently drift.

/-
Copyright (c) 2026 Le Chen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Le Chen
-/
import TotalColoring

#check TotalColoring.InAuxiliaryClass
#check TotalColoring.ExtensionPalette
#check TotalColoring.HasValidRainbowColoring
#check TotalColoring.MinimalExtraction.hasValidRainbowColoring_of_inAuxiliaryClass
#check TotalColoring.Auxiliary.Extension.decode_valid
#check TotalColoring.Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass
#check TotalColoring.Auxiliary.PairSingletonWitness
#check TotalColoring.Auxiliary.PairSingletonWitness.auxiliaryGraph
#check TotalColoring.Auxiliary.PairSingletonWitness.extension
#check TotalColoring.Auxiliary.PairSingletonWitness.classEdge_mem_distinguishedEdgeSet
#check TotalColoring.Auxiliary.PairSingletonWitness.degree_some_eq
#check TotalColoring.Auxiliary.PairSingletonWitness.card_add_degree_none_eq_two_mul_distinguished_card
#check TotalColoring.Auxiliary.PairSingletonWitness.isAuxiliaryClassMember_of_class_count_and_bounds
#check TotalColoring.Auxiliary.PairSingletonWitness.isAuxiliaryClassMember_of_highDegree
#check TotalColoring.Auxiliary.EquitableIndependentPartition
#check TotalColoring.Auxiliary.EquitableIndependentPartition.toPairSingletonWitness
#check TotalColoring.Auxiliary.EquitableIndependentPartition.distinguished_card
#check TotalColoring.Auxiliary.EquitableIndependentPartition.highDegreeWitness_inAuxiliaryClass
#check TotalColoring.Auxiliary.EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition
#check TotalColoring.MatchingLowerBound.exists_matchingGraph_edgeFinset_card_ge
#check TotalColoring.MatchingLowerBound.exists_complement_matchingGraph_edgeFinset_card_ge
#check TotalColoring.MatchingLowerBound.exists_complement_matchingGraph_edgeFinset_card_eq
#check TotalColoring.Auxiliary.exists_pairSingletonWitness_of_highDegree
#check TotalColoring.Auxiliary.exists_valid_assignment_of_highDegree_nonempty
#check TotalColoring.exists_valid_assignment_of_isEmpty
#check TotalColoring.exists_valid_assignment_of_highDegree

-- Historical proof branch `agent/independent-seed-endpoint`, source commit
-- `cc4dd7ae1d858ea0583549f88707952e2414bf60`, tree
-- `9af6a84e1305aed9a0156dcd59c279de792dea4a`.  These declarations are on
-- current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`,
-- tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`.
#check TotalColoring.exists_valid_assignment_of_independentSeedPeel
#check TotalColoring.exists_valid_assignment_of_maxDegreeIndependentSeedPeel

-- Historical proof branch `agent/total-independent-selector-decoder`, source commit
-- `d008514c7a1cf834007bf0bd8de0d10a93926711`, tree
-- `1847934c78da03fe80bb67236868700c79016129`.  These declarations are on
-- current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`,
-- tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`.
#check TotalColoring.SelectorCorePeelCertificate
#check TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel
#check TotalColoring.exists_valid_assignment_of_maxDegreeTotalIndependentSelectorPeel
#check TotalColoring.AlternatingRainbowPathSelectorCertificate
#check TotalColoring.exists_valid_assignment_of_alternatingRainbowPathSelector
#check TotalColoring.exists_valid_assignment_of_maxDegreeAlternatingRainbowPathSelector

-- Historical stacked branch `agent/partial-edge-selector-normalization`, source
-- commit `c3dbe69c15f96e3c71d8481ae4e517ee2f4fdbf2`, tree
-- `11007a4aa381984a8d66aa1db297312cebe8d8b5`.  These declarations are on
-- current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`,
-- tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`.
#check TotalColoring.EdgeAssignment.ValidOutside
#check TotalColoring.partialEdgeSelectorEdgeAssignment_valid
#check TotalColoring.partialEdgeSelectorAssignment_valid
#check TotalColoring.totalIndependentSelectorAssignment_valid_of_validOutside
#check TotalColoring.PartialEdgeSelectorNormalization
#check TotalColoring.partialEdgeSelectorNormalization_of_valid
#check TotalColoring.maxDegreePartialEdgeSelectorNormalization_of_valid

-- Merged into `main` by PR #13 (commit `dc6e3a4b7510b3d2df4fb5074afaee2027e9b442`,
-- 2026-07-20); present on current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`,
-- tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`; exact endpoint
-- vertex-coloring interface only.  Physical donor-matching existence and
-- unrestricted total-coloring existence remain outside this declaration.
#check TotalColoring.adaptedSpareVertexColor_proper_iff
#check TotalColoring.Certificate.checkExtension_sound

Run it directly with:

lake env lean docs/examples/Quickstart.lean

Use the library downstream

Import the umbrella module when exploring:

import TotalColoring

For a smaller dependency surface, import the module that owns the declaration you need. The theorem index lists the principal public entrypoints and source modules.

Build the documentation

python3 -m venv .venv-docs
. .venv-docs/bin/activate
python -m pip install --requirement requirements-docs.txt
bash scripts/build-docs.sh

The generated site is in site/. Preview it with:

python -m http.server --directory site 8000

Then open http://127.0.0.1:8000/.

Before contributing

Read CONTRIBUTING.md and the stricter repository contract in AGENTS.md. The complete gate includes lake build, leanchecker, the forbidden-token scan, and both Git diff checks.