It's interesting to see a lot of formalized proofs gather around Lean (specifically Mathlib). I've in a formal math class right now, so it's a bit weird learning ZFC while messing around with Lean, which is based on dependant types.

There's a lot of other proof assistants out there, like Mizar, Isabelle, Metamath, Metamath0, and Coq, each based on different foundations. Metamath0 in particular looks really intriguing, since it's the brainchild of Mario Carneiro, who was also the person who started Mathlib (and I believe is still an active contributor).

Anyways, Lean definitely has a lot going for it, but I love to tinker, and it's interesting to see other proof assistants' takes on things.

Metamath is fascinating to me in that it is the most "math-like," in terms of being both readable and executable on pen and paper through simple substitution. I've spent a month or two formalizing basic results in it and found it quite fun; unfortunately the proof assistant and surrounding tooling is, archaic, to put it generously. However, the fact that the system still works and that the proof tree is grounded in results from 1994 that still stand to modern day without modification is testament to its design.

Most people seem to be rallying around Lean these days, which is powerful and quite featureful, but with tactics metaprogramming feels more like writing C++ templates instead of the "assembly language of proof" which I liken metamath to, for its "down to the metal" atomization of proof into very explicit steps. Different (levels of) abstractions for different folks.

Once I return to a proper desktop I will probably woodshed myself into Lean for a week or two to get a better handle on it, but for now tactics feel like utter magic when not just chaining `calc` everywhere.