Lean4 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず FizzBuzz の証明を書いてみました。 import Std def fizz_buzz : Nat → String := fun n => if n % 15 = 0 then "Fizz…