How to use Lean4 for an absolute beginner?

Stream: new members

[Josiah Winslow]

Hello, I'm trying to use this for the first time and I don't even know the first thing about it. How can I use this to start proving logical theorems using some system of axioms?

[Scott Morrison]

@Josiah Winslow, are you certain you want to use Lean4? It is not really ready for regular users, and if you're not sure then you should be using Lean3 instead. It has a better user experience, way more documentation, etc.

[Scott Morrison]

(That said, the transition to Lean4 will happen over the next year, hopefully.)

[Scott Morrison]

Please look at https://leanprover-community.github.io/ for starting resources.

[Scott Morrison]

If you haven't seen it already, you might start at http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Josiah Winslow]

@Scott Morrison I don't know what I wanna be using, tbh. How would I set up Lean3, in this case?

[Scott Morrison]

https://leanprover-community.github.io/get_started.html#regular-install

[Floris van Doorn]

Start by playing the natural number game (linked above)
After that, you can follow the installation instructions here: https://leanprover-community.github.io/get_started.html#regular-install