Hi

Stream: new members

[Barnabás Kiglics]

Hi everyone! I'm Barnabás Kiglics a high school student from Hungary.I'm interested in formalising mathematics as a learning tool. I dipped my feet in Metamath which is a really simple system similar to Lean but unfortunately I don't know enough set theory for it (not yet at least). I also discovered Lean a couple months ago. I've done a the natural number game (It's really fun) until the power world and I'm just now starting the function world. I've heard that there is a discord, but I couldn't find an active invite link. Can I get one somehow? One more question: I've read that Lean4 is not backwards compatible with Lean3. Which one should I learn as a complete beginner?

[Johan Commelin]

@Barnabás Kiglics Welcome! I would recommend starting with Lean 3, because Lean 4 is still very experimental.

[Johan Commelin]

The discord is run by @Kevin Buzzard and is mostly meant for undergrads, afaik.

[Johan Commelin]

See https://leanprover-community.github.io/learn.html for more info.

[Kevin Buzzard]

Definitely start with Lean 3, there is a ton more teaching material and a bunch of helpful libraries, and to a beginner the systems are basically indistinguishable.

[Barnabás Kiglics]

Johan Commelin said:

Barnabás Kiglics Welcome! I would recommend starting with Lean 3, because Lean 4 is still very experimental.

Thank you for the answers I'll start with Lean3 then. I can always switch later when Lean4 is more developed.