Even graphs are edge-disjoint… to Near-perfect triangle packings…

TheoremEven graphs are edge-disjoint unions of cycles#

Decomposes every finite loopless edge set with even degree at each vertex into edge-disjoint simple cycles and derives a simultaneous fixed-point-free pairing of incident edges.

Quoted from the card LeanPool/projects/even-graph-cycle-decomposition.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanFinset.exists_cycleDecomp · Finset.exists_edge_pairing_of_even

DefinitionExtended Demazure Product on ASP Permutations#

Formalizes the extended Demazure product on almost-sign-preserving integer permutations, including slipface models, residuals, greedy and stingy characterizations, reduction theorems, adjacent-transposition formulas, and 321-avoiding factorization results.

Quoted from the card LeanPool/projects/demazure-product.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 9 main results, each with its informal statement quoted from the card. The scan finds 9 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.DemazureProduct.AspPerm.star

TheoremFinite hypergraph rounding and the asymptotic triangle-packing gap#

Formalizes a finite ceiling-carrying nibble theorem for uniform hypergraphs that are near-regular outside a small exceptional set and have suitably bounded codegrees, and derives the uniform subquadratic gap between fractional and integral triangle packing in finite graphs, together with its fractional-cover formulation.

Quoted from the card LeanPool/projects/asymptotic-triangle-packing.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.AsymptoticTrianglePacking.trianglePackingGap

TheoremFinite max-flow / min-cut#

Develops finite networks with real nonnegative capacities, proves cut-flow weak duality and maximum-flow attainment, and derives max-flow/min-cut equality by an augmenting-path argument.

Quoted from the card LeanPool/projects/finite-max-flow-min-cut.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanContrib.MaxFlowMinCut.maxflow_eq_mincut

TheoremFrontierMath Ramsey Hypergraphs#

Formalizes lower bounds for the Brian-Larson hypergraph extremal function H(n), including a uniform 26/25 improvement over the recursive benchmark k_n for n ≥ 15 and a Lubell-frame asymptotic lower bound.

Quoted from the card LeanPool/projects/frontiermath-open-hypergraphs.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanHypergraphLowerBound.thm_main_H_lower_bound

DefinitionFundamental groups of finite connected graphs#

Constructs the standard interval-cell realization of a finite connected directed multigraph and proves that its topological fundamental group is a free group of rank E - V + 1. The proof uses an explicit spanning-tree basis and develops a verified path-lifting cover, a contraction of the covering tree, root-change equivalences, the tree/triviality criterion, and the corresponding free-abelian result.

Quoted from the card LeanPool/projects/finite-graph-fundamental-group.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanFiniteGraphFreeGroup.graphTopologicalFundamentalGroupEquiv

TheoremGenus-Zero Pairings and Catalan Numbers#

Formalizes the finite combinatorics behind the genus-zero term of the Wigner semicircle law: a pairing of Fin (2n), viewed as a fixed-point-free involution, has genus zero (total cycle count of the rotation product maximal) exactly when it is noncrossing, and these genus-zero pairings are counted by the Catalan number Cₙ. The Catalan recurrence is obtained from an explicit equivalence decomposing a noncrossing pairing by the partner of vertex 0 into independent inside and outside pairings.

Quoted from the card LeanPool/projects/semicircle-catalan.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
Leancard_noncrossingPairing_eq_catalan · Pairing.genus_zero_count

TheoremGeometric Four-Colorings of the Moser Lattice and Ring#

Formalizes the two explicit parity colorings from Dúcz's 2026 note on the Moser lattice. The development derives the exact quadratic norm formula, proves that the integer-coordinate embedding is faithful, proves both colorings proper and geometric on the entire lattice, and descends them through localization by powers of three to the Moser ring. As a structural corollary, every unit-distance graph realized entirely in the Moser ring is four-colorable. The uniqueness classification of geometric four-colorings and the chromatic number of the full Euclidean plane are not claimed.

Quoted from the card LeanPool/projects/moser-lattice-colorings.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.MoserLatticeColorings.MoserRing.both_colorings_are_geometric

TheoremGraph removal and extremal stability#

