Latest getting-started info

Stream: new members

[Martin C. Martin]

Hi! I'm a software engineer with a math background looking to perhaps contribute to mathlib.

Is the Lean Reference Manual the most up-to-date reference in getting started with Lean?

For someone with experience in both VSCode and Emacs, which environment is best for Lean?

For new contributors, where do you suggest we start to contribute? For example, mathlib 3 or 4? Which area of undergrad math is most in need of contributions in mathlib?

[Bryan Gin-ge Chen]

The Lean reference manual you linked is a bit out of date. We recommend the resources on our "Learning" page.

The recommended instructions for setting up Lean 3 are here: #install.

[Anne Baanen]

Welcome! The reference manual is sadly very outdated. The Lean community website has a list of up-to-date resources: https://leanprover-community.github.io/learn.html

For a software engineering background, I would recommend #tpil and #hglv

[Kevin Buzzard]

The community's website, with tons of resources, is here: https://leanprover-community.github.io/

The Lean reference manual is a fairly formal description of Lean 3. If you actually want to learn how to use it, try #tpil which is written to teach. I would strongly recommend VS Code over emacs simply because there are more tools available (and I had 25 years of emacs experience and 0 VS Code experience when I started).

[Patrick Massot]

A lot of answers are waiting for you at https://leanprover-community.github.io/

[Kevin Buzzard]

There is no mathlib4 yet. mathlib3 := mathlib is huge, and you can see what's missing on this page.

[Patrick Massot]

Four answers in the same minute, is that our record?

[Kevin Buzzard]

maybe we should write a bot which posts this stuff :-)