Zulip Chat Archive

Stream: new members

Topic: Hi


view this post on Zulip Barnabás Kiglics (Apr 11 2021 at 15:58):

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?

view this post on Zulip Johan Commelin (Apr 11 2021 at 17:53):

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

view this post on Zulip Johan Commelin (Apr 11 2021 at 17:54):

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

view this post on Zulip Johan Commelin (Apr 11 2021 at 17:54):

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

view this post on Zulip Kevin Buzzard (Apr 11 2021 at 17:55):

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.

view this post on Zulip Barnabás Kiglics (Apr 11 2021 at 18:05):

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.


Last updated: May 15 2021 at 23:13 UTC