1. https://mitpress.mit.edu/9780262527958/the-little-prover/
2. https://mitpress.mit.edu/9780262536431/the-little-typer/
David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.
Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/
And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/
Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4
This is the best intro to Lean I know, plus it teaches you why a + b = b + a.
induction b with d hd
rw [add_zero, zero_add]
rfl
rw [add_succ, succ_add]
rw [hd]
rfl
I'd also argue that automation is essential to practical proof engineering. It make the proofs less brittle to minor changes and therefore more maintainable.
Also, after using a tactic enough you can guess why it's used.
Agda and Idris are more beautiful for sure, but a proof is a proof (according to the law of the excluded middle)
I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?
It's similar to a type system in that regard. The same difference could be applied there (comparing a Python type assert). Types, however, generally only cover checks similar to "the shape of the data is X".
Lean is different in that its language for expressing properties is wide enough to express anything you can imagine. The bottleneck becomes accurately stating properties you'd like to enforce and, subsequently, discovering proofs of whether or not they're true.
`lean4` is very much about the same two ideas. you can make statements about what it means for the code to say something interesting, usually something relevant to whether or not it's correct, and you make statements about the circumstances in which you would evaluate that.
people are interested in `lean4` because it allows you to make more interesting statements of both kinds, and you have tools to be much more specific about the details, the `assert` statements in `python` can't really call each other for example, they don't really compose. in `lean4` the ability to compose such statements is very important.
but you can write regular programs in it too. this is a reverse proxy faster than `nginx`: https://cdn.s4.gl/serve-fd.lean
b) Please don't hijack my scrolling.
c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
I've not gone too deep down this train of thought because a standard library/ecosystem should be solid and I don't think LLMs are quite there... but if we can use LLMs+Lean maybe we can get the quality we need to bootstrap more of the Lean ecosystem?
In the end I wasn't able to read it on my ebook reader and reading it on a PC or smartphone kinda makes it annoying to read on the commute. So I've only read the first two chapters or so but it seemed like a lot of fun. All this talk about using Lean in AI-powered proofs kinda makes me want to pick it up again.
Small feedback: - Great flow, explaination, motivation and so on! :) - Typo: "conext" at the bottom - If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)