ushumpei https://blog.hatena.ne.jp/ushumpei/ ushumpei’s blog https://ushumpei.hatenablog.com/ Lean4 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず FizzBuzz の証明を書いてみました。 import Std def fizz_buzz : Nat → String := fun n => if n % 15 = 0 then "FizzBuzz" else if n % 3 = 0 then "Fizz" else if n % 5 = 0 then "Buzz" else toString n -- 15 の倍数で FizzBuzz になることを証明する theorem fizz_buzz_mul… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fushumpei.hatenablog.com%2Fentry%2F2023%2F10%2F30%2F155345" title="Lean4 学習10 - ushumpei’s blog" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2023-10-30 15:53:45 rich https://ushumpei.hatenablog.com/entry/2023/10/30/155345 1.0 100%