Formalizes the graph removal lemma for every fixed graph, Füredi's sharp stability inequality and Erdős–Simonovits stability for colourable forbidden graphs. A bridge theorem shows that near-extremal graphs with few labelled forbidden copies are close to a complete multipartite graph.

Quoted from the card LeanPool/projects/graph-removal-extremal-stability.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanTuranStability.stability · RemovalLemma.graph_removal

TheoremThe Hajnal–Szemerédi theorem on equitable vertex colourings#

Every finite simple graph of maximum degree at most r admits a proper colouring with r + 1 colours whose class sizes differ by at most one. When the vertex count is s(r + 1), every class can have exactly s vertices. The proof follows the Kierstead–Kostochka argument, preserving finite-subgraph and arbitrary-palette recolouring, reachability, terminal-class and discharging infrastructure. The polynomial-time algorithm from Section 3 is outside the imported scope.

Quoted from the card LeanPool/projects/hajnal-szemeredi.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanHajnalSzemeredi.hajnalSzemeredi · HajnalSzemeredi.hajnalSzemeredi_exact

TheoremHard-sphere Mayer NBC identity and fork-packing volume bound#

A kernel-checked Lean formalization of the exact no-broken-circuit volume identity for hard-sphere Mayer cluster integrals and the stronger dimension-three fork-packing upper bound for each tree-owned NBC region. The development proves finite broken-circuit cancellation, the measurable finite-region decomposition, the anchored Euclidean product-measure theorem, and its explicit flat-coordinate transport. Its geometric result is the attachment-aware estimate Vol(NBC_T) <= (17/32)^hardSphereNu T * hardSphereKappa^(k-1), where hardSphereNu T is the maximum cardinality of a packing of pairwise vertex-disjoint, order-compatible forks in T. A formal fork is an ordered triple (a,b,c) with a < b < c, center a, leaves b,c, and tree edges {a,b} and {a,c}. The central contribution is the complete pointwise-to-integral bridge together with the orientation-aware measure-preserving factorization that realizes the per-fork volume suppression.

Quoted from the card LeanPool/projects/hs-virial-nbc-identity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanPalomarHS.main_result · PalomarHS.nbc_region_real_volume_le_fork_factor

TheoremHäggkvist–Janssen list edge colouring of complete graphs#

Proves that arbitrary lists of at least n colours on the edges of a complete graph with n vertices admit a proper list edge colouring. The proof constructs and proves uniqueness of the local rank certificate, identifies a nonzero extended-star polynomial coefficient, and applies Mathlib's combinatorial Nullstellensatz. This is an alternative proof presentation, not a literal translation of the article's argument. The conclusion uses Mathlib's actual edge type and line-graph colouring, with no certificate hypothesis and no restriction on the colour universe. This formalizes a classical theorem, not a new bound or a solution of the general list-edge conjecture.

Quoted from the card LeanPool/projects/list-edge-coloring-complete.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.ListEdgeColoringComplete.exists_listEdgeColoring_complete

TheoremKahn–Kalai expectation-threshold theorem#

Formalizes Tran and Vu's short proof of the Park–Pham theorem resolving the Kahn–Kalai expectation-threshold conjecture. For an ℓ-bounded family of subsets of a finite ground set, it proves the strengthened covering theorem with the explicit constant L = 1000 and derives the threshold bound p_c(F) ≤ K q(F) log₂ ℓ with the explicit witness K = 100000. The supporting library develops finite-set cover cost, level-density, double-counting, binomial-tail, and numeric estimates.

Quoted from the card LeanPool/projects/kahn-kalai.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • KahnKalai.covering_theorem (theorem; a main declaration), declared in LeanPool/KahnKalai.lean, line 34: “If ℓ ≤ N, p lies in [0, 1], and an ℓ-bounded family H has cover cost at least 1/2 - 2^(-(ℓ+2)), then its upset has at least (2/3 + 2^(-(ℓ+2))) choose(N, m) members of cardinality m, where m = floor(1000 p N log₂(ℓ+1)). For m ≤ N this is the corresponding level-density bound; for N < m both cardinalities are zero.”
  • KahnKalai.park_pham (theorem; a main declaration), declared in LeanPool/KahnKalai.lean, line 49: “There is an absolute positive constant K such that every ℓ-bounded finite family with ℓ at least two satisfies p_c(F) ≤ K q(F) log₂ ℓ; the proof supplies K = 100000.”
