Hacker News Reader

Comment by sega_sai | Hacker News Reader

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/

It's quite instructive.

View on HN

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

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.

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

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/

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.

Reply on news.ycombinator.com