I have been watching Lean a little bit. Not sure where it stands on stability between versions 3 and 4. Does anyone have any insight into how the project is progressing?
I can’t comment on Lean 3 versus Lean 4, but all of mathlib (the library where all the math development for Lean happens, including work in the cited article) is done in a fork of Lean 3. Porting everything to Lean 4 is work in progress; as far as I understand, Lean 4 is yet to be fully released (two pre-release milestones are public here).
What a great reply. Thanks for the context and insight into mathlib. Really looking forward to digging in more.
Happy to help :–)! Here are some more resources to save you some digging