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