2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Perhaps this MO question would be interesting for you. While looking for that question I've seen that Kevin Buzzard (who asked that question) has a blog about his use of Lean in his teaching, which could also be interesting. $\endgroup$ – Arnaud D. Jul 5 at 20:16
1
$\begingroup$

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!

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.