まだ小学生の頃に習ったことで印象に残っているのは３の倍数の確認方法でした。各桁を足した数が３の倍数ならば元の数も３の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この３の倍数の確認方法の証明を書き下してみようと思いました。自分で定理を形式化して証明を与えることを一通りやるには良いのではないかと思ったのです。 任意桁数の３の倍数で証明しようとすると、その数の10進数展開がk桁あるとして各桁を$a_n$とすると$\sum_{n=0}^{k-1} a_n\,10^n$と表すことができるところから始める必要があります。まだ$\sum$記号を勉強していないこともあり、えいやで３…
