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 ;)
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/
Assuming you are serious; there is a lot to know conceptually before one can answer the above comprehensively.
Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?"
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.
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.
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?
Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).
Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.
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.
24 comments
[ 1.1 ms ] story [ 46.1 ms ] threadSmall 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 ;)
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.
Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?"
Some simple tutorials;
Introduction to Lean for Programmers: The syntax and semantics of mathematics - https://towardsdatascience.com/introduction-to-lean-for-prog...
The hitchhiker's guide to reading Lean 4 theorems - https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin...
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.
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 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?
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.
> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.
https://adam.math.hhu.de/
I found that out when reading the recent articls about counterexamples.
Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.
There's a blog post with a demo at https://proofsandintuitions.net/2026/02/09/distributed-verif...
It's still early days, but we're committed to making distributed protocol verification work extremely well in Lean.
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