Archive
Posts about learning Lean 4, formal verification, and writing proofs alongside code. I'm documenting what I figure out as I go, mostly focusing on how to apply these ideas to practical programming problems.
Categories
Posts
-
Lean Got Better!
Lean has definitely improved in the last couple of years! As I write this, Lean 4.22 is hot off the presses, so let's look at a few of the improvements since 4.0. In Lean, I can define a type of expressions with variables:
Read more -
Making Fibonacci Fast (And Proving It's Correct)
In my last post, I showed off a simple recursive Fibonacci implementation. While it clearly expresses the mathematical definition, it has a serious performance problem that becomes obvious pretty quickly.
Read more -
Writing Technical Posts in Lean
I've been thinking about starting a technical blog for a while, and recently decided to try Verso—a documentation tool that lets you write in Lean 4. The appeal is being able to mix explanations with actual executable code and verified proofs rather than relying on screenshots or hand-wavy arguments. Since Lean understands the code directly, you get accurate syntax highlighting, identifiers automatically link to the Lean reference manual, and you can hover over functions to see their documentation and type signatures.
Here are a couple of examples to show what this looks like in practice.
Read more -
Starting This Blog
I've been meaning to start writing about technical topics for a while, but kept putting it off. The usual blogging platforms never felt quite right for the kind of content I wanted to create—mixing code examples with mathematical reasoning in a way that actually works.
Over the past year, I've been learning about formal methods and theorem proving, partly out of curiosity and partly because I think these techniques could be useful for writing more reliable software.
Read more