First-party checked source

Source for Brooks’s Theorem

This pinned Lean source formalizes the following mathematical result: 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. Download the complete checked closure or open its single Lean endpoint to study the proof or develop an extension.

Immutable source commit: 4d3072bdd6694411d89525c31194aea124123ea7

Checked source + agent continuation package · 1 Lean file · 1 evidence record · Download ZIP

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Formalization at a glance

What is checked—and how much source supports it

Browse the counted source

Declarations covered by evidence: 1
First-party Lean files: 1
Lean source lines: 3,373
Main recorded file: 3,373 lines

How counting works: Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence; it is not a count of every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Brooks’s Theorem

AtlasKnownTheorems.BrooksTheorem.brooksTheorem

This hash-matched file is the complete first-party Lean closure for the theorem.

Commit: 4d3072bdd6694411d89525c31194aea124123ea7
Main Lean file: AtlasKnownTheorems/BrooksTheorem/Basic.lean
Main-file footprint: 3,373 lines
File SHA-256: sha256:a2b8279e72319b6ee50df38a58b0d46d6757fb55086d01a8cb5bcd1f04da6847
Complete Lean closure: 1 file · 3,373 lines
Toolchain: leanprover/lean4:v4.29.1

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Advameg, Inc. notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

This theorem's complete first-party Lean closure is the single main file shown above: 3,373 lines. External Mathlib modules remain dependency-locked separately.

Source hashMatches checked record

Lean buildPassed in recorded evidence

LicenseApache-2.0 · Advameg, Inc.

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Advameg, Inc.; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.