Lean4で累積帰納法を証明する

ライセンス この記事上のコードはすべて CC0 (パブリックドメイン) で公開します。 この記事のコードは以下でも公開しています。 Lean4とは Lean4は関数型プログラミング言語のように使える証明支援系です。証明支援系では数学で行われる「証明」を形式化して展開することができます。 注意 この記事では自然数 (\N) は 0 から始まります。 \N = \{0, 1, 2, \cdots\} 数学的帰納法 数学的帰納法について振り返ります。 ある自然数に関する命題 P(n) について、すべての n \in \N で成り立つことを証明するのがゴールです。 P(n) としては以下のような例が考えられます n = n n + 1 = 1 + n n は奇数 \displaystyle\sum_{k=0}^{n} k = \frac{n(n+1)}{2} a_0 = 2, a_{n+1} =