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.UtilLeanCamCombi.PlainCombi.OrderShatterLeanCamCombi.GraphTheory.ExampleSheet2LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYMLeanCamCombi.Mathlib.Combinatorics.SimpleGraph.SubgraphLeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.ConstructionsLeanCamCombi.Mathlib.Algebra.BigOperators.FieldLeanCamCombi.Mathlib.Data.Fintype.Card- feat: add
Decidable,Fintype,Encodablelinters #10235 - chore: deprecate
Nat.(case_)strong_induction_on#16464 - feat: lint on declarations mentioning
InvertibleorUnique#17518 - feat: the
metrisableSpacelinter #17519 - chore(Data/Finset/Image): split file #19903
- feat: extensible
push_negtactic #21769 - chore(Data/Fintype): split
Data/Fintype/Basic.lean#21831 - refactor(Cache): use module name as key instead of unresolved file path #21834
- chore(Data/Fintype): split
Fintype/Card.lean#21840 - chore(Data/Finset): don’t import algebra when defining
Finset.card#21866 - chore(Data/Set/Finite): avoid importing algebra in
Data.Set.Finite#21870 - chore(Data/Set): avoid importing algebra in
Data/Set/Countable.lean#21874
- feat: add
LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
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.