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.
This is a lot of useful data for the next iteration of Claude because not only does Anthropic have the final artifacts but they also saw the entire workflow from start to finish & Facebook paid them for the privilege of giving them all of that training data.
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.