group theory: mathlib4

Stream: lean4

[Siddharth Bhat]

I've been working on implementing core computational group theory algorithms like Schreier–Sims over at opencompl/lean-gap.

I want to write Lean-checked proofs of these which will need basic group theory (structure of the permutation group, some facts about cosets, subgroups). I am quite unsure about the status of mathlib4. Do I simply pull in leanprover-community/mathlib4 and start reusing group theoretic theorems? Is mathlib4 a stable target for such use?

[Alex J. Best]

Cool! https://leanprover-community.github.io/blog/posts/intro-to-mathport/ is a pretty up-to-date summary of the status of the different porting components.

[Siddharth Bhat]

The link was very useful to get a lay of the land, thank you! I'm unsure what action I should concretely take.

My takeaway was that I should see what parts of mathlib3 are useful for me, then check if they compile correctly in mathlib3port. If it does not, I then fix the files in mathlib3port and send a PR to mathlib4.

Is that correct?