3 ms·

Interesting. I always wanted to try Lean, and personally never found an easy way to do it, as it requires installing a plugin in vscode, create a project or rea

Interesting. I always wanted to try Lean, and personally never found an easy way to do it, as it requires installing a plugin in vscode, create a project or reading the lean book. But following the links I've found this nice interactive tutorial for proving 2+2=4 in Peano arithmetic: https://adam.math.hhu.de/#/g/leanprover-community/nng4/ https://adam.math.hhu.de/#/g/leanprover-community/nng4/ It's quite instructive.

thechao 1y ago
Ironically, the website broke, and became stuck on the "rw[one_is_succ_zero]" rewrite rule, continually telling me that "rfl" isn't valid. Sigh.
gfaster 1y ago
Lean is more complex to develop in than most programming languages since it relies heavily on interactive programming, i.e. the context pane. The "easy way" is with a plugin. If you're interested in learning more about Lean for writing proofs, I would recommend The Mechanics of Proof [0]. It strips out a lot of the convenience tactics in Mathlib to focus on the more primitive mechanisms Mathlib builds on. [0]: https://hrmacbeth.github.io/math2001/index.html https://hrmacbeth.github.io/math2001/index.html
- sega_sai 1y ago
  I've seen the book, but I've personally found it not very useful for a person who wants to first get the basics. The natural number's game is actually quite fun, and I did understand much better the language. And it's also interactive, so you can try your solutions, and there are hints when stuck.
gopiandcode 1y ago
Fwiw there's also an Emacs plugin which is what I use and it works really well. For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024 https://github.com/lean-forward/logical_verification_2024 Also, Lean is also remarkably usable as a programming language itself, which might give an easier onboarding ramp: https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/

thechao 1y ago

Ironically, the website broke, and became stuck on the "rw[one_is_succ_zero]" rewrite rule, continually telling me that "rfl" isn't valid. Sigh.

gfaster 1y ago

Lean is more complex to develop in than most programming languages since it relies heavily on interactive programming, i.e. the context pane. The "easy way" is with a plugin. If you're interested in learning more about Lean for writing proofs, I would recommend The Mechanics of Proof [0]. It strips out a lot of the convenience tactics in Mathlib to focus on the more primitive mechanisms Mathlib builds on. [0]: https://hrmacbeth.github.io/math2001/index.html https://hrmacbeth.github.io/math2001/index.html

sega_sai 1y ago
I've seen the book, but I've personally found it not very useful for a person who wants to first get the basics. The natural number's game is actually quite fun, and I did understand much better the language. And it's also interactive, so you can try your solutions, and there are hints when stuck.

gopiandcode 1y ago

Fwiw there's also an Emacs plugin which is what I use and it works really well. For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024 https://github.com/lean-forward/logical_verification_2024 Also, Lean is also remarkably usable as a programming language itself, which might give an easier onboarding ramp: https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/