logical_verification_2021 VS formalising-mathematics

There is also the https://github.com/blanchette/logical_verification_2021 with the accompanying course website https://lean-forward.github.io/logical-verification/2021/.

He's saying that you should treat that implementation of lists-as-sets as being commutative, but with the caveat that you need to regard lists that are permutations of each other (i.e. lists that have the same elements, possibly in a different order) as equivalent. In this setting, you identify "equivalent" elements -- if R is an equivalence relation, and R a b, and [a] and [b] are their equivalence classes, you say [a] = [b]. Lean has a type for quotients where you get equality in sense (although strictly speaking, lean's quotients aren't implemented as equivalence classes).

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.

If you're not already up to speed on proof based mathematics, there's a lot of great intros. I got into it with getting into coding with LEAN though, so... obligatory link to the natural number game if that sounds interesting. If you finished that and wanted to keep going, this would be the next step.

I don't want to distract from your journey into PM, but if this is the kind of thing you're into, I'd highly recommend checking out LEAN at some point in the future. It's a proof assistant language... in some ways you could call it (one of the many) modern efforts to continue what PM set out to do. If you're inclined, the natural number game is where to start, with this as a great followup. The standard reference here is what you'd get the most out of reading, but it'd be hard to follow without getting your hands dirty a little first.

Hard agree. As a followup from a related source, I highly suggest this repo. It's an 8 week series meant to be a followup on the natural number game, starting with basic logic, then going into groups, some basic analysis, and a number of other things. It's a great way to start to get a little more comfort with a bigger range of mathlib's library, and it's all still laid out in a way that's pretty easy to follow still while you do it. The only catch, unlike the natural number game, this one requires going through it directly in visual studio code, filling in the blanks basically. Slightly more setup than the natural number game, but well worth it if a person was still inclined to do more after finishing that intro.