Upstreaming dashboard

The eventual goal of the LeanCamCombi project is to not contain any significant new formalisation, but instead to act as a shallow layer over Mathlib showing concretely how to turn paper-combinatorics into Lean-combinatorics.

As such, it is crucial to continuously upstream code from LeanCamCombi to Mathlib. The way we organise this is with the following two lists, showing files with no LeanCamCombi dependencies depending on whether they contain the keyword sorry or not.

Files ready to upstream

The following files are sorry-free and do not depend on any other LeanCamCombi, meaning they can be readily PRed to Mathlib.

• LeanCamCombi.Util
• LeanCamCombi.PlainCombi.OrderShatter
• LeanCamCombi.PlainCombi.KatonaCircle
• LeanCamCombi.GraphTheory.ExampleSheet2
• LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
  • chore: use mixin ordered algebraic typeclasses (part 1) #20594
  • refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API #4127
• LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
  • chore: use mixin ordered algebraic typeclasses (part 1) #20594
  • chore: deprecate former interaction of finite intervals and succ/pred lemmas #22327
• LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions

Files easy to unlock

The following files do not depend on any other LeanCamCombi file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.

• LeanCamCombi.PlainCombi.VanDenBergKesten 1 sorry
• LeanCamCombi.PlainCombi.LittlewoodOfford 1 sorry
• LeanCamCombi.StableCombi.Rel 2 sorries
• LeanCamCombi.GraphTheory.ExampleSheet1 16 sorries
• LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup 7 sorries