Lean4 は Haskell のような純粋関数型言語ですが,より型システムが強力なので,定義した関数が望ましい性質を満たすことを証明することができます. その1例として,ここでは(何番煎じかわかりませんが)フィボナッチ数列を取り上げます.*1 まずはフィボナッチ数列を関数として定義しましょう. /-- フィボナッチ数列の通常の定義をそのまま Lean の関数として書いたもの -/ def fibonacci : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fibonacci n + fibonacci (n + 1) example : [0, 1, 2, …