From ec2351769cd8ed449b6dd37bb53a6379f0ef5e1a Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Tue, 26 Sep 2023 14:32:02 +0100
Subject: [PATCH] power world tinkering

---
 Game/Levels/Power/L01zero_pow_zero.lean |  5 ++++-
 Game/Levels/Power/L08pow_pow.lean       | 12 +++++++-----
 Game/Levels/Power/L09add_sq.lean        |  1 +
 Game/Levels/Power/L10FLT.lean           | 11 ++++++++---
 4 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/Game/Levels/Power/L01zero_pow_zero.lean b/Game/Levels/Power/L01zero_pow_zero.lean
index 35afaf0..5e1518c 100644
--- a/Game/Levels/Power/L01zero_pow_zero.lean
+++ b/Game/Levels/Power/L01zero_pow_zero.lean
@@ -10,7 +10,10 @@ namespace MyNat
 
 Introduction "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."
+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."
 
 DefinitionDoc Pow as "^" "
   `Pow a b`, with notation `a ^ b`, is the usual
diff --git a/Game/Levels/Power/L08pow_pow.lean b/Game/Levels/Power/L08pow_pow.lean
index c0f594f..a3411f9 100644
--- a/Game/Levels/Power/L08pow_pow.lean
+++ b/Game/Levels/Power/L08pow_pow.lean
@@ -8,9 +8,9 @@ namespace MyNat
 
 Introduction
 "
-One of the best named levels in the game, a savage `pow_pow` appears
-as the music reaches a frenzy. Could this be the final boss? What
-else could there be to prove about powers?
+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?
 "
 
 LemmaDoc MyNat.pow_pow as "pow_pow" in "Pow" "
@@ -39,9 +39,11 @@ Conclusion
 "
 The music dies down. Is that it?
 
+Course it isn't, you can
+clearly see that there are two worlds left.
+
 A passing mathematician says that mathematicians don't have a name
 for the structure you just constructed. You feel cheated.
 
-Suddenly the music starts up again, and this time you know:
-the final level of power world is next, including the final boss.
+Suddenly the music starts up again. This really is the final boss.
 "
diff --git a/Game/Levels/Power/L09add_sq.lean b/Game/Levels/Power/L09add_sq.lean
index fbb21c8..96a1230 100644
--- a/Game/Levels/Power/L09add_sq.lean
+++ b/Game/Levels/Power/L09add_sq.lean
@@ -42,6 +42,7 @@ in Lean 4!
 It's all over! You have proved a theorem which has tripped up
 schoolkids for generations (some of them think $(a+b)^2=a^2+b^2$).
 If you did it using rewrites, how many did you use? I can do it in 12.
+**TODO** link to source code?
 
 If you didn't play the other worlds like even/odd world yet,
 then feel free to try these next.
diff --git a/Game/Levels/Power/L10FLT.lean b/Game/Levels/Power/L10FLT.lean
index dd93234..abf26b4 100644
--- a/Game/Levels/Power/L10FLT.lean
+++ b/Game/Levels/Power/L10FLT.lean
@@ -8,8 +8,6 @@ namespace MyNat
 
 Introduction
 "
-Second stage!
-
 We now have enough to state mathematically accurate, but slightly
 clunky, version of Fermat's Last Theorem.
 
@@ -27,6 +25,13 @@ and Taylor into Lean, although this task will take many years.
 You can see the current state of his efforts at ...?
 
 **TODO** add info if I get funded.
+
+## 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 **TODO** put link to
+Mathematics In Lean when I'm not in the eurotunnel.
 "
 
 /-- For all naturals $a$ $b$ $c$ and $n$, we have
@@ -39,5 +44,5 @@ LemmaTab "Pow"
 
 Conclusion
 "
-Congratulations! You proved Fermat's Last Theorem!
+Congratulations! You have proved Fermat's Last Theorem!
 "