diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot
index 1efd046..f4b2da4 100644
--- a/.i18n/en/Game.pot
+++ b/.i18n/en/Game.pot
@@ -721,7 +721,8 @@ msgid "## Summary\n"
 msgstr ""
 
 #: Game.Levels.Addition.L05add_right_comm
-msgid "`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n"
+msgid ""
+"`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n"
 "\n"
 "In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\n"
 "as `a + b + c = a + c + b`."
@@ -927,7 +928,8 @@ msgid "`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b
 msgstr ""
 
 #: Game.Levels.Multiplication.L07mul_add
-msgid "Multiplication distributes\n"
+msgid ""
+"Multiplication distributes\n"
 "over addition on the left.\n"
 "\n"
 "`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`."
@@ -962,7 +964,9 @@ msgid "add_left_eq_self"
 msgstr ""
 
 #: Game.Levels.Multiplication
-msgid "How should we define `37 * x`? Just like addition, we need to give definitions\n"
+msgid ""
+"How should we define `37 * x`? Just like addition, we need to give "
+"definitions\n"
 "when $x=0$ and when $x$ is a successor.\n"
 "\n"
 "The zero case is easy: we define `37 * 0` to be `0`. Now say we know\n"
@@ -974,8 +978,10 @@ msgid "How should we define `37 * x`? Just like addition, we need to give defini
 "  * `mul_zero a : a * 0 = 0`\n"
 "  * `mul_succ a d : a * succ d = a * d + a`\n"
 "\n"
-"In this world, we must not only prove facts about multiplication like `a * b = b * a`,\n"
-"we must also prove facts about how multiplication interacts with addition, like `a * (b + c) = a * b + a * c`.\n"
+"In this world, we must not only prove facts about multiplication like `a * b "
+"= b * a`,\n"
+"we must also prove facts about how multiplication interacts with addition, "
+"like `a * (b + c) = a * b + a * c`.\n"
 "Let's get started."
 msgstr ""
 
@@ -1367,7 +1373,8 @@ msgid "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`."
 msgstr ""
 
 #: Game.Levels.Implication.L04succ_inj
-msgid "# Statement\n"
+msgid ""
+"# Statement\n"
 "\n"
 "If $a$ and $b$ are numbers, then\n"
 "`succ_inj a b` is the proof that\n"
@@ -1384,7 +1391,8 @@ msgid "# Statement\n"
 "You can think of `succ_inj` itself as a proof; it is the proof\n"
 "that `succ` is an injective function. In other words,\n"
 "`succ_inj` is a proof of\n"
-"$\\forall a, b \\in  \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
+"$\\forall a, b \\in  \\mathbb{N}, ( \\operatorname{succ}(a) = "
+"\\operatorname{succ}(b)) \\implies a=b$.\n"
 "\n"
 "`succ_inj` was postulated as an axiom by Peano, but\n"
 "in Lean it can be proved using `pred`, a mathematically\n"
@@ -1734,7 +1742,8 @@ msgid "If `a` and `b` are numbers, then `succ_inj a b` is a proof\n"
 msgstr ""
 
 #: Game.Levels.Algorithm.L02add_algo1
-msgid "In some later worlds, we're going to see some much nastier levels,\n"
+msgid ""
+"In some later worlds, we're going to see some much nastier levels,\n"
 "like `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\n"
 "Brackets need to be moved around, and variables need to be swapped.\n"
 "\n"
@@ -2145,7 +2154,8 @@ msgid "We now have enough to prove that multiplication is associative,\n"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L04add_right_eq_self
-msgid "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n"
+msgid ""
+"`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n"
 "Two ways to do it spring to mind; I'll mention them when you've solved it."
 msgstr ""
 
@@ -2167,23 +2177,33 @@ msgid "Now finish in one line."
 msgstr ""
 
 #: Game.Levels.AdvAddition.L05add_right_eq_zero
-msgid "The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\n"
+msgid ""
+"The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` "
+"and `b = 0`.\n"
 "Let's prove one of these facts in this level, and the other in the next.\n"
 "\n"
 "## A new tactic: `cases`\n"
 "\n"
