【解答編】2026年お年賀パズル

この記事は以下の記事の解答編です。

https://zenn.dev/seasawher/articles/27fe1c5344ebf5

問題としてはとてもシンプルで、mod 3 （３で割った余り）で考えればいいです。
そしたら左辺は $0, 1$ にしかならないけど、右辺は $2$ にしかならないので矛盾するという寸法ですね。

import Mathlib.Tactic

theorem theorem_for_2026 (x y : Int) : ¬ y^2 = x^3 + 2 * x + 2 * 2026 := by
  intro h
  -- ZMod 3 にキャストして考える
  replace h : (y : ZMod 3)^2 = (x : ZMod 3)^3 + 2 * (x : ZMod 3) + 2 * 2026 := by
    have := congrArg (Int.cast (R := ZMod 3)) h
    simp only [Int.cast_pow, Int.cast_add, Int.cast_mul, Int.cast_ofNat] at this
    assumption
  -- y^2 は ZMod 3 で 0 か 1
  -- x^3 + 2x + 4052 は ZMod 3 で常に 2
  -- ZMod 3 の元は有限なので decide で確認できる
  have hcontra : ∀ (a b : ZMod 3), b^2 ≠ a^3 + 2 * a + 2 * 2026 := by decide
  exact hcontra (x : ZMod 3) (y : ZMod 3) h

おしまい。