Some newbie questions

Stream: new members

[DayDun]

Hello everyone. I'm coming from a programming background and I find this formal verification stuff super interesting. Would love to learn more about lean, but I have a few questions:

• What's the deal with lean 3 vs 4? I'm currently using lean 4, but it looks like most resources are targeted towards lean 3. Though it looks like lean 3 was last updated back in 2019, so should a beginner like me focus on learning lean 3 or 4?
• I've stumbled across numerous introduction guides to lean, but is there any more structured documentation on features and syntax of the language? Or am I supposed to figure stuff out by reading the source code?

[Mario Carneiro]

You should be using the community edition of lean 3, at leanprover-community.github.io

[Kevin Buzzard]

Lean 3 is forked, and alive and well at the Leanprover community website. Sounds like you might want to look at the community home page to get up to speed with what's happening with Lean 3.

[DayDun]

Alright, didn't see it was forked. What's the status of lean 4? How usable is it? And is there any estimation when it will be "ready"? I quite like the fact that large parts of it are written in lean, and reading about the changes from lean 3 to 4, many of them sound quite handy.

[Mac]

@DayDun It's perfectly usable, but it is currently undergoing rapid development and changes by the day. The very work-in-progress Lean 4 manual has a section on how to set it up. Currently, despite the existence of a supposed stable release, the nightly is the only version actively supported (e.g., by the VSCode extension and #lean4 stream). So, if you are fine playing with an alpha product you can jump in and toy around with stuff if you want. However, if you want a stable Lean with some rich documentation, the Lean 3 community version is for you.