WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Combinatorics

Revision #2026 → #2408 · back to history

modifiedSushruta's 63 combinations of tastesef5a1b8a776e
FieldFrom #2026To #2408
noteThe count 2^6 − 1 = 63 nonempty subsets is a special case of `Finset.card_powerset`, but the specific story is not formalized.The count 2^6 − 1 = 63 nonempty subsets is a special case of `Finset.card_powerset` (verified to exist), but the specific story is not formalized.
addedSchröder–Hipparchus numbers4d7adc7bae0f
modifiedSymmetry of binomial coefficientse3f039671d0f
FieldFrom #2026To #2408
note`Nat.choose_symm` states `choose n k = choose n (n-k)`, the symmetry of binomial coefficients.`Nat.choose_symm` (verified) states `choose n k = choose n (n-k)`, the symmetry of binomial coefficients.
modifiedPascal's triangle / arithmetical triangleb30dc1ab24a7
FieldFrom #2026To #2408
notePascal's rule `choose (n+1) (k+1) = choose n k + choose n (k+1)` underlies the triangle.Pascal's rule `Nat.choose_succ_succ` (verified) underlies the triangle.
modifiedHamiltonian cycles in Cayley graphs50894132cc34
FieldFrom #2026To #2408
noteHamiltonian cycles are formalized as `SimpleGraph.Walk.IsHamiltonianCycle`; the Cayley-graph-on-permutations specialization is not.Hamiltonian cycles are formalized as `SimpleGraph.Walk.IsHamiltonianCycle` (verified); the Cayley-graph-on-permutations specialization is not.
modifiedFibonacci numbers4ad42c38832e
FieldFrom #2026To #2408
noteFibonacci numbers are defined as `Nat.fib` in Mathlib.Fibonacci numbers are defined as `Nat.fib` (verified) in Mathlib.
modifiedTwelvefold way047368e1d9e4
FieldFrom #2026To #2408
note`Mathlib/Data/Sym/Card.lean` cites the Twelvefold Way and formalizes one of its 12 cells, but the full framework is not unified.`Sym.card_sym_eq_choose` (verified) formalizes one cell of the twelvefold way, but the full unified framework is not.
modifiedPartition theory6b3c87d14939
FieldFrom #2026To #2408
noteInteger partitions are defined in `Mathlib/Combinatorics/Enumerative/Partition/`, but the field itself is not a formal object.Integer partitions are defined as `Nat.Partition` (verified), but the subfield itself is not a formal object.
addedYoung diagrams5215d0bae69b
addedSymmetric groupcf3923cc6f5b
modifiedGraph theory considerationsec8938b45482
FieldFrom #2026To #2408
noteGraphs are formalized as `SimpleGraph`, but the meta-claim about their fundamental role is not a theorem.Graphs are formalized as `SimpleGraph` (verified), but the meta-claim about their fundamental role is not a theorem.
addedSteiner system546038cf759d
modifiedFinite geometrye67bea3c51a7
FieldFrom #2026To #2408
note`Mathlib/Combinatorics/Configuration.lean` covers projective-plane-style finite incidence configurations via `Configuration.Nondegenerate`, but the field is not defined as such.`Configuration.Nondegenerate` (verified) covers projective-plane-style finite incidence configurations, but the field is not defined as such.
modifiedOrder theoryc0ea7396a36e
FieldFrom #2026To #2408
notePartial orders are extensively formalized under `Mathlib/Order/`, though the subfield itself is not a formal object.Partial orders are extensively formalized via `PartialOrder` (verified), though the subfield itself is not a formal object.
modifiedLattices358dd41de240
FieldFrom #2026To #2408
noteLattices are formalized as the `Lattice` typeclass with extensive API.Lattices are formalized as the `Lattice` typeclass (verified) with extensive API.
modifiedBoolean algebras1c4d72de2a6f
FieldFrom #2026To #2408
noteBoolean algebras are formalized as the `BooleanAlgebra` typeclass.Boolean algebras are formalized as the `BooleanAlgebra` typeclass (verified).
modifiedMatroid theory26b1a934d0ed
FieldFrom #2026To #2408
noteMatroids are defined in `Mathlib/Combinatorics/Matroid/Basic.lean` with substantial accompanying API.Matroids are defined as `Matroid` (verified) in `Mathlib/Combinatorics/Matroid/Basic.lean` with substantial API.
modifiedSperner's theoremefc6cc8d3d3b
FieldFrom #2026To #2408
note`IsAntichain.sperner` bounds antichains in `Finset α` by the middle binomial coefficient — Sperner's theorem.`IsAntichain.sperner` (verified) bounds antichains in `Finset α` by the middle binomial coefficient — Sperner's theorem.
modifiedLargest triangle-free graph39de432793f1
FieldFrom #2026To #2408
noteTurán's theorem is formalized and specialises (r=2) to Mantel's theorem for triangle-free graphs.Turán's theorem is formalized (verified) and specialises (r=2) to Mantel's theorem for triangle-free graphs.
modifiedRamsey theory259ed965a5dc
FieldFrom #2026To #2408
noteThe Hales–Jewett theorem (a Ramsey-type result) is formalized, but Ramsey's theorem itself is not stated directly.The Hales–Jewett theorem (verified) — a Ramsey-type result — is formalized, but Ramsey's theorem itself is not stated directly.
modifiedPigeonhole principle84d417591f1c
FieldFrom #2026To #2408
noteThe pigeonhole principle is formalized as `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`.The pigeonhole principle is formalized as `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` (verified).
addedConvex sets2986e0355e69
modifiedAdditive number theoryd7d8ed7ee9b9
FieldFrom #2026To #2408
noteMany additive number theory results are in `Mathlib/Combinatorics/Additive/` (e.g. `ZMod.cauchy_davenport`), but the subfield itself has no formal definition.Many additive number theory results are in `Mathlib/Combinatorics/Additive/` (e.g. `ZMod.cauchy_davenport`, verified), but the subfield itself has no formal definition.
modifiedCombinatorial optimization04bc5b2e8d28
FieldFrom #2026To #2408
note`Mathlib/Combinatorics/Optimization/ValuedCSP.lean` covers valued constraint satisfaction, a slice of combinatorial optimization, but the field is not defined.`ValuedCSP` (verified) covers valued constraint satisfaction, a slice of combinatorial optimization, but the field is not defined.