Mathematicians sometimes debate what 0 ^ 0 is; the answer depends, of course, on your definitions. In this game, 0 ^ 0 = 1. See if you can prove it.

Check out the Pow tab in your list of theorems to see the new proofs which are available.

0 ^ 0 = 1

New: pow_zero

pow_zero a : a ^ 0 = 1 is one of the two axioms defining exponentiation in this game.

New: ^

Pow a b, with notation a ^ b, is the usual exponentiation of natural numbers. Internally it is defined via two axioms:

• pow_zero a : a ^ 0 = 1

• pow_succ a b : a ^ succ b = a ^ b * a

Note in particular that 0 ^ 0 = 1.

theorem zero_pow_zero : (0 : ℕ) ^ 0 = 1

We've just seen that 0 ^ 0 = 1, but if n is a successor, then 0 ^ n = 0. We prove that here.

For all numbers m, 0 ^{\operatorname{succ} (m)} = 0.

New: pow_succ

pow_succ a b : a ^ (succ b) = a ^ b * a is one of the two axioms defining exponentiation in this game.

theorem zero_pow_succ (m : ℕ) : (0 : ℕ) ^ (succ m) = 0

For all naturals a, a ^ 1 = a.

theorem pow_one (a : ℕ) : a ^ 1 = a

For all naturals m, 1 ^ m = 1.

theorem one_pow (m : ℕ) : (1 : ℕ) ^ m = 1

Note: this lemma will be useful for the final boss!

For all naturals a, a ^ 2 = a \times a.

theorem pow_two (a : ℕ) : a ^ 2 = a * a

Let's now begin our approach to the final boss, by proving some more subtle facts about powers.

For all naturals a, m, n, we have a^{m + n} = a ^ m a ^ n.

theorem pow_add (a m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n

The music gets ever more dramatic, as we explore the interplay between exponentiation and multiplication.

If you're having trouble exchanging the right a * b because rw [mul_comm] swaps the wrong multiplication, then read the documentation of rw for tips on how to fix this.

For all naturals a, b, n, we have (ab) ^ n = a ^ nb ^ n.

theorem mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n

One of the best named levels in the game, a savage pow_pow sub-boss appears as the music reaches a frenzy. What else could there be to prove about powers after this?

For all naturals a, m, n, we have (a ^ m) ^ n = a ^ {mn}.

theorem pow_pow (a m n : ℕ) : (a ^ m) ^ n = a ^ (m * n)

[final boss music]

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

theorem add_sq (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

We now have enough to state a mathematically accurate, but slightly clunky, version of Fermat's Last Theorem.

Fermat's Last Theorem states that if x,y,z>0 and m \geq 3 then x^m+y^m\not =z^m. If you didn't do inequality world yet then we can't talk about m \geq 3, so we have to resort to the hack of using n + 3 for m, which guarantees it's big enough. Similarly instead of x > 0 we use a + 1.

This level looks superficially like other levels we have seen, but the shortest solution known to humans would translate into many millions of lines of Lean code. The author of this game, Kevin Buzzard, is working on translating the proof by Wiles and Taylor into Lean, although this task will take many years.

CONGRATULATIONS!

You've finished the main quest of the natural number game! If you would like to learn more about how to use Lean to prove theorems in mathematics, then take a look at Mathematics In Lean, an interactive textbook which you can read in your browser, and which explains how to work with many more mathematical concepts in Lean.

For all naturals a b c and n, we have (a+1)^{n+3}+(b+1)^{n+3}\not=(c+1)^{n+3}.

example (a b c n : ℕ) : (a + 1) ^ (n + 3) + (b + 1) ^ (n + 3) ≠ (c + 1) ^ (n + 3)