Introduction to Formal Verification with Lean Part 1
hashcloak.com
hashcloak.com
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.
Edit: a couple more thoughts. First, there is nothing stopping you from defining proof objects directly in Lean without tactics. That flexibility is quite nice -- you can automate as much or as little as you like. Of course, in practice, people almost always use tactics. Second, I use the ACL2 prover quite a bit, which is not tactic-based. Instead, you give high-level "hints" that steer the aggressively-automated prover. Funny enough, I have colleagues that look at Lean proofs and say "these proofs are so verbose, how does anyone understand them!".
Personally, I am experimenting a lot with Agda's instance arguments these days. They somehow have a bad rep for being slow, but their performance has improved a lot! One can juice it to write really readable code (Like truly ad-hoc polymorphic operators, or declaring axioms used in a theorem like `⦃ AC ⦄ → Theorem`), but it also allows for proof searches. Contrary to “tactics”, instance arguments feel like a fluid part of the proof language.
I think there is a lot of room for innovation in the space of proof engineering. I really hope that LLMs will not suck all the oxygen out of the room, by being trained on existing dogmas.
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)
The number of mentions of Lean in HN submissions aside, how do we gauge that? HN has odd trends like that - a decade ago, we loved everything "Bayesian" - but they don't necessarily translate to anything that's happening in the mainstream.
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.
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 ;)
TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.
> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.
The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.
So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.
A proof is just a manipulation of each "side" until they are trivially equal to each other).
One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)
`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
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.
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...
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?
I'd inform the webmaster but the telephone number listed on the site is "(123) 456 789", so I guess AI slop is AI slop.
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 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?
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
"rfl" stands for "reflexivity", the mathy term for "everything is equal to itself". As the article says, "[rfl] deems two things equal if they are equal by computation". That is to say, if the current subproblem is of the form "prove x = y" where both x and y are some sort of expressions that clearly evaluate to the same value, then applying rfl will finish the proof and mark this problem as solved.
"decide" is another tactic. Not sure where you got it from, I don't see it mentioned in this article. But basically it's a more powerful "I don't want to write out all the steps of this, please try to prove it for me" command.
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.