1. 10

  2. 2

    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?

    1. 4

      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).

      1. 2

        What a great reply. Thanks for the context and insight into mathlib. Really looking forward to digging in more.

        1. 4

          Happy to help :–)! Here are some more resources to save you some digging

          • Lean community is the main source of information on mathlib with lots of toolchain tutorials and API overviews such as this one
          • Project Xena, originally Professor Buzzard’s effort to formalize ICL undergrad maths curriculum, now also active as a more general blog and a Twitter account
          • Natural Number Game is a basic introduction, mentioned in both Xena and Lean community site, but worth mentioning here; it’s a very chill, slow-paced starting point that works entirely online!
          • Lean for the Curious Mathematician 2020 is a more advanced series of workshops with videos on YouTube, everything very recent
          • EPSRC TCC 2021 is another series of workshops, even more recent
          • And finally, the Zulip server is very active and people are very helpful!