引言 最近开始学习Lean 4来做数学证明，虽然挺有挑战，但是对于我这个30多岁的大叔来说有种刚学编程时候探索的乐趣hhh自然数平方差公式这个问题，是我刚学了平方和公式，想变变给自己练手用的，结果卡了我好久&#xff0c…