Project
Sources
LeanKahnKalai.covering_theorem · KahnKalai.park_pham

TheoremKnown Bounds for the Hadwiger-Nelson Problem#

Formalizes the currently known bounds 5 <= chi(R^2) <= 7 for the chromatic number of the Euclidean plane. The upper bound constructs an explicit Isbell-style seven-coloring. The lower bound checks Parts' 481-vertex coloring certificate, develops a finite doubled triangular-lattice forcing gadget, proves its exact Euclidean embedding, and closes the four-color contradiction with a spindle construction. The exact chromatic number remains open.

Quoted from the card LeanPool/projects/hadwiger-nelson-bounds.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanHadwigerNelsonBounds.hadwiger_nelson_known_bounds

TheoremKolokolnikov's ACMAX conjecture#

Proves that every simple graph on n ≥ 4 vertices with 2(n−2) edges has algebraic connectivity at most 2, attained by the complete bipartite graph K₂,ₙ₋₂. Develops Laplacian test-vector bounds, sparse cut certificates, and non-backtracking walk estimates used in the proof.

Quoted from the card LeanPool/projects/acmax-conjecture.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanACMax.acmax_conjecture

DefinitionLine-graph colourings and matching decompositions#

Connects Mathlib line-graph colourings to palette-indexed partitions of actual graph edges into Mathlib matching subgraphs. Both conversions are inverse, preserve each matching exactly, and allow empty colours without a default colour or a finiteness assumption. An edge equivalence yields exact edge accounting: natural-number counts require only finite edges and a finite palette, while indexed cardinal counts allow arbitrary vertices, edges, and palettes. This is classical representation interoperability, not a new colouring bound or a claim of priority.

Quoted from the card LeanPool/projects/line-graph-colouring-matching.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanSimpleGraph.lineGraphColoringEquivMatchingDecomposition

TheoremLinear finite bipartization costs force countable graph colourings#

A graph whose every finite subgraph on m vertices can be made bipartite by deleting at most C m edges has a proper colouring by natural numbers. Consequently the maximum finite-subgraph bipartization cost h_G(n), divided by n, tends to infinity for every graph that is not countably colourable, including every graph with chromatic cardinal aleph-one. The development preserves finite edge costs, rooted-pattern extension costs, closure chains, probability laws on Boolean products, finite minimax, Hilbert-space classes, and colouring along well-founded orders. It answers the limit question of Erdős Problem 111; it does not determine the exact growth of h_G.

Quoted from the card LeanPool/projects/erdos111-bipartization.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanErdos111.countably_colorable_of_linear

TheoremMaxima of Coxeter frieze patterns are Fibonacci numbers#

Formalizes the claim that the sequence of maxima of values of (Coxeter) arithmetic frieze patterns is the Fibonacci sequence, using a correspondence between arithmetic frieze patterns and n-flutes.

Quoted from the card LeanPool/projects/frieze-patterns.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
Leanmain3 · FluteBounded · glideSymm · translationInvariance

TheoremNash-Williams–Tutte tree packing and arboricity#

A finite simple graph on a nonempty vertex type has k edge-disjoint spanning trees exactly when every partition into m nonempty parts has at least k(m − 1) crossing edges. The development also proves the Nash-Williams characterization of covering the edges by k forests, and that every finite nonempty 2k-edge-connected simple graph has k edge-disjoint spanning trees. It preserves the general forest exchange lemma and supporting reachability and edge-counting infrastructure, using Mathlib's graph definitions.

Quoted from the card LeanPool/projects/nash-williams-tutte.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanNashWilliamsTutte.tree_packing · NashWilliamsTutte.arboricity

TheoremNear-perfect triangle packings from sum-zero triples#

Records a reusable formalization byproduct accompanying Paper III: pairwise edge-disjoint triangles in any finite complete graph such that every vertex is incident to at most three uncovered edges, using a cyclic-group sum-zero triple system, with a bridge to Mathlib's SimpleGraph API.

Quoted from the card LeanPool/projects/erdos81-paper-iii-sum-zero-triangles.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanSumZeroTriangles.exists_simpleGraph_triangle_packing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.