Optimal Pebbling Number of the… to Vizing's theorem and equitable…
TheoremOptimal Pebbling Number of the Hypercube#
Formalizes that the optimal pebbling number of the n-dimensional hypercube Q_n is Theta((4/3)^n). Builds a weight-function lower bound of (4/3)^n and a probabilistic recursive upper bound C * (4/3)^n with an explicit constant, combining them into a two-sided big-Theta witness.
Quoted from the card LeanPool/projects/pebbling-hypercube.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.
PebblingLean.Hypercube.Paper.optimalPebblingNumber_theta(theorem; a main declaration), declared in LeanPool/PebblingLean/Paper.lean, line 177: “The optimal pebbling number of Q_n has order (4/3)^n: there is a positive constant C with (4/3)^n <= o(Q_n) <= C * (4/3)^n for all n.”PebblingLean.Hypercube.Paper.lower_bound(theorem), declared in LeanPool/PebblingLean/Paper.lean, line 145: “The optimal pebbling number of Q_n is at least (4/3)^n, proved by a weight-function argument summing one-pebble weights over the cube.”PebblingLean.Hypercube.Paper.upper_bound(theorem), declared in LeanPool/PebblingLean/Paper.lean, line 160: “The optimal pebbling number of Q_n is at most C * (4/3)^n for an explicit constant C, via a probabilistic recursive splitting construction.”
Project
- Authors: Lior Pachter.
- Source: Optimal pebbling number of the hypercube by Lior Pachter.
- Project repository: pachterlab/P_2026_2.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 05C57.
- In Lean Pool: LeanPool/PebblingLean, from the card LeanPool/projects/pebbling-hypercube.yaml.
Sources
TheoremPólya's enumeration theorem#
Formalizes Pólya's enumeration theorem counting orbits of colorings under a group action.
Quoted from the card LeanPool/projects/polya-enumeration-theorem.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.
LeanPool.PolyaEnumerationTheorem.polya_theorem(theorem; a main declaration), declared in LeanPool/PolyaEnumerationTheorem/Basic.lean, line 279: “Counts distinct colorings of a finite set under a group action by averaging powers of the number of colors over cycle indices.”
Project
- Authors: Luka Opravš.
- Project repository: Luka-O/polya-enumeration-theorem.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2024 Luka-O”.
- MSC2020: 05A15, 20B30.
- In Lean Pool: LeanPool/PolyaEnumerationTheorem, from the card LeanPool/projects/polya-enumeration-theorem.yaml.
Sources
TheoremSabidussi's compatibility conjecture for Eulerian multigraphs#
Formalizes Sabidussi's compatibility conjecture for finite labelled endpoint multigraphs with loops and parallel edges, where a loop contributes two half-edge incidences to the degree of its vertex. Given an Euler tour and minimum degree at least four, the main theorem constructs a partition of all edges into nonempty, edge-connected, 2-regular ordinary circuits such that consecutive edges of the Euler tour never lie in the same circuit. The proof runs a four-colour (F_2^2) algebra over the cyclic transition word, uses an odd balancing parity lemma to choose compatible local frames, and transports the resulting colouring back to a compatible ordinary circuit decomposition.
Quoted from the card LeanPool/projects/sabidussi.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.
Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary(theorem; a main declaration), declared in LeanPool/Sabidussi/OrdinaryCircuit.lean, line 451: “For any finite endpoint multigraph with an Euler tour and minimum degree at least four, the edges partition into ordinary, nonempty, connected, 2-regular circuits that are compatible with the tour: no circuit contains two consecutive tour edges.”Sabidussi.LoopMultigraph.loop_sabidussi_compatibility(theorem), declared in LeanPool/Sabidussi/LoopGraphBridge.lean, line 133: “The same compatibility statement phrased with the intrinsic even-edge-set circuit decomposition, from which the ordinary-circuit form is derived.”
Project
- Authors: Nikolay Ulyanov.
- Source: Graph Puzzles III.1: A proof of Sabidussi's compatibility conjecture by Nikolay Ulyanov, https://github.com/gexahedron/sabidussi-lean/blob/032e640df0cc41d4d3d217f7c68628ab19cb3767/sabidussi_proof.pdf.
- Project repository: gexahedron/sabidussi-lean.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05C45.
- In Lean Pool: LeanPool/Sabidussi, from the card LeanPool/projects/sabidussi.yaml.
Sources
TheoremThe sharp finite-field Nikodym exponent#
Proves a lower bound for Nikodym sets over arbitrary finite fields and a matching exponent upper construction over sufficiently large prime fields, using interpolation, algebraic degree bounds, and multiquadratic constructions.
Quoted from the card LeanPool/projects/nikodym.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.
Nikodym.card_ge_pow_sub(theorem; a main declaration), declared in LeanPool/Nikodym/Nikodym/Main.lean, line 55: “Every Nikodym set in dimension d ≥ 2 over a finite field of size q has size at least q^d − (8d²+1)q^(d−2^(1−d)).”Nikodym.exists_isNikodym_card_le(theorem; a main declaration), declared in LeanPool/Nikodym/Nikodym/Main.lean, line 64: “For every positive ε and dimension d ≥ 2, sufficiently large prime fields admit a Nikodym set of size at most q^d − q^(d−2^(1−d)−ε).”
Project
- Authors: Ting-Wei Chao, Zach Hunter, Cosmin Pohoata, Hung-Hsun Hans Yu, Shengtong Zhang.
- Project repository: shengtongzhang-alt/nikodym, at commit 38d16dcd.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05B25, 11T99.
- In Lean Pool: LeanPool/Nikodym, from the card LeanPool/projects/nikodym.yaml.
Sources
TheoremShelah's bound for the Hales–Jewett numbers#
Proves the Hales–Jewett theorem with Shelah's primitive recursive bound. The proof is by induction on the alphabet; to add a letter it finds a subspace on which the coloring is insensitive to replacing the new letter by an old one, building each dimension of the subspace from a line given by the pigeonhole principle. This gives an explicit recursion shelahBound k r for the dimension, which is proved to be below the fifth level of the Ackermann function, so every r-coloring of the words of length n ≥ A(5, 2k + r) over k ≥ 1 letters has a monochromatic combinatorial line.
Quoted from the card LeanPool/projects/shelah-hales-jewett.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.
Combinatorics.Line.exists_mono_of_shelahBound_le(theorem; a main declaration), declared in LeanPool/ShelahHalesJewett/HalesJewett.lean, line 190: “Over a nonempty finite alphabet α, every coloring with κ colors of the words indexed by a finite type ι has a monochromatic combinatorial line when |ι| ≥ shelahBound |α| |κ|.” Its source, as the card gives it: “The Hales–Jewett theorem with Shelah's bound.”Combinatorics.Subspace.exists_insensitive(theorem), declared in LeanPool/ShelahHalesJewett/HalesJewett.lean, line 65: “For letters a and b and a finite type η, in a cube of dimension insensitiveBound every coloring has an η-dimensional subspace on which replacing a by b in any coordinates does not change the color.” Its source, as the card gives it: “Shelah's insensitivity lemma.”Combinatorics.Line.shelahBound_lt_ack(theorem; a main declaration), declared in LeanPool/ShelahHalesJewett/Ackermann.lean, line 88: “shelahBound k r < A(5, 2k + r), where A is the Ackermann function.”Combinatorics.Line.exists_mono_of_ack_le(theorem; a main declaration), declared in LeanPool/ShelahHalesJewett/Ackermann.lean, line 98: “Over a nonempty finite alphabet of k letters, every coloring with r colors of the words of length n ≥ A(5, 2k + r) has a monochromatic combinatorial line.”
Project
- Authors: Gabriel Dahia.
- Source: Primitive recursive bounds for van der Waerden numbers by Saharon Shelah, doi:10.1090/S0894-0347-1988-0929498-X.
- Project repository: gdahia/ShelahHalesJewett, at commit 8a91fc0e.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05D10, 03D20.
- In Lean Pool: LeanPool/ShelahHalesJewett, from the card LeanPool/projects/shelah-hales-jewett.yaml.
Sources
TheoremThe smallest critical set in a Latin square#
Proves that every partial Latin square of order n with fewer than floor(n²/4) filled cells has an even number of completions. Consequently every defining set has at least floor(n²/4) entries, and the two corner triangles in the cyclic square attain this bound as a critical set. Includes general results on matrix minors, square-zero ideals, and square-free polynomial coefficients.
Quoted from the card LeanPool/projects/latin-quarter.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.
LatinQuarter.Textbook.completions_even(theorem; a main declaration), declared in LeanPool/LatinQuarter/Textbook.lean, line 127: “Every set of fewer than floor(n²/4) filled triples of an order-n partial Latin square has an even number of labelled Latin-square completions.”LatinQuarter.Textbook.scs_eq_quarter(theorem; a main declaration), declared in LeanPool/LatinQuarter/Textbook.lean, line 245: “For every positive n, the smallest critical-set size among all Latin squares of order n, and the smallest critical-set size in the cyclic Latin square, both equal floor(n²/4).”LatinQuarter.defining_set_lower_bound(theorem), declared in LeanPool/LatinQuarter/LowerBound.lean, line 51: “Every defining set in every labelled Latin square of order n has at least floor(n²/4) cells.”LatinQuarter.cornerSet_isCritical(theorem), declared in LeanPool/LatinQuarter/Main.lean, line 37: “For every positive n, the two opposite corner triangles form a critical set in the cyclic Latin square.”
Project
- Authors: Richard Bean.
- Source: arXiv:2610.18199.
- Project repository: RichardBean/latin-quarter-lean, at commit 9997439d.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05B15.
- In Lean Pool: LeanPool/LatinQuarter, from the card LeanPool/projects/latin-quarter.yaml.
Sources
TheoremSplit, cograph and threshold graph structures#
Connects split partitions, cotrees and threshold creation sequences on Mathlib SimpleGraph. Proves the finite forbidden-induced-subgraph characterizations, split iff chordal and co-chordal, and completeness of cotrees and creation sequences. Supplies certificate-preserving operations, twins and nonempty union/join decompositions for cographs, maximum-clique split partitions, and induced/isomorphic transport of existing chordal elimination orders and clique trees. Classical graph theory is formalized; no new mathematical theorem, canonical certificate or recognition-time bound is claimed.
Quoted from the card LeanPool/projects/structural-graph-classes.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 10 main results, each with its informal statement quoted from the card. The scan finds 10 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.
SimpleGraph.isSplit_iff_forbidden_induced_subgraphs(theorem), declared in LeanPool/StructuralGraphClasses/ForbiddenCharacterization.lean, line 49: “A finite graph is split iff it contains no induced 2K2, C4 or C5.” Its source, as the card gives it: “Földes and Hammer, Split graphs (1977).”SimpleGraph.isSplit_iff_isChordal_and_compl(theorem), declared in LeanPool/StructuralGraphClasses/SplitExtension.lean, line 214: “A finite graph is split iff both it and its complement are chordal.” Its source, as the card gives it: “Földes and Hammer, Split graphs (1977).”SimpleGraph.isCograph_iff_nonempty_cotreeRepresentation(theorem), declared in LeanPool/StructuralGraphClasses/CotreeCompleteness.lean, line 82: “A finite graph is P4-free iff it is isomorphic to the graph of a cotree, whose constructors are empty, singleton, disjoint union and join.” Its source, as the card gives it: “Seinsche (1974), doi:10.1016/0095-8956(74)90063-X; Corneil, Lerchs and Stewart Burlingham (1981), doi:10.1016/0166-218X(81)90013-5.”SimpleGraph.isThreshold_iff_isSplit_and_isCograph(theorem), declared in LeanPool/StructuralGraphClasses/Cotree.lean, line 137: “A graph has a split partition with nested independent-side neighbourhoods iff it is both split and P4-free. No finiteness is required.” Its source, as the card gives it: “Classical threshold characterization; local Threshold.lean and Cotree.lean.”SimpleGraph.isThreshold_iff_forbidden_induced_subgraphs(theorem), declared in LeanPool/StructuralGraphClasses/ForbiddenCharacterization.lean, line 70: “A finite graph is threshold iff it contains no induced 2K2, C4 or P4.” Its source, as the card gives it: “Chvátal and Hammer (1977), doi:10.1016/S0167-5060(08)70731-3.”SimpleGraph.isThreshold_iff_nonempty_creationRepresentation(theorem; a main declaration), declared in LeanPool/StructuralGraphClasses/ThresholdCreation.lean, line 228: “A finite graph is threshold iff it is isomorphic to a graph constructed from the empty graph by successively adding an isolated or universal vertex.” Its source, as the card gives it: “Classical threshold creation characterization; local ThresholdCreation.lean.”SimpleGraph.IsCograph.exists_twins(theorem), declared in LeanPool/StructuralGraphClasses/CographTwins.lean, line 120: “A finite cograph with at least two vertices has two distinct vertices with identical adjacency outside their pair, whether adjacent or not.” Its source, as the card gives it: “Cotree induction in CographTwins.lean; classical cograph structure.”SimpleGraph.IsCograph.exists_union_root(theorem), declared in LeanPool/StructuralGraphClasses/CographTwins.lean, line 177: “A finite cograph that is not preconnected admits a cotree representation with a union root and two nonempty children. This is an existence claim, not a claim about every unreduced cotree.” Its source, as the card gives it: “Seinsche decomposition and CotreeRepresentation constructors.”SimpleGraph.IsCograph.exists_join_root(theorem), declared in LeanPool/StructuralGraphClasses/CographTwins.lean, line 189: “A preconnected finite cograph with at least two vertices admits a cotree representation with a join root and two nonempty children.” Its source, as the card gives it: “Seinsche decomposition and CotreeRepresentation constructors.”SimpleGraph.IsSplit.exists_partition_with_maximum_clique(theorem), declared in LeanPool/StructuralGraphClasses/SplitDecomposition.lean, line 72: “Every finite split graph admits a split partition whose clique part has maximum cardinality. Such a partition need not be unique.” Its source, as the card gives it: “Direct finite maximization argument in SplitDecomposition.lean.”
Project
- Authors: Juan Pablo Traverso Gianini.
- Source: Structural graph classes, original Lean development checkpoint, https://github.com/jtraverso/lean-pool/tree/c431fcecd3c963bcca643c379d807260585711b8/LeanPool/StructuralGraphClasses.
- Project repository: jtraverso/lean-pool, at commit c431fcec.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05C75, 05C05.
- In Lean Pool: LeanPool/StructuralGraphClasses, from the card LeanPool/projects/structural-graph-classes.yaml.
Sources
TheoremStrict Beck–Fiala rounding for incidence matrices#
Proves the rational integer-making form of Beck–Fiala rounding for finite zero-one incidence matrices with column degree bounded by a positive t. Every row has discrepancy strictly less than t, and initially integral coordinates are preserved. Includes the necessity of the positive-bound hypothesis. This is distinct from the Komlós discrepancy bound and from the non-strict hyperedge-selection rounding used in triangle packing.
Quoted from the card LeanPool/projects/beck-fiala-matrix.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.
BeckFialaMatrix.exists_rounding(theorem; a main declaration), declared in LeanPool/BeckFialaMatrix/Basic.lean, line 380: “Given a finite zero-one integer matrix with at most t ones per column, t at least one, and a rational vector in the unit cube, there is a zero-one integer vector whose discrepancy in every row is strictly less than t.” Its source, as the card gives it: “Rational unit-cube integer-making form with the stated strict discrepancy bound.”BeckFialaMatrix.exists_rounding_preserving_integral(theorem), declared in LeanPool/BeckFialaMatrix/Basic.lean, line 364: “The strict rounding can additionally be chosen to leave every initially integral coordinate unchanged.” Its source, as the card gives it: “Strengthened conclusion of the floating-coordinate proof in the pinned source.”BeckFialaMatrix.zero_bound_counterexample(theorem), declared in LeanPool/BeckFialaMatrix/Basic.lean, line 392: “The same universally quantified strict rounding claim without the assumption t at least one is false, already for a one-by-one zero matrix with t equal to zero.” Its source, as the card gives it: “Boundary-condition witness in the pinned formalization.”
Project
- Authors: Juan Pablo Traverso Gianini.
- Source: "Integer-making" theorems by József Beck, Tibor Fiala, doi:10.1016/0166-218X(81)90022-6, https://github.com/jtraverso/lean-pool/blob/523a4ae71168258f9142d70bccf650a140355650/LeanPool/BeckFialaMatrix/Basic.lean.
- Project repository: jtraverso/lean-pool, at commit 523a4ae7.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05D40.
- In Lean Pool: LeanPool/BeckFialaMatrix, from the card LeanPool/projects/beck-fiala-matrix.yaml.
Sources
TheoremSuperexponential lower bounds for multicolor triangle Ramsey numbers#
Resolves Erdős problem 183 by proving that the k-color triangle Ramsey number has a k-th root tending to infinity. The development constructs saturated palette families and recursive edge colorings, derives an explicit superexponential lower bound, and proves matching order-of-growth bounds for the logarithm of the Ramsey number.
Quoted from the card LeanPool/projects/multicolor-triangle-ramsey.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.
ErdosProblems.MulticolourTriangleRamsey.erdos_183(theorem), declared in LeanPool/MulticolorTriangleRamsey.lean, line 3106: “The k-th root of the k-color triangle Ramsey number tends to infinity, resolving Erdős problem 183.”ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit(theorem; a main declaration), declared in LeanPool/MulticolorTriangleRamsey.lean, line 3113: “For every k at least two, the k-color triangle Ramsey number is at least ((k^(1/3))/(6 exp(38) log k))^k, and its k-th root tends to infinity.”ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_log_isTheta(theorem), declared in LeanPool/MulticolorTriangleRamsey.lean, line 3037: “The logarithm of the k-color triangle Ramsey number has order k log k.”
Project
- Authors: OpenAI.
- Source: Ten Advances in Mathematics and Theoretical Computer Science by OpenAI.
- Project repository: openai/ten-proofs, at commit 94bc0feb.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05D10, 05C55.
- In Lean Pool: LeanPool/MulticolorTriangleRamsey, from the card LeanPool/projects/multicolor-triangle-ramsey.yaml.
Sources
TheoremThe ten minimum universal collections of MacMahon cubes#
Classifies all minimum universal inventories of six-coloured MacMahon cubes. A universal inventory can build a two-by-two-by-two model of every cube variety, with matching exterior faces and eight distinct physical copies. The minimum inventory size is twelve, exactly ten labelled inventories attain it, and they are precisely the two-triangle collections in Conway's tableau. Natural-number multiplicities are allowed; every minimum inventory has no repeated variety. The tableau has zero diagonal; its thirty off-diagonal entries are the varieties. The development also verifies all proper signed-axis rotations, the thirty varieties, all six-colour face assignments, and the equivalence of corner matching with physical face matching. This resolves Johnson and Roldán's Conjectures 4 and 8 (arXiv:2407.13208v1), with a stronger multiset conclusion.
Quoted from the card LeanPool/projects/macmahon-min-universal-sets.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 10 main results, each with its informal statement quoted from the card. The scan finds 10 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.
MacMahon.minimum_size(theorem; a main declaration), declared in LeanPool/MacMahon/Theorems.lean, line 86: “Twelve is the attained minimum size of a universal physical inventory.”MacMahon.physical_minimum(theorem), declared in LeanPool/MacMahon/Theorems.lean, line 62: “Every universal physical inventory has at least twelve cubes.”MacMahon.physical_exactly_ten(theorem; a main declaration), declared in LeanPool/MacMahon/Theorems.lean, line 80: “Exactly ten labelled universal physical inventories have size twelve.”MacMahon.physical_iff_two_triangles(theorem), declared in LeanPool/MacMahon/Theorems.lean, line 71: “An inventory of twelve cubes is physically universal exactly when its Conway tableau is the two disjoint triangles of a partition of the six labels into two triples, with one copy of each directed edge.”MacMahon.physical_minimum_has_no_repeats(theorem), declared in LeanPool/MacMahon/Submission.lean, line 19: “Every variety has multiplicity at most one in a minimum universal inventory.”MacMahon.proper_rotation_iff(theorem), declared in LeanPool/MacMahon/Rotations.lean, line 50: “The rotation table contains precisely all proper signed-axis rotations.”MacMahon.exposed_face_rule(theorem), declared in LeanPool/MacMahon/Rotations.lean, line 79: “The outward faces at each of the eight positions obey the coordinate sign rule.”MacMahon.face_colours_valid(theorem), declared in LeanPool/MacMahon/Rotations.lean, line 63: “Every off-diagonal tableau entry assigns the six distinct nonzero colours.”MacMahon.face_assignment_coverage(theorem), declared in LeanPool/MacMahon/Submission.lean, line 24: “Every assignment of six distinct nonzero colours is a rotated tableau variety.”MacMahon.face_assignment_unique(theorem), declared in LeanPool/MacMahon/Submission.lean, line 40: “The variety and proper rotation representing a face assignment are unique.”
Project
- Authors: Jason Davies.
- Project repository: jasondavies/macmahon-min-universal-sets, at commit d8856c97.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05A15, 05C70, 68V15, 00A08.
- In Lean Pool: LeanPool/MacMahon, from the card LeanPool/projects/macmahon-min-universal-sets.yaml.
Sources
TheoremTurán's theorem (the "Book" weighting proof)#
Formalizes the weighting/optimization proof of Turán's theorem from Proofs from THE BOOK, bounding the number of edges of a p-clique-free simple graph by (1/2)(1 - 1/(p-1)) n².
Quoted from the card LeanPool/projects/turan3.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.
Turan3.turans(theorem; a main declaration), declared in LeanPool/Turan3/Turans3rdProof.lean, line 2577: “Turán's theorem — a p-clique-free simple graph on n vertices has at most (1/2)(1 - 1/(p-1)) n² edges.”Turan3.finale_bound(theorem; a main declaration), declared in LeanPool/Turan3/Turans3rdProof.lean, line 2343: “For any weight distribution on a p-clique-free graph, the total edge weight is at most ((p-1)(p-2)/2)·(1/(p-1))², the bound used to derive the edge count.”Turan3.Better_forms_clique(theorem; a main declaration), declared in LeanPool/Turan3/Turans3rdProof.lean, line 532: “Starting from any weight function, the minimal-support weight-non-decreasing improvement has support that forms a clique.”Turan3.Enhance_total_weight_stricinc(theorem), declared in LeanPool/Turan3/Turans3rdProof.lean, line 1545: “Equalizing weights between a maximum- and minimum-weight vertex in the clique support strictly increases the total edge weight.”
Project
- Authors: Rodrigo Gutierrez, Yves Jäckle.
- Project repository: ro-gut/turan3.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 05C35.
- In Lean Pool: LeanPool/Turan3, from the card LeanPool/projects/turan3.yaml.
Sources
TheoremTutte’s path theorem for matroids#
Proves the modular-cut path theorem for finite matroids, with reusable rank-partition, hyperplane-separation, relative-complement, indecomposable-cover, and diamond constructions.
Quoted from the card LeanPool/projects/tutte-path.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.
TutteFormalization.path_theorem(theorem; a main declaration), declared in LeanPool/TuttePath/PathTheorem.lean, line 36: “In a finite connected matroid, any two hyperplanes containing a proper indecomposable flat and lying outside a modular cut are joined by a finite Tutte path all of whose vertices contain that flat and avoid the cut. Consecutive vertices are distinct hyperplanes with indecomposable corank-two intersection; repeated nonconsecutive vertices are permitted.”TutteFormalization.path_theorem_of_indecomposable(theorem), declared in LeanPool/TuttePath/PathTheorem.lean, line 27: “In any finite matroid, two hyperplanes containing an indecomposable flat F and lying outside a modular cut are joined by a Tutte path whose vertices contain F and avoid the cut. This strengthens the cited path theorem by requiring only connectedness of the contraction by F; properness of F follows from containment in an endpoint hyperplane.”TutteFormalization.exists_indecomposable_complement(theorem), declared in LeanPool/TuttePath/IndecomposableComplement.lean, line 55: “If an indecomposable flat S and a flat U span the ground, every indecomposable flat T contained in both extends inside S to an indecomposable flat R spanning the ground with U, with corank R equal to rank U minus rank T.”TutteFormalization.exists_relative_complement(theorem), declared in LeanPool/TuttePath/RelativeComplement.lean, line 70: “For nested flats T contained in S, there is a flat U containing T whose intersection with S is T, whose join with S is the ground, and whose corank equals rank S minus rank T.”
Project
- Authors: Tutte formalization contributors.
- Source: arXiv:2601.02582.
- Project repository: mbaker386/tutte-homotopy-lean, at commit ab33c233.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 05B35.
- In Lean Pool: LeanPool/TuttePath, from the card LeanPool/projects/tutte-path.yaml.
Sources
TheoremVerified canonical labelling of finite graphs#
Implements an individualisation-refinement canonical-labelling algorithm in the style of nauty and proves that its canonical adjacency form is invariant under vertex relabelling and classifies finite graphs up to isomorphism. The imported core includes the executable search, refinement, orbit-pruning and backjumping machinery together with its equivariance, termination, soundness and optimality proofs.
Quoted from the card LeanPool/projects/isograph-canonical-labelling.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.
IsoGraph.Canon.canonAdj_eq_iff(theorem; a main declaration), declared in LeanPool/IsoGraph/Canon/Spec.lean, line 464: “Two Boolean adjacency functions on Fin n have equal canonical forms exactly when one is a relabelling of the other by a vertex permutation.”IsoGraph.Canon.canonAdj_relabel(theorem; a main declaration), declared in LeanPool/IsoGraph/Canon/Spec.lean, line 430: “Relabelling a finite graph by any permutation leaves its canonical adjacency form unchanged.”IsoGraph.Canon.exists_relabel_of_canonAdj_eq(theorem), declared in LeanPool/IsoGraph/Canon/Spec.lean, line 264: “Equality of canonical adjacency forms yields an explicit permutation relating the original adjacency functions.”
Project
- Authors: Alex Meiburg.
- Source: IsoGraph by Alex Meiburg.
- Project repository: Timeroot/IsoGraph, at commit bbfcefd1.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 05C60, 68R10.
- In Lean Pool: LeanPool/IsoGraph, from the card LeanPool/projects/isograph-canonical-labelling.yaml.
Sources
TheoremVizing's theorem and equitable edge colourings#
Proves the maximum-degree-plus-one edge-colouring bound for finite simple graphs by fans and Kempe exchanges. A separate component-swapping argument equitably rebalances any finite proper edge colouring on its original palette. Together they give equitable proper edge colourings on any palette of at least maximum degree plus one colours, with every class bounded by the ceiling of the average class size. Extracted from the published Paper IV formalization; these are classical colouring results, not a claim to new mathematics or to the paper's clique-partition bound.
Quoted from the card LeanPool/projects/vizing-equitable-edge-colouring.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.
LeanPool.Vizing.lineGraph_colorable(theorem), declared in LeanPool/Vizing/Main.lean, line 140: “The line graph of a finite simple graph G is colourable with maximum degree of G plus one colours.” Its source, as the card gives it: “Vizing's theorem for finite simple graphs; Vizing (1964).”SimpleGraph.lineGraph_chromaticNumber_le_maxDegree_succ(theorem), declared in LeanPool/Vizing/Main.lean, line 153: “The chromatic number of the line graph of a finite simple graph G is at most maximum degree of G plus one.”LeanPool.Vizing.Equitable.exists_equitable_colouring(theorem), declared in LeanPool/Vizing/Equitable.lean, line 751: “Every proper edge colouring of a finite simple graph with a finite palette admits a proper recolouring on the same palette in which any two colour classes differ in size by at most one.”LeanPool.Vizing.exists_equitable_edge_colouring(theorem; a main declaration), declared in LeanPool/Vizing/Corollaries.lean, line 26: “For every finite simple graph G and natural c at least maximum degree of G plus one, there is an equitable proper edge colouring with c colours; each colour class has at most ceiling(|E(G)|/c) edges.”
Project
- Authors: Juan Pablo Traverso Gianini.
- Source: Vizing and equitable edge-colouring modules in the published Paper IV freeze by Juan Pablo Traverso Gianini.
- Project repository: jtraverso/erdos-81-chordal-clique-partitions, at commit ff2019f5.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 05C15.
- In Lean Pool: LeanPool/Vizing, from the card LeanPool/projects/vizing-equitable-edge-colouring.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.