hi

Stream: new members

[Alessandro]

hi everybody. just read that lean was designed by leo... i'm the dev of Metatheory.jl and a big e-graph fan. Are e-graphs used for congruence closure or equational reasoning in lean?

[crab]

Hello, I am new to Lean. I hope to use it for mathematical programing

[crab]

what is the best way I can learn lean?

[Alex J. Best]

There are many ways, so the best way depends a bit on you, what you've learned in the past, and what you want to do with lean. We have a list of resources at:
https://leanprover-community.github.io/learn.html
In particular the natural number game is a good way to get started learning some of the syntax for proving mathematical results in lean.

[crab]

Are there any that are simpler than the others?

[Yakov Pechersky]

Natural Number Game is great place to start

[crab]

Natural Number Game?

[Yakov Pechersky]

(deleted)

[crab]

Let me search it up

[Yakov Pechersky]

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

[crab]

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

[crab]

this?

[crab]

sniped lol

[crab]

ok

[crab]

I will start with that