import MyNat.Power
import AdditionWorld.Level5 -- one_eq_succ_zero
import PowerWorld.Level3 -- pow_one
import AdditionWorld.Level6 -- simp additions
import MultiplicationWorld.Level7 -- add_mul
import MultiplicationWorld.Level9 -- simp additions
namespace MyNat
open MyNat

Power World

Level 8: add_squared

Theorem

For all naturals a and b, we have (a + b)^2 = a^2 + b^2 + 2ab.

The first step in writing this proof is to convert 2 into something we have theorems about, which is 1 and 0.

def 
two: MyNat
two : 
MyNat: Type
MyNat := 
2: MyNat
2
def 
two_eq_succ_one: two = succ 1
two_eq_succ_one : 
two: MyNat
two = 
succ: MyNat → MyNat
succ 
1: MyNat
1 := by
two = succ 1 rfl
Goals accomplished! 🐙
lemma 
one_plus_one: 1 + 1 = 2
one_plus_one : (
1: MyNat
1 : 
MyNat: Type
MyNat) + (
1: MyNat
1 : 
MyNat: Type
MyNat) = (
2: MyNat
2 : 
MyNat: Type
MyNat) := by
1 + 1 = 2 rfl
Goals accomplished! 🐙
-- and we already have one_eq_succ_zero.

Now we are ready to tackle the proof:

lemma 
add_squared: ∀ (a b : MyNat), (a + b) ^ two = a ^ two + b ^ two + 2 * a * b
add_squared (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) :
  (
a: MyNat
a + 
b: MyNat
b) ^ 
two: MyNat
two = 
a: MyNat
a ^ 
two: MyNat
two + 
b: MyNat
b ^ 
two: MyNat
two + 
2: MyNat
2 * 
a: MyNat
a * 
b: MyNat
b := by
a, b: MyNat
(a + b) ^ two = a ^ two + b ^ two + 2 * a * b
  rw [
a, b: MyNat
(a + b) ^ two = a ^ two + b ^ two + 2 * a * b
two_eq_succ_one: two = succ 1
two_eq_succ_one
a, b: MyNat
(a + b) ^ succ 1 = a ^ succ 1 + b ^ succ 1 + 2 * a * b]
a, b: MyNat
(a + b) ^ succ 1 = a ^ succ 1 + b ^ succ 1 + 2 * a * b
  rw [
a, b: MyNat
(a + b) ^ succ 1 = a ^ succ 1 + b ^ succ 1 + 2 * a * b
one_eq_succ_zero: 1 = succ 0
one_eq_succ_zero
a, b: MyNat
(a + b) ^ succ (succ 0) = a ^ succ (succ 0) + b ^ succ (succ 0) + 2 * a * b]
a, b: MyNat
(a + b) ^ succ (succ 0) = a ^ succ (succ 0) + b ^ succ (succ 0) + 2 * a * b
  repeat
a, b: MyNat
(a + b) ^ succ (succ 0) = a ^ succ (succ 0) + b ^ succ (succ 0) + 2 * a * b rw [
a, b: MyNat
(a + b) ^ 0 * (a + b) * (a + b) = a ^ 0 * a * a + b ^ succ (succ 0) + 2 * a * b
pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succ
a, b: MyNat
(a + b) ^ 0 * (a + b) * (a + b) = a ^ 0 * a * a + b ^ succ 0 * b + 2 * a * b]
a, b: MyNat
(a + b) ^ 0 * (a + b) * (a + b) = a ^ succ 0 * a + b ^ succ (succ 0) + 2 * a * b
  repeat
a, b: MyNat
(a + b) ^ 0 * (a + b) * (a + b) = a ^ 0 * a * a + b ^ 0 * b * b + 2 * a * b rw [
a, b: MyNat
1 * (a + b) * (a + b) = a ^ 0 * a * a + b ^ 0 * b * b + 2 * a * b
pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero
a, b: MyNat
1 * (a + b) * (a + b) = 1 * a * a + 1 * b * b + 2 * a * b]
a, b: MyNat
1 * (a + b) * (a + b) = 1 * a * a + b ^ 0 * b * b + 2 * a * b
  repeat
a, b: MyNat
1 * (a + b) * (a + b) = 1 * a * a + 1 * b * b + 2 * a * b rw [
a, b: MyNat
(a + b) * (a + b) = a * a + 1 * b * b + 2 * a * b
one_mul: ∀ (m : MyNat), 1 * m = m
one_mul
a, b: MyNat
(a + b) * (a + b) = a * a + 1 * b * b + 2 * a * b]
a, b: MyNat
(a + b) * (a + b) = a * a + 1 * b * b + 2 * a * b
  rw [
a, b: MyNat
(a + b) * (a + b) = a * a + b * b + 2 * a * b
mul_add: ∀ (t a b : MyNat), t * (a + b) = t * a + t * b
mul_add
a, b: MyNat
(a + b) * a + (a + b) * b = a * a + b * b + 2 * a * b]
a, b: MyNat
(a + b) * a + (a + b) * b = a * a + b * b + 2 * a * b
  repeat
a, b: MyNat
(a + b) * a + (a + b) * b = a * a + b * b + 2 * a * b rw [
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + 2 * a * b
add_mul: ∀ (a b t : MyNat), (a + b) * t = a * t + b * t
add_mul
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + 2 * a * b]
a, b: MyNat
a * a + b * a + (a + b) * b = a * a + b * b + 2 * a * b
  rw [
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + 2 * a * b←
one_plus_one: 1 + 1 = 2
one_plus_one
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 + 1) * a * b]
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 + 1) * a * b
  repeat
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 + 1) * a * b rw [
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 + 1) * a * b
add_mul: ∀ (a b t : MyNat), (a + b) * t = a * t + b * t
add_mul
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 * a * b + 1 * a * b)]
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 * a + 1 * a) * b
  repeat
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 * a * b + 1 * a * b) rw [
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (1 * a * b + 1 * a * b)
one_mul: ∀ (m : MyNat), 1 * m = m
one_mul
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (a * b + a * b)]
a, b: MyNat
a * a + b * a + (a * b + b * b) = a * a + b * b + (a * b + a * b)
  simp
Goals accomplished! 🐙

It is also helpful to teach simp our new tricks:

attribute [simp] 
pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succ 
pow_one: ∀ (a : MyNat), a ^ 1 = a
pow_one 
pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero

There is some fun discussion on Lean3 Zulip about different ways to solve this one in fewer steps. Feel free to try some of those solutions here, just note that the Lean 4 syntax is a bit different, no commands between tactics, and square brackets are required on the rw tactic.

Do you fancy doing (a+b)^3 now? You might want to read this Xena Project blog post before you start though.

If you got this far -- very well done! If you only learnt the three tactics rw, induction and refl then there are now more tactics to learn; time to try Function World.

The main thing we really want to impress upon people is that we believe that all of pure mathematics can be done in this new way.

The Liquid Tensor Experiment shows that Lean3 could be used to prove very large math theorems.

Lean 3 also has a definition of perfectoid spaces (a very complex modern mathematical structure). We believe that these systems will one day cause a paradigm shift in the way mathematics is done, but first we need to build what we know, or at least build enough to state what we mathematicians believe.

If you want to get involved, come and join us at the Zulip Lean chat. The #new members stream is a great place to start asking questions.

Next up Function World.