Our great sponsors
-
formalising-mathematics
Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
As far as implementations go, I highly recommend checking out LEAN. There's a lot of systems obviously (as mentioned in the comments, though Coq and Isabelle seem to have the most literature around them) but LEAN's the one I've spent some time exploring. If you're this curious, check out the natural number game. You start with Peano's axioms, and then build up the full proof that the structure is a totally ordered ring. If you do that and you're still having fun with it, this is the followup. It's a little tour through a few basic topics in group theory, point set topology, sequences and limits, quotient spaces, and so on. Basically it's the repo from an 8 week workshop series that was taught in 2021. After spending a little time with LEAN (enough to have a little sense of what's going on) you'll likely also find a ton of value in going through the documentation. There's a ton of really interesting, thought provoking stuff in there, including a little bit on the philosophy of how to approach making a language like this.