alt Hacker NewsIntroduction to Formal Verification with Lean Part 1
Comments
If you like Lean, here are two more great, short books on proving things about your program (not with Lean, though):
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.
I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you run it interactively and observe the goals at each step. In contrast languages like Idris do not use tactics and require explicit manipulation of proof objects; it’s a lot less automated and verbose. Using the function call analogy, it’s like having to write down every argument passed to a function call and name every return value. It’s more tedious to write but both the writer and the reader gain more by the explicitness. But in the age of AI, the tedium to write proofs without tactics really shouldn’t have mattered.
The Natural Numbers Game is amazing, highly recommended.
> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.
Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).
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 ;)
I built an automated math research system using Lean to verify the results: https://alethean.org
This is cool and im not familiar with what lean actually does beyond the words "formal methods"
immediate questions from reading:
* what is rfl?
* what is decide?
i spent a lot of time looking for where these keywords(? declarations?) were made and i still dont know what they end up meaning
(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
a) Thanks for putting this together!
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.
how is lean different from tlaplus for helping you with reasoning during the design phase?
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?
https://www.amazon.com/Maths-Proofs-Lean-First-Steps-ebook/d... I like this author and a while ago found that he'd published a book on Lean!
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.
Does anyone do TLA style distributed systems verification with Lean? Curious the experience there and how well supported it is
I just wish Lean4 is easier to use. Tried Mathematics in Lean and couldn’t even get the dependencies right
Just in case anyone else decides to write along like the article suggests. I chose to use the live.lean-lang.org link, but it seems to default to a newer version of lean where the simp[xor] actually returns both sides still wrapped in the lambdas so the next simp[add_comm] will actually fail. The way to get around it is changing the version to v4.32.0 which the article doesn't seem to mention.
Why does Lean always have a way to mess up your file system, writing to any files, rather than just proving proofs?
I found that out when reading the recent articls about counterexamples.
[flagged]
Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/
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.