Lean Introduces Verified Fizzbuzz Programming Tutorial

This post introduces Lean as both a programming language and interactive proof assistant, and demonstrates implementing and verifying the Fizzbuzz problem using Lean's pure functional style and dependent typing. It contrasts Lean with Dafny, explains design trade-offs (no mutable state, proof-driven verification, fewer SMT timeouts), presents code examples (fb_one, fizzbuzz), and promises readers enough background to verify simple programs by the end of the series.