Showcases of formalized mathematics in a system like Coq or Lean?

Question

I have been reading about and trying out type theory based proof assistants Lean and Coq, and I have seen a few formalized proofs of basic, isolated propositions.

I am looking for examples, showcases, of a formalized body of theory of e.g. standard undergraduate texts, to showcase how one would go about setting up complex formalized theories. E.g. I'd be interested to see a formalization in a proof assistant like Lean or Coq, of the theory of groups, together with the homomorphism theorems, and so forth.

Answer 1

There is an ongoing project called mathlib that is formalizing a lot of maths from different areas in lean. You can look around this folder to see the various topics already formalized, for example you can see in this folder which group theory results have been formalized.

It is not organized like a textbook and different topics are at very different levels, but it's one of the biggest bodies of formalized math out there!

Answer 2

The systems are unlike Coq or Lean in many ways, but Mizar has the journal Formalized Mathematics which has identifiers you can look up at, say this list of current HTML files to get the original code. And Metamath is used to make the Metamath Proof Explorer. Both have an assortment of math that has been formally checked.