Zulip Chat Archive

Stream: new members

Topic: Latest getting-started info


Martin C. Martin (Jul 21 2021 at 16:24):

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 (Jul 21 2021 at 16:26):

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 (Jul 21 2021 at 16:26):

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 (Jul 21 2021 at 16:26):

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 (Jul 21 2021 at 16:26):

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

Kevin Buzzard (Jul 21 2021 at 16:27):

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

Patrick Massot (Jul 21 2021 at 16:27):

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

Kevin Buzzard (Jul 21 2021 at 16:28):

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


Last updated: Dec 20 2023 at 11:08 UTC