引言

• 最近开始学习Lean 4来做数学证明，虽然挺有挑战，但是对于我这个30多岁的大叔来说有种刚学编程时候探索的乐趣hhh
• 自然数平方差公式这个问题，是我刚学了平方和公式，想变变给自己练手用的，结果卡了我好久，因为要的是自然数，而非整数，所以需要加上大小约束关系，而加上关系之后怎么使用rw规则就晕了
• 最后各种尝试终于搞定小小记录一下
• ps 由于一些语法规则还搞的不是很清楚，现在先记录一下通过编译验证的，一些重要细节的补充，等我学习更深入了再回来补充～

Lean 4 code

theorem square_diff_nat (a b: ℕ) (h: b ≤ a) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := bycalca ^ 2 - b ^ 2= a * a - b * b := by repeat rw [Nat.pow_two]_ = a * a - b * b + 0 := by rw [add_zero (a * a - b * b)]_ = a * a - b * b + (a * b - a * b) := by rw [←Nat.sub_self (a * b)]have h1: a * b ≤ a * b := by rflhave h2: b * b ≤ a * a := Nat.mul_self_le_mul_self hcalc_ = a * a + (a * b - a * b) - b * b  := by rw[←Nat.sub_add_comm h2]_ = a * a + a * b - a * b - b * b := by rw [← Nat.add_sub_assoc h1]_ = a * (a + b) - (b * (a + b)) := by rw[←Nat.mul_add, Nat.sub_sub, ← Nat.add_mul, Nat.mul_comm (a + b) b]_ = (a + b) * (a - b) := by rw [← Nat.sub_mul, Nat.mul_comm]