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
-
Writing Technical Posts in Lean
Hello! This was generated from the Verso templates.
def fib : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fib n + fib (n + 1)As expected, it maps natural numbers to natural numbers:
#check fibThe answers are as expected:
#eval fib 10#eval fib 15Read more -
Weekly tips: Using git worktrees in Mathlib
hello
Read more