-"The `cases` tactic will split an object or hypothesis up into the possible ways\n"
+"The `cases` tactic will split an object or hypothesis up into the possible "
+"ways\n"
 "that it could have been created.\n"
 "\n"
-"For example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\n"
-"but don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\n"
-"In this situation you can use `cases b with d` instead. There are two ways to make\n"
-"a number: it's either zero or a successor. So you will end up with two goals, one\n"
+"For example, sometimes you want to deal with the two cases `b = 0` and `b = "
+"succ d` separately,\n"
+"but don't need the inductive hypothesis `hd` that comes with `induction b "
+"with d hd`.\n"
+"In this situation you can use `cases b with d` instead. There are two ways "
+"to make\n"
+"a number: it's either zero or a successor. So you will end up with two "
+"goals, one\n"
 "with `b = 0` and one with `b = succ d`.\n"
 "\n"
-"Another example: if you have a hypothesis `h : False` then you are done, because a false statement implies\n"
-"any statement. Here `cases h` will close the goal, because there are *no* ways to\n"
-"make a proof of `False`! So you will end up with no goals, meaning you have proved everything."
+"Another example: if you have a hypothesis `h : False` then you are done, "
+"because a false statement implies\n"
+"any statement. Here `cases h` will close the goal, because there are *no* "
+"ways to\n"
+"make a proof of `False`! So you will end up with no goals, meaning you have "
+"proved everything."
 msgstr ""
 
 #: Game
@@ -2240,7 +2260,8 @@ msgid "Let's now begin our approach to the final boss,\n"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L06add_left_eq_zero
-msgid "How about this for a proof:\n"
+msgid ""
+"How about this for a proof:\n"
 "\n"
 "```\n"
 "rw [add_comm]\n"
@@ -2640,7 +2661,8 @@ msgid "Let's now learn about Peano's second axiom for addition, `add_succ`."
 msgstr ""
 
 #: Game.Levels.LessOrEqual.L09succ_le_succ
-msgid "Here's my proof:\n"
+msgid ""
+"Here's my proof:\n"
 "```\n"
 "cases hx with d hd\n"
 "use d\n"
@@ -2980,15 +3002,18 @@ msgid "For all natural numbers $a$ and $b$, we have\n"
 msgstr ""
 
 #: Game.Levels.AdvMultiplication.L06mul_right_eq_one
-msgid "# Summary\n"
+msgid ""
+"# Summary\n"
 "\n"
-"The `have` tactic can be used to add new hypotheses to a level, but of course\n"
+"The `have` tactic can be used to add new hypotheses to a level, but of "
+"course\n"
 "you have to prove them.\n"
 "\n"
 "\n"
 "## Example\n"
 "\n"
-"The simplest usage is like this. If you have `a` in your context and you execute\n"
+"The simplest usage is like this. If you have `a` in your context and you "
+"execute\n"
 "\n"
 "`have ha : a = 0`\n"
 "\n"
@@ -3302,7 +3327,8 @@ msgid "`zero_mul x` is the proof that `0 * x = 0`.\n"
 msgstr ""
 
 #: Game
-msgid "# Welcome to the Natural Number Game\n"
+msgid ""
+"# Welcome to the Natural Number Game\n"
 "#### An introduction to mathematical proof.\n"
 "\n"
 "In this game, we will build the basic theory of the natural\n"
@@ -3322,12 +3348,15 @@ msgid "# Welcome to the Natural Number Game\n"
 "Note: this is a new Lean 4 version of the game containing several\n"
 "worlds which were not present in the old Lean 3 version. More new worlds\n"
 "such as Strong Induction World, Even/Odd World and Prime Number World\n"
-"are in development; if you want to see their state or even help out, checkout\n"
-"out the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues).\n"
+"are in development; if you want to see their state or even help out, "
+"checkout\n"
+"out the [issues in the github repo](https://github.com/leanprover-community/"
+"NNG4/issues).\n"
 "\n"
 "## More\n"
 "\n"
-"Click on the three lines in the top right and select \"Game Info\" for resources,\n"
+"Click on the three lines in the top right and select \"Game Info\" for "
+"resources,\n"
 "links, and ways to interact with the Lean community."
 msgstr ""