【問題編】2026年お年賀パズル

もうすぐ2026年ということで、2026にちなんだパズルを作ってみました。
どういう問題かというと、こんな感じです：

$y^2 = x^3 + 2 * x + 2 * 2026$ という方程式に整数解がないことを証明してください。

以下の sorry の部分を埋めて証明を完成させてください。

import Mathlib.Tactic

theorem theorem_for_2026 (x y : Int) : ¬ y^2 = x^3 + 2 * x + 2 * 2026 := by
  sorry

ヒント

この形の多項式は楕円曲線と言われる奴ですが、楕円曲線の知識はなんもいりません。たぶん高校生でも解けるやつです。