Writing Technical Posts in Lean

Lua

2025-07-12

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:

fib : Nat → Nat#check fib

fib : Nat → Nat

The answers are as expected:

55#eval fib 10

610#eval fib 15

The #eval commands show the actual computed results. This naive recursive implementation isn't efficient for large numbers, but it clearly demonstrates the mathematical definition. When you see this code, you know it actually runs exactly as written—there's no risk of typos or inconsistencies between the explanation and implementation.

Proofs Don't Fib

Here are a couple of proofs that demonstrate Lean's verification capabilities using our Fibonacci function. First off, the Fibonacci sequence is non-decreasing. That is, F_{n} \le F_{n + 1}:

theorem fib_nondec : fib n ≤ fib (n + 1) := byn:Nat⊢ fib n ≤ fib (n + 1)
  induction nzero⊢ fib 0 ≤ fib (0 + 1)succn✝:Nata✝:fib n✝ ≤ fib (n✝ + 1)⊢ fib (n✝ + 1) ≤ fib (n✝ + 1 + 1) <;>zero⊢ fib 0 ≤ fib (0 + 1)succn✝:Nata✝:fib n✝ ≤ fib (n✝ + 1)⊢ fib (n✝ + 1) ≤ fib (n✝ + 1 + 1) simp [fib]All goals completed! 🐙

Furthermore, the sequence is strictly increasing after the first two elements. The first step is to show that for all positive n, F_n is positive:

@[Try these:
  [apply] [grind .] for pattern: [@LE.le `[Nat] `[instLENat] `[1] (fib #1)]
  [apply] [grind →] for pattern: [@LE.le `[Nat] `[instLENat] `[1] #1]
  [apply] [grind! .] for pattern: [fib #1]grind]
theorem fib_pos : n > 0 → fib n > 0 := byn:Nat⊢ n > 0 → fib n > 0
  induction n with
  | zero =>zero⊢ 0 > 0 → fib 0 > 0 simp [fib]All goals completed! 🐙
  | succ n' ih =>succn':Natih:n' > 0 → fib n' > 0⊢ n' + 1 > 0 → fib (n' + 1) > 0
    simpsuccn':Natih:n' > 0 → fib n' > 0⊢ 0 < fib (n' + 1)
    cases n'succ.zeroih:0 > 0 → fib 0 > 0⊢ 0 < fib (0 + 1)succ.succn✝:Natih:n✝ + 1 > 0 → fib (n✝ + 1) > 0⊢ 0 < fib (n✝ + 1 + 1) <;>succ.zeroih:0 > 0 → fib 0 > 0⊢ 0 < fib (0 + 1)succ.succn✝:Natih:n✝ + 1 > 0 → fib (n✝ + 1) > 0⊢ 0 < fib (n✝ + 1 + 1) grind [fib]All goals completed! 🐙

Now, grind can use the lemma to show that fib is strictly increasing:

theorem fib_gt_1_inc : fib (n + 2) < fib (n + 3) := byn:Nat⊢ fib (n + 2) < fib (n + 3)
  induction nzero⊢ fib (0 + 2) < fib (0 + 3)succn✝:Nata✝:fib (n✝ + 2) < fib (n✝ + 3)⊢ fib (n✝ + 1 + 2) < fib (n✝ + 1 + 3) <;>zero⊢ fib (0 + 2) < fib (0 + 3)succn✝:Nata✝:fib (n✝ + 2) < fib (n✝ + 3)⊢ fib (n✝ + 1 + 2) < fib (n✝ + 1 + 3) grind [fib]All goals completed! 🐙

Additionally, every third element of the sequence is even. If a number n is even, then there exists some k such that n = 3k; the proof is by induction on k.

theorem fib_third_even : 3 ∣ n → 2 ∣ fib n := byn:Nat⊢ 3 ∣ n → 2 ∣ fib n
  intro ⟨k, hk⟩n:Natk:Nathk:n = 3 * k⊢ 2 ∣ fib n
  rw [hk]n:Natk:Nathk:n = 3 * k⊢ 2 ∣ fib (3 * k)
  clear n hkk:Nat⊢ 2 ∣ fib (3 * k)
  induction kzero⊢ 2 ∣ fib (3 * 0)succn✝:Nata✝:2 ∣ fib (3 * n✝)⊢ 2 ∣ fib (3 * (n✝ + 1)) <;>zero⊢ 2 ∣ fib (3 * 0)succn✝:Nata✝:2 ∣ fib (3 * n✝)⊢ 2 ∣ fib (3 * (n✝ + 1)) grind [fib]All goals completed! 🐙

Moving Forward

Having executable code and verified proofs directly in blog posts eliminates the usual gap between explanation and implementation. The interactive features—like being able to hover over function names to see their types and documentation—make the reading experience more informative than “plain” code blocks. Furthermore, tactic proofs are difficult to read without intermediate proof states, so Verso makes these visible.

For more advanced users, Verso itself can be extended in Lean, which opens up interesting possibilities for custom blog functionality. I'm planning to explore some data structure implementations and more mathematical concepts in future posts.