diff --git a/.gitignore b/.gitignore
index 32f4763..69db1e9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@ build/
 lake-packages/
 .lake/
 **/.DS_Store
+.i18n/*.mo
diff --git a/.i18n/Game-zh_CN.po b/.i18n/Game-zh_CN.po
new file mode 100644
index 0000000..bbe5470
--- /dev/null
+++ b/.i18n/Game-zh_CN.po
@@ -0,0 +1,5296 @@
+#
+#, fuzzy
+msgid ""
+msgstr ""
+"Project-Id-Version: Game v4.6.0\n"
+"Report-Msgid-Bugs-To: \n"
+"POT-Creation-Date: Mon Mar 18 16:33:40 2024\n"
+"PO-Revision-Date: \n"
+"Last-Translator: \n"
+"Language-Team: none\n"
+"Language: zh_CN\n"
+"MIME-Version: 1.0\n"
+"Content-Type: text/plain; charset=UTF-8\n"
+"Content-Transfer-Encoding: 8bit\n"
+"X-Generator: Poedit 3.4.2\n"
+
+#: Game.Levels.Tutorial.L01rfl
+msgid "The rfl tactic"
+msgstr "rfl策略"
+
+#: Game.Levels.Tutorial.L01rfl
+msgid ""
+"## Summary\n"
+"\n"
+"`rfl` proves goals of the form `X = X`.\n"
+"\n"
+"In other words, the `rfl` tactic will close any goal of the\n"
+"form `A = B` if `A` and `B` are *identical*.\n"
+"\n"
+"`rfl` is short for \"reflexivity (of equality)\".\n"
+"\n"
+"## Example:\n"
+"\n"
+"If the goal looks like this:\n"
+"\n"
+"```\n"
+"x + 37 = x + 37\n"
+"```\n"
+"\n"
+"then `rfl` will close it. But if it looks like `0 + x = x` then `rfl` won't work, because even\n"
+"though $0+x$ and $x$ are always equal as *numbers*, they are not equal as *terms*.\n"
+"The only term which is identical to `0 + x` is `0 + x`.\n"
+"\n"
+"## Details\n"
+"\n"
+"`rfl` is short for \"reflexivity of equality\".\n"
+"\n"
+"## Game Implementation\n"
+"\n"
+"*Note that our `rfl` is weaker than the version used in core Lean and `mathlib`,\n"
+"for pedagogical purposes; mathematicians do not distinguish between propositional\n"
+"and definitional equality because they think about definitions in a different way\n"
+"to type theorists (`zero_add` and `add_zero` are both \"facts\" as far\n"
+"as mathematicians are concerned, and who cares what the definition of addition is).*"
+msgstr ""
+"## 小结\n"
+"\n"
+"`rfl` 证明形如 `X = X` 的目标。\n"
+"\n"
+"换句话说，如果 `A` 和 `B` *完全相同*，`rfl` 策略将关闭任何形如 `A = B` 的目标。\n"
+"\n"
+"`rfl` 是 “reflexivity（等价关系的反身性）”的缩写。\n"
+"\n"
+"## 示例：\n"
+"\n"
+"如果目标如下：\n"
+"\n"
+"```\n"
+"x + 37 = x + 37\n"
+"```\n"
+"\n"
+"那么 `rfl` 将关闭（译注：这个的关闭是证明的意思）它。但如果它看起来像 `0 + x = x`，那么 `rfl` 将无法工作，因为即使 $0+x$ 和 $x$ 作为*数字*总是相等，但它们作为*项*并不相等。唯一与 `0 + x` 相同的项是 `0 + x`。\n"
+"\n"
+"\n"
+"## 详细信息\n"
+"\n"
+"`rfl` 是 “reflexivity of equality（等价关系的反身性）”的缩写。\n"
+"\n"
+"## 游戏实现\n"
+"\n"
+"*请注意，出于教学目的，我们的 `rfl` 比核心 Lean 和 `mathlib` 中使用的版本弱一些；数学家不区分命题等价和定义等价，因为他们以不同于类型理论家的方式思考定义（就数学家而言，`zero_add` 和 `add_zero` 都是 “事实”，谁会在乎加法的定义是什么呢）。*\n"
+"（译注：因为 `add_zero` 是加法定义的一部分，而定义等价是可以直接用 `rfl` 证明的。也就是说 `x + 0 = x` 可以用 `rfl` 证明。所以作者多了一嘴，但实际上因为很少有人知道类型理论家怎么思考，所以这个注解看起来会有些奇怪。）"
+
+#: Game.Levels.Tutorial.L01rfl
+msgid ""
+"\n"
+"# Read this first\n"
+"\n"
+"Each level in this game involves proving a mathematical theorem (the \"Goal\").\n"
+"The goal will be a statement about *numbers*. Some numbers in this game have known values.\n"
+"Those numbers have names like $37$. Other numbers will be secret. They're called things\n"
+"like $x$ and $q$. We know $x$ is a number, we just don't know which one.\n"
+"\n"
+"In this first level we're going to prove the theorem that $37x + q = 37x + q$.\n"
+"You can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`\n"
+"are numbers.\n"
+"\n"
+"We solve goals in Lean using *Tactics*, and the first tactic we're\n"
+"going to learn is called `rfl`, which proves all theorems of the form $X = X$.\n"
+"\n"
+"Prove that $37x+q=37x+q$ by executing the `rfl` tactic.\n"
+msgstr ""
+"\n"
+"# 首先阅读此内容\n"
+"\n"
+"这个游戏中的每个关卡都涉及到证明一个数学定理（“目标”）。目标将是关于 *自然数* 的陈述。这个游戏中的一些数有已知的值。这些数有像 $37$ 这样的名字。其他数将是秘密的。它们被称为像 $x$ 和 $q$ 这样的名字。我们知道 $x$ 是一个自然数，我们只是不知道它是哪一个。\n"
+"\n"
+"在这个第一层中，我们将证明定理 $37x + q = 37x + q$。你可以在下面的*对象*中看到 `x q : ℕ`，这意味着 `x` 和 `q` 是自然数。\n"
+"\n"
+"我们使用*策略*在 Lean 中解决目标，我们要学习的第一个策略叫做 `rfl`，它证明了所有形式为 $X = X$ 的定理。\n"
+"\n"
+"通过执行 `rfl` 策略来证明 $37x+q=37x+q$。\n"
+
+#: Game.Levels.Tutorial.L01rfl
+msgid "If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$"
+msgstr "如果 $x$ 和 $q$ 是任意自然数，那么 $37x+q=37x+q$ 。"
+
+#: Game.Levels.Tutorial.L01rfl
+msgid ""
+"In order to use the tactic `rfl` you can enter it in the text box\n"
+"under the goal and hit \"Execute\"."
+msgstr "要使用策略 \"rfl\"，您可以在目标下的文本框中输入它，然后点击 \"执行\"。"
+
+#: Game.Levels.Tutorial.L01rfl
+msgid ""
+"\n"
+"Congratulations! You completed your first verified proof!\n"
+"\n"
+"Remember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,\n"
+"you can click on `rfl` in the list of tactics on the right.\n"
+"\n"
+"Now click on \"Next\" to learn about the `rw` tactic.\n"
+msgstr ""
+"\n"
+"恭喜！你完成了你的第一个经过验证的证明！\n"
+"\n"
+"请记住，`rfl` 是一个*策略*。如果你想要了解关于 `rfl` 策略的信息，你可以点击右侧策略列表中的 `rfl`。\n"
+"\n"
+"现在点击“下一个”来学习 `rw` 策略。\n"
+
+#: Game.Levels.Tutorial.L02rw
+msgid "the rw tactic"
+msgstr "rw 策略"
+
+#: Game.Levels.Tutorial.L02rw
+msgid ""
+"## Summary\n"
+"\n"
+"If `h` is a proof of an equality `X = Y`, then `rw [h]` will change\n"
+"all `X`s in the goal to `Y`s. It's the way to \"substitute in\".\n"
+"\n"
+"## Variants\n"
+"\n"
+"* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n"
+"\n"
+"* `rw [h1, h2]` (a sequence of rewrites)\n"
+"\n"
+"* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n"
+"\n"
+"* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\n"
+"get the `⊢` symbol with `\\|-`.)\n"
+"\n"
+"* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\n"
+"until there are no more matches for `? + 0`.\n"
+"\n"
+"* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n"
+"\n"
+"### Example:\n"
+"\n"
+"If you have the assumption `h : x = y + y` and your goal is\n"
+"```\n"
+"succ (x + 0) = succ (y + y)\n"
+"```\n"
+"\n"
+"then\n"
+"\n"
+"`rw [add_zero]`\n"
+"\n"
+"will change the goal into `succ x = succ (y + y)`, and then\n"
+"\n"
+"`rw [h]`\n"
+"\n"
+"will change the goal into `succ (y + y) = succ (y + y)`, which\n"
+"can be solved with `rfl`.\n"
+"\n"
+"### Example:\n"
+"\n"
+"You can use `rw` to change a hypothesis as well.\n"
+"For example, if you have two hypotheses\n"
+"```\n"
+"h1 : x = y + 3\n"
+"h2 : 2 * y = x\n"
+"```\n"
+"then `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n"
+"\n"
+"## Common errors\n"
+"\n"
+"* You need the square brackets. `rw h` is never correct.\n"
+"\n"
+"* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\n"
+"for example if `h` is a function or an implication,\n"
+"then `rw` is not the tactic you want to use. For example,\n"
+"`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\n"
+"not the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n"
+"\n"
+"## Details\n"
+"\n"
+"The `rw` tactic is a way to do \"substituting in\". There\n"
+"are two distinct situations where you can use this tactic.\n"
+"\n"
+"1) Basic usage: if `h : A = B` is an assumption or\n"
+"the proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\n"
+"will change them all to `B`'s. The tactic will error\n"
+"if there are no `A`s in the goal.\n"
+"\n"
+"2) Advanced usage: Assumptions coming from theorem proofs\n"
+"often have missing pieces. For example `add_zero`\n"
+"is a proof that `? + 0 = ?` because `add_zero` really is a function,\n"
+"and `?` is the input. In this situation `rw` will look through the goal\n"
+"for any subterm of the form `x + 0`, and the moment it\n"
+"finds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n"
+"\n"
+"Exercise: think about why `rw [add_zero]` changes the term\n"
+"`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n"
+"`0 + (x + 0) + 0 + (x + 0)`\n"
+"\n"
+"If you can't remember the name of the proof of an equality, look it up in\n"
+"the list of lemmas on the right.\n"
+"\n"
+"## Targetted usage\n"
+"\n"
+"If your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\n"
+"to `c + a`, then `rw [add_comm]` will not work because Lean finds another\n"
+"addition first and swaps those inputs instead. Use `rw [add_comm a c]` to\n"
+"guarantee that Lean rewrites `a + c` to `c + a`. This works because\n"
+"`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\n"
+"that `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n"
+"\n"
+"If `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\n"
+"If you only want to change the 37th occurrence of `X`\n"
+"to `Y` then do `nth_rewrite 37 [h]`."
+msgstr ""
+"## 摘要\n"
+"\n"
+"如果 `h` 是等式 `X = Y` 的证明，那么 `rw [h]` 将改变\n"
+"目标中的所有 `X`s 变为 `Y`s。这是 \"代入 \"的方法。\n"
+"\n"
+"## Variants\n"
+"\n"
+"* `rw [← h]` （将 `Y`s 更改为 `X`s；通过输入 `\\left ` 或 `\\l` 获取后箭头）。\n"
+"\n"
+"* `rw [h1, h2]`（重写序列）\n"
+"\n"
+"* `rw [h] at h2`（将假设 `h2` 中的 `X`s 改为 `Y`s）\n"
+"\n"
+"* `rw [h] at h1 h2 ⊢` （将两个假设和目标中的 `X`s 改为 `Y`s；\n"
+"用 `\\|-` 获取 `⊢` 符号）。\n"
+"\n"
+"* `repeat rw [add_zero]` 将继续将 `? + 0` 更改为 `?`。\n"
+"直到没有更多匹配的 `? + 0`。\n"
+"\n"
+"* `nth_rewrite 2 [h]` 只会将目标中的第二个 `X` 改为 `Y`。\n"
+"\n"
+"#### 示例：\n"
+"\n"
+"如果假设为 `h : x = y + y`，目标为\n"
+"```.\n"
+"succ (x + 0) = succ (y + y)\n"
+"```.\n"
+"\n"
+"则\n"
+"\n"
+"`rw [add_zero]`\n"
+"\n"
+"会将目标改为 `succ x = succ (y + y)`，然后\n"
+"\n"
+"`rw [h]`\n"
+"\n"
+"会将目标变为 `succ (y + y) = succ (y + y)`，这\n"
+"可以用 `rfl` 解决。\n"
+"\n"
+"#### 示例：\n"
+"\n"
+"你也可以用 `rw` 来改变一个假设。\n"
+"例如，如果您有两个假设\n"
+"```\n"
+"h1 : x = y + 3\n"
+"h2 : 2 * y = x\n"
+"```\n"
+"则 `rw [h1] at h2` 将把 `h2` 变为 `h2 : 2 * y = y + 3`。\n"
+"-/\n"
+"\n"
+"## 常见错误\n"
+"\n"
+"* 需要方括号。`rw h` 永远不会正确。\n"
+"\n"
+"* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的语句）、\n"
+"例如，如果 `h` 是一个函数或蕴涵、\n"
+"那么 `rw` 就不是您要使用的策略。例如\n"
+"`rw [P = Q]` 绝对不正确：`P = Q` 是定理*陈述、\n"
+"而不是证明。如果 `h : P = Q` 是证明，那么 `rw [h]` 也可以。\n"
+"\n"
+"## 详情\n"
+"\n"
+"`rw` 策略是 \"代入 \"的一种方法。有\n"
+"有两种不同的情况可以使用这种策略。\n"
+"\n"
+"1) 基本用法：如果 `h : A = B` 是一个假设或\n"
+"如果目标包含一个或多个 `A`s，那么 `rw [h]`\n"
+"会将它们全部改为 `B`。如果没有 OFeTl\n"
+"如果目标中没有 `A`s。\n"
+"\n"
+"2) 高级用法：来自定理证明的假设\n"
+"通常会有缺失。例如 `add_zero`\n"
+"是 `? + 0 = ?` 的证明，因为 `add_zero` 确实是一个函数、\n"
+"而 `?` 是输入。在这种情况下，`rw` 将在目标中查找\n"
+"寻找任何形式为 `x + 0` 的子项。\n"
+"就会将 `?` 固定为 `x`，然后将所有 `x + 0` 改为 `x`s。\n"
+"\n"
+"练习：想一想为什么 `rw [add_zero]` 会改变术语\n"
+"`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为\n"
+"`0 + (x + 0) + 0 + (x + 0)`\n"
+"\n"
+"如果您记不起相等证明的名称，请在\n"
+"右侧的公例列表中查找。\n"
+"\n"
+"## 目标用法\n"
+"\n"
+"如果您的目标是 `b + c + a = b + (a + c)`，而您想将 `a + c` 重写为\n"
+"为 `c + a`，那么 `rw [add_comm]` 将不起作用，因为 Lean 会先找到另一个加法，然后交换这些输入\n"
+"加法，并交换这些输入。使用 `rw [add_comm a c]` 来\n"
+"保证Lean将 `a + c` 改写为 `c + a`。这是因为\n"
+"`add_comm` 是 `?1 + ?2 = ?2 + ?1` 的证明，`add_comm a` 是 RKKlMOjb8Agf07H9 的证明。\n"
+"是 `a + ? = ? + a` 的证明，而 `add_comm a c` 是 `a + c = c + a` 的证明。\n"
+"\n"
+"如果是 `h : X = Y`，那么 `rw [h]` 将把所有 `X`s 变为 `Y`s。\n"
+"如果您只想将第 37 次出现的 `X`\n"
+"改为 `Y`，则执行 `nth_rewrite 37 [h]`。"
+
+#: Game.Levels.Tutorial.L02rw
+msgid ""
+"## Summary\n"
+"\n"
+"`repeat t` repeatedly applies the tactic `t`\n"
+"to the goal. You don't need to use this\n"
+"tactic, it just speeds things up sometimes.\n"
+"\n"
+"## Example\n"
+"\n"
+"`repeat rw [add_zero]` will turn the goal\n"
+"`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\n"
+"into the goal\n"
+"`a = b`.\n"
+"\"\n"
+"\n"
+"TacticDoc nth_rewrite \"\n"
+msgstr ""
+"## 摘要\n"
+"\n"
+"`repeat t` 反复应用策略 `t` 到目标上。这个是个可选策略，它只是有时可以节省步骤。\n"
+"\n"
+"## 示例\n"
+"\n"
+"`repeat rw [add_zero]` 会将目标\n"
+"`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\n"
+"变为\n"
+"`a = b`。\n"
+"\n"
+
+#: Game.Levels.Tutorial.L02rw
+msgid ""
+"## Summary\n"
+"\n"
+"If `h : X = Y` and there are several `X`s in the goal, then\n"
+"`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n"
+"\n"
+"## Example\n"
+"\n"
+"If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\n"
+"will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\n"
+"will change the goal to `succ 1 + succ 1 = 4`."
+msgstr ""
+"## 小结\n"
+"\n"
+"如果 `h : X = Y` 并且在目标中有多个 `X`，那么 `nth_rewrite 3 [h]` 将仅更改第三个 `X` 为 `Y`。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果目标是 `2 + 2 = 4`，那么 `nth_rewrite 2 [two_eq_succ_one]` 将目标更改为 `2 + succ 1 = 4`。相比之下，`rw [two_eq_succ_one]` 将目标更改为 `succ 1 + succ 1 = 4`。"
+
+#: Game.Levels.Tutorial.L02rw
+msgid ""
+"\n"
+"In this level the *goal* is $2y=2(x+7)$ but to help us we\n"
+"have an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\n"
+"your list of assumptions. Lean thinks of `h` as being a secret proof of the\n"
+"assumption, rather like `x` is a secret number.\n"
+"\n"
+"Before we can use `rfl`, we have to \"substitute in for $y$\".\n"
+"We do this in Lean by *rewriting* the proof `h`,\n"
+"using the `rw` tactic.\n"
+msgstr ""
+"\n"
+"在这个关卡中，*目标*是 $2y=2(x+7)$，但为了帮助我们，我们有一个*假设* `h` 表明 $y = x + 7$。检查你是否能在假设列表中看到 `h`。Lean 将 `h` 视为假设的一个秘密证明，有点像 `x` 是一个秘密数字。（译注，原文里的秘密在中文中其实并不是很容易理解，我觉得可以简单的认为是不特定的意思。）\n"
+"\n"
+"在我们能使用 `rfl` 之前，我们需要“代入 $y$”。我们通过*重写*证明 `h` 来在 Lean 中做到这一点，使用的是 `rw` 策略。\n"
+
+#: Game.Levels.Tutorial.L02rw
+msgid "If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$."
+msgstr "如果 $x$ 和 $y$ 是自然数，并且 $y = x + 7$，那么 $2y = 2(x + 7)$。"
+
+#: Game.Levels.Tutorial.L02rw
+msgid "First execute `rw [h]` to replace the `y` with `x + 7`."
+msgstr "首先执行 `rw [h]` 将 `y` 替换为 `x + 7`。"
+
+#: Game.Levels.Tutorial.L02rw
+msgid "Can you take it from here? Click on \"Show more help!\" if you need a hint."
+msgstr "你能从这里开始吗？如果您需要提示，请点击 \"显示更多帮助！\"。"
+
+#: Game.Levels.Tutorial.L02rw
+msgid "Now `rfl` will work."
+msgstr "现在 `rfl` 可以工作了。"
+
+#: Game.Levels.Tutorial.L02rw
+msgid "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey.\n"
+msgstr "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey.\n"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "Numbers"
+msgstr "数字"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid ""
+"`ℕ` is the natural numbers, just called \"numbers\" in this game. It's\n"
+"defined via two rules:\n"
+"\n"
+"* `0 : ℕ` (zero is a number)\n"
+"* `succ (n : ℕ) : ℕ` (the successor of a number is a number)\n"
+"\n"
+"## Game Implementation\n"
+"\n"
+"*The game uses its own copy of the natural numbers, called `MyNat` with notation `ℕ`.\n"
+"It is distinct from the Lean natural numbers `Nat`, which should hopefully\n"
+"never leak into the natural number game.*"
+msgstr ""
+"`ℕ` 是自然数，在这个游戏中简称为“数字”。（译注：这个简称在本翻译中很少用到，一般都重新改写为自然数。因为汉语中这样使用很不自然。但是仍然有存在遗漏未改写的，在本游戏中，如果没有强调，几乎所有的数字指的都是自然数。）它通过两条规则定义：\n"
+"\n"
+"* `0 : ℕ`（零是自然数）\n"
+"* `succ (n : ℕ) : ℕ`（自然数的后继数是自然数）\n"
+"\n"
+"## 游戏实现\n"
+"\n"
+"*游戏使用自己复制的自然数，称为 `MyNat`，标记为 `ℕ`。它不同于 Lean 自然数 `Nat`，后者不应泄露到自然数游戏中。*"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "`one_eq_succ_zero` is a proof of `1 = succ 0`.\""
+msgstr "`one_eq_succ_zero` 是 `1 = succ 0`的证明。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "`two_eq_succ_one` is a proof of `2 = succ 1`."
+msgstr "`two_eq_succ_one` 是 `2 = succ 1` 的证明。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "`three_eq_succ_two` is a proof of `3 = succ 2`."
+msgstr "`three_eq_succ_two` 是 `3 = succ 2` 的证明。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "`four_eq_succ_three` is a proof of `4 = succ 3`."
+msgstr "`four_eq_succ_three` 是 `4 = succ 3` 的证明。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid ""
+"\n"
+"## The birth of number.\n"
+"\n"
+"Numbers in Lean are defined by two rules.\n"
+"\n"
+"* `0` is a number.\n"
+"* If `n` is a number, then the *successor* `succ n` of `n` is a number.\n"
+"\n"
+"The successor of `n` means the number after `n`. Let's learn to\n"
+"count, and name a few small numbers.\n"
+"\n"
+"## Counting to four.\n"
+"\n"
+"`0` is a number, so `succ 0` is a number. Let's call this new number `1`.\n"
+"Similarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.\n"
+"This gives us plenty of numbers to be getting along with.\n"
+"\n"
+"The *proof* that `2 = succ 1` is called `two_eq_succ_one`.\n"
+"Check out the \"012\" tab in the list of lemmas on the right\n"
+"for this and other proofs.\n"
+"\n"
+"Let's prove that $2$ is the number after the number after zero.\n"
+msgstr ""
+"\n"
+"## 自然数的诞生\n"
+"\n"
+"Lean中的自然数是根据两条规则定义的。\n"
+"\n"
+"* `0` 是一个自然数。\n"
+"* 如果 `n` 是一个自然数，那么`n`的*后继数* `succ n` 也是一个自然数。\n"
+"\n"
+"`n`的后继数意味着在`n`之后的自然数。让我们学会数数，并给一些小数字命名。\n"
+"\n"
+"## 数到四。\n"
+"\n"
+"`0` 是一个自然数，所以 `succ 0` 也是一个自然数。让我们称这个新自然数为 `1`。\n"
+"类似地，我们定义 `2 = succ 1`、`3 = succ 2` 和 `4 = succ 3`。\n"
+"这给了我们足够的数字来继续后面的关卡。\n"
+"\n"
+"证明 `2 = succ 1` 的*证明*被称为 `two_eq_succ_one`。\n"
+"查看右侧引理列表中的“012”标签，了解这个以及其他证明。\n"
+"\n"
+"让我们证明 $2$ 是零之后再之后的数字。\n"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0 Game.Levels.Tutorial.L04rw_backwards
+msgid "$2$ is the number after the number after $0$."
+msgstr "$2$ 是 $0$ 之后再之后的数字。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "Start with `rw [two_eq_succ_one]` to begin to break `2` down into its definition."
+msgstr "从使用 `rw [two_eq_succ_one]` 开始，将 `2` 分解为它的定义。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "Can you take it from here?"
+msgstr "你能从这里接手吗？"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "Next turn `1` into `succ 0` with `rw [one_eq_succ_zero]`."
+msgstr "接下来用 `rw [one_eq_succ_zero]` 把 `1` 变成 `succ 0'。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid "Now finish the job with `rfl`."
+msgstr "现在用 `rfl` 完成证明。"
+
+#: Game.Levels.Tutorial.L03two_eq_ss0
+msgid ""
+"\n"
+"Note that you can do `rw [two_eq_succ_one, one_eq_succ_zero]`\n"
+"and then `rfl` to solve this level in two lines.\n"
+msgstr ""
+"\n"
+"请注意，您可以先使用 `rw [two_eq_succ_one, one_eq_succ_zero]`\n"
+"然后再用 `rfl` 来快速通过这关。\n"
+
+#: Game.Levels.Tutorial.L04rw_backwards
+msgid "rewriting backwards"
+msgstr "逆向重写"
+
+#: Game.Levels.Tutorial.L04rw_backwards
+msgid ""
+"\n"
+"If `h` is a proof of `X = Y` then `rw [h]` will\n"
+"turn `X`s into `Y`s. But what if we want to\n"
+"turn `Y`s into `X`s? To tell the `rw` tactic\n"
+"we want this, we use a left arrow `←`. Type\n"
+"`\\l` and then hit the space bar to get this arrow.\n"
+"\n"
+"Let's prove that $2$ is the number after the number\n"
+"after $0$ again, this time by changing `succ (succ 0)`\n"
+"into `2`.\n"
+msgstr ""
+"\n"
+"如果 `h` 是 `X = Y` 的证明，那么 `rw [h]` 将\n"
+" `X` 转换为 `Y`s。但如果我们想要\n"
+"将 `Y`s 转换为 `X`s怎么办？我们使用左箭头 `←` 来告诉`rw`策略\n"
+"我们想要这个。输入\n"
+"`\\l` 然后按空格键得到这个箭头。\n"
+"\n"
+"我们来证明一下 $2$ 就是 $0$ 之后再之后的数字。请将`succ (succ 0)`\n"
+"重写为 `2`。\n"
+
+#: Game.Levels.Tutorial.L04rw_backwards
+msgid "Try `rw [← one_eq_succ_zero]` to change `succ 0` into `1`."
+msgstr "尝试用 `rw [← one_eq_succ_zero]` 将 `succ 0` 改为 `1`。"
+
+#: Game.Levels.Tutorial.L04rw_backwards
+msgid "Can you now change the goal into `2 = 2`?"
+msgstr "你现在能将目标改为 \"2 = 2 \"吗？"
+
+#: Game.Levels.Tutorial.L04rw_backwards
+msgid "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`."
+msgstr "现在 `rw [← two_eq_succ_one]` 会把 `succ 1` 改为 `2`。"
+
+#: Game.Levels.Tutorial.L04rw_backwards
+msgid ""
+"\n"
+"Why did we not just define `succ n` to be `n + 1`? Because we have not\n"
+"even *defined* addition yet! We'll do that in the next level.\n"
+msgstr ""
+"\n"
+"为什么我们不直接将 `succ n` 定义为 `n + 1`？因为我们还没有\n"
+" *定义* 加法！我们将在下一关做到这一点。\n"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid "Adding zero"
+msgstr "加零"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid ""
+"`Add a b`, with notation `a + b`, is\n"
+"the usual sum of natural numbers. Internally it is defined\n"
+"via the following two hypotheses:\n"
+"\n"
+"* `add_zero a : a + 0 = a`\n"
+"\n"
+"* `add_succ a b : a + succ b = succ (a + b)`\n"
+"\n"
+"Other theorems about naturals, such as `zero_add a : 0 + a = a`, are proved\n"
+"by induction using these two basic theorems.\""
+msgstr ""
+"`Add a b`，符号为 `a + b`，是\n"
+"自然数之和。\n"
+"通过以下两个假设定义：\n"
+"\n"
+"* `add_zero a : a + 0 = a`\n"
+"\n"
+"* `add_succ a b : a + succ b = succ (a + b)`\n"
+"\n"
+"其他关于自然数的定理，例如 `zero_add a : 0 + a = a`，也\n"
+"通过数学归纳法使用这两个基本定义进行证明。"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid ""
+"`add_zero a` is a proof that `a + 0 = a`.\n"
+"\n"
+"## Summary\n"
+"\n"
+"`add_zero` is really a function, which\n"
+"eats a number, and returns a proof of a theorem\n"
+"about that number. For example `add_zero 37` is\n"
+"a proof that `37 + 0 = 37`.\n"
+"\n"
+"The `rw` tactic will accept `rw [add_zero]`\n"
+"and will try to figure out which number you omitted\n"
+"to input.\n"
+"\n"
+"## Details\n"
+"\n"
+"A mathematician sometimes thinks of `add_zero`\n"
+"as \"one thing\", namely a proof of $\forall n ∈ ℕ, n + 0 = n$.\n"
+"This is just another way of saying that it's a function which\n"
+"can eat any number n and will return a proof that `n + 0 = n`."
+msgstr ""
+"`add_zero a` 是 `a + 0 = a` 的证明。\n"
+"\n"
+"## 小结\n"
+"\n"
+"`add_zero` 实际上是一个函数，它接受一个数字，并返回关于那个数字的定理的证明。例如，`add_zero 37` 是 `37 + 0 = 37` 的证明。\n"
+"\n"
+"`rw` 策略会接受 `rw [add_zero]` 并尝试推断出你省略输入的数字。\n"
+"\n"
+"## 细节\n"
+"\n"
+"数学家有时将 `add_zero` 视为“一个东西”，即 $∀ n ∈ ℕ, n + 0 = n$ 的证明。这只是另一种说法，它是一个函数，可以接受任何数字 n 并返回 `n + 0 = n` 的证明。"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid ""
+"## Summary\n"
+"\n"
+"`repeat t` repeatedly applies the tactic `t`\n"
+"to the goal. You don't need to use this\n"
+"tactic, it just speeds things up sometimes.\n"
+"\n"
+"## Example\n"
+"\n"
+"`repeat rw [add_zero]` will turn the goal\n"
+"`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\n"
+"into the goal\n"
+"`a = b`."
+msgstr ""
+"## 小结\n"
+"\n"
+"`repeat t` 会重复应用策略 `t` 到目标上。你不一定要使用这个策略，它有时只是加快了速度。\n"
+"\n"
+"## 示例\n"
+"\n"
+"`repeat rw [add_zero]` 会将目标 `a + 0 + (0 + (0 + 0)) = b + 0 + 0` 转变为目标 `a = b`。"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid ""
+"\n"
+"We'd like to prove `2 + 2 = 4` but right now\n"
+"we can't even *state* it\n"
+"because we haven't yet defined addition.\n"
+"\n"
+"## Defining addition.\n"
+"\n"
+"How are we going to add $37$ to an arbitrary number $x$? Well,\n"
+"there are only two ways to make numbers in this game: $0$\n"
+"and successors. So to define `37 + x` we will need\n"
+"to know what `37 + 0` is and what `37 + succ x` is.\n"
+"Let's start with adding `0`.\n"
+"\n"
+"### Adding 0\n"
+"\n"
+"To make addition agree with our intuition, we should *define* `37 + 0`\n"
+"to be `37`. More generally, we should define `a + 0` to be `a` for\n"
+"any number `a`. The name of this proof in Lean is `add_zero a`.\n"
+"For example `add_zero 37` is a proof of `37 + 0 = 37`,\n"
+"`add_zero x` is a proof of `x + 0 = x`, and `add_zero` is a proof\n"
+"of `? + 0 = ?`.\n"
+"\n"
+"We write `add_zero x : x + 0 = x`, so `proof : statement`.\n"
+msgstr ""
+"\n"
+"我们想证明 `2 + 2 = 4` ，但现在\n"
+"我们甚至无法 *陈述* 它，\n"
+"因为我们还没有定义加法。\n"
+"\n"
+"## 定义加法。\n"
+"\n"
+"我们如何将任意数字 $x$ 加在 $37$ 上？\n"
+"在这个游戏中只有两种方法可以生成数字：$0$\n"
+"和后继数。因此，要定义 `37 + x`，我们需要\n"
+"了解 `37 + 0` 是什么以及 `37 + succ x` 是什么。\n"
+"让我们从加 `0` 开始。\n"
+"\n"
+"### 添加 0\n"
+"\n"
+"为了使加法符合我们的直觉，我们应该 *定义* `37 + 0`\n"
+"为 `37`。更一般地，对于任何数字 `a`，我们应该将 `a + 0` 定义为 `a`。\n"
+"这个证明在Lean中的名称是 `add_zero a`。\n"
+"例如 `add_zero 37` 是 `37 + 0 = 37` 的证明，\n"
+"`add_zero x` 是 `x + 0 = x` 的证明，`add_zero` 是\n"
+"`? + 0 = ?` 的证明。\n"
+"\n"
+"我们记 `add_zero x : x + 0 = x`，证明的名称在前，证明的内容在后。\n"
+
+#: Game.Levels.Tutorial.L05add_zero Game.Levels.Tutorial.L06add_zero2
+msgid "$a+(b+0)+(c+0)=a+b+c.$"
+msgstr "$a+(b+0)+(c+0)=a+b+c$ 。"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid "`rw [add_zero]` will change `b + 0` into `b`."
+msgstr "`rw [add_zero]` 会把 `b + 0` 改为 `b`。"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid "Now `rw [add_zero]` will change `c + 0` into `c`."
+msgstr "现在，`rw [add_zero]` 会把 `c + 0` 改为 `c`。"
+
+#: Game.Levels.Tutorial.L05add_zero
+msgid ""
+"Those of you interested in speedrunning the game may want to know\n"
+"that `repeat rw [add_zero]` will do both rewrites at once.\n"
+msgstr ""
+"那些对极速通关游戏感兴趣的玩家可能想知道\n"
+"`repeat rw [add_zero]` 将同时进行两项重写。\n"
+
+#: Game.Levels.Tutorial.L06add_zero2
+msgid "Precision rewriting"
+msgstr "精准重写"
+
+#: Game.Levels.Tutorial.L06add_zero2
+msgid ""
+"\n"
+"## Precision rewriting\n"
+"\n"
+"In the last level, there was `b + 0` and `c + 0`,\n"
+"and `rw [add_zero]` changed the first one it saw,\n"
+"which was `b + 0`. Let's learn how to tell Lean\n"
+"to change `c + 0` first by giving `add_zero` an\n"
+"explicit input.\n"
+msgstr ""
+"\n"
+"## 精确重写\n"
+"\n"
+"在上一个层级中，有 `b + 0` 和 `c + 0`，\n"
+"而 `rw [add_zero]` 改变了它看到的第一个加0，\n"
+"也就是 `b + 0`。让我们学习如何告诉 Lean\n"
+"通过给 `add_zero` 一个明确的输入来首先改变 `c + 0`。\n"
+
+#: Game.Levels.Tutorial.L06add_zero2
+msgid "Try `rw [add_zero c]`."
+msgstr "尝试使用 `rw [add_zero c]`。"
+
+#: Game.Levels.Tutorial.L06add_zero2
+msgid ""
+"`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.\n"
+"You can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You\n"
+"can usually stick to `rw [add_zero]` unless you need real precision."
+msgstr ""
+"`add_zero c` 是 `c + 0 = c` 的证明，所以可以用来改写目标了。\n"
+"现在你可以用 `rw [add_zero]` 或 `rw [add_zero b]` 把 `b + 0` 改成 `b`。您\n"
+"通常可以使用 `rw [add_zero]`，除非你需要准确控制改写内容。"
+
+#: Game.Levels.Tutorial.L06add_zero2
+msgid ""
+"\n"
+"Let's now learn about Peano's second axiom for addition, `add_succ`.\n"
+msgstr ""
+"\n"
+"现在让我们了解皮亚诺的第二个加法公理 `add_succ`。\n"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "add_succ"
+msgstr "add_succ"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
+msgstr "`add_succ a b` 是 `a + succ b = succ (a + b)` 的证明。"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "`succ_eq_add_one n` is the proof that `succ n = n + 1`."
+msgstr "`succ_eq_add_one n` 是 `succ n = n + 1` 的证明。"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid ""
+"\n"
+"Every number in Lean is either $0$ or a successor. We know how to add $0$,\n"
+"but we need to figure out how to add successors. Let's say we already know\n"
+"that `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n"
+"`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\n"
+"the number one bigger than `q`. More generally `x + succ d` should\n"
+"be `succ (x + d)`. Let's add this as a lemma.\n"
+"\n"
+"* `add_succ x d : x + succ d = succ (x + d)`\n"
+"\n"
+"If you ever see `... + succ ...` in your goal, `rw [add_succ]` is\n"
+"normally a good idea.\n"
+"\n"
+"Let's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\n"
+"the picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n"
+"`012` (numerals) tabs under \"Theorems\" on the right to\n"
+"see which proofs you can rewrite.\n"
+msgstr ""
+"\n"
+"Lean 中的每个数字要么是 $0$ 要么是后继数。我们已经知道如何加 $0$，\n"
+"我们还需要弄清楚如何添加后继数。假设我们已经知道\n"
+"`37 + d = q`。 `37 + succ d` 的答案应该是什么？\n"
+"`succ d` 比 `d` 大1，因此 `37 + succ d` 应该是 `succ q`，\n"
+"也就是比 `q` 大1。更一般地说，`x + succ d` 应该\n"
+"为 `succ (x + d)`。让我们将其添加为引理。\n"
+"\n"
+"* `add_succ x d : x + succ d = succ (x + d)`\n"
+"\n"
+"如果您在证明目标中看到 `... + succ ...`，那么用 `rw [add_succ]` 改写\n"
+"通常是个好主意。\n"
+"\n"
+"现在让我们证明 `succ n = n + 1`。弄清楚如何引入 `+ succ` \n"
+"，然后再 `rw [add_succ]`。在右侧“定理”下的 `+`（加法）和\n"
+" `012`（数字）选项卡里\n"
+"看看你可以用哪些证明重写目标。\n"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$."
+msgstr "对于所有自然数 $a$，我们有 $\\operatorname{succ}(a) = a+1$ 。"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "Start by unravelling the `1`."
+msgstr "从解开 \"1 \"开始。"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "`rw [one_eq_succ_zero]` will do this."
+msgstr "`rw [one_eq_succ_zero]` 能这样做。"
+
+#: Game.Levels.Tutorial.L07add_succ Game.Levels.Tutorial.L08twoaddtwo
+msgid "Now you can `rw [add_succ]`"
+msgstr "现在，您可以 `rw [add_succ]`"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "And now `rw [add_zero]`"
+msgstr "现在使用`rw [add_zero]`"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "And finally `rfl`."
+msgstr "最后是 \"rfl`\"。"
+
+#: Game.Levels.Tutorial.L07add_succ
+msgid "[dramatic music]. Now are you ready to face the first boss of the game?"
+msgstr "[背景音乐] 现在你准备好面对游戏的第一个boss了吗？"
+
+#: Game.Levels.Tutorial.L08twoaddtwo
+msgid "2+2=4"
+msgstr "2+2=4"
+
+#: Game.Levels.Tutorial.L08twoaddtwo
+msgid ""
+" Good luck!\n"
+"\n"
+"  One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.\n"
+"  If you only want to change one of them, say the 3rd one, then use\n"
+"  `nth_rewrite 3 [h]`.\n"
+msgstr ""
+"祝你好运！\n"
+"\n"
+"最后一个提示。如果 `h : X = Y`，那么 `rw [h]` 会将 *所有* 的 `X` 替换为 `Y`。\n"
+"如果你只想替换其中一个，比如第 3 个，那么使用\n"
+"`nth_rewrite 3 [h]`。\n"
+
+#: Game.Levels.Tutorial.L08twoaddtwo
+msgid "$2+2=4$."
+msgstr "$2+2=4$。"
+
+#: Game.Levels.Tutorial.L08twoaddtwo
+msgid "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`."
+msgstr "我认为 `nth_rewrite 2 [two_eq_succ_one]` 比 `rw [two_eq_succ_one]` 更快。"
+
+#: Game.Levels.Tutorial.L08twoaddtwo
+msgid ""
+"\n"
+"Here is an example proof of 2+2=4 showing off various techniques.\n"
+"\n"
+"```lean\n"
+"nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.\n"
+"rw [add_succ]\n"
+"rw [one_eq_succ_zero]\n"
+"rw [add_succ, add_zero] -- two rewrites at once\n"
+"rw [← three_eq_succ_two] -- change `succ 2` to `3`\n"
+"rw [← four_eq_succ_three]\n"
+"rfl\n"
+"```\n"
+"\n"
+"Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\n"
+"on the `</>` button in the top right. You can now see your proof\n"
+"written as several lines of code. Move your cursor between lines to see\n"
+"the goal state at any point. Now cut and paste your code elsewhere if you\n"
+"want to save it, and paste the above proof in instead. Move your cursor\n"
+"around to investigate. When you've finished, click the `>_` button in the top right to\n"
+"move back into \"Typewriter mode\".\n"
+"\n"
+"You have finished tutorial world!\n"
+"Click \"Leave World\" to go back to the\n"
+"overworld, and select Addition World, where you will learn\n"
+"about the `induction` tactic.\n"
+msgstr ""
+"\n"
+"下面是一个证明 2+2=4 的例子，展示了各种技巧。\n"
+"\n"
+"```lean\n"
+"nth_rewrite 2 [two_eq_succ_one] -- 只将第二个 `2 ` 改为 `succ 1` 。\n"
+"rw [add_succ］\n"
+"rw [one_eq_succ_zero]\n"
+"rw [add_succ, add_zero] -- 一次改写两个内容\n"
+"rw [← three_eq_succ_two] -- 将 `succ 2` 改为 `3`\n"
+"rw [← four_eq_succ_three] 。\n"
+"rfl\n"
+"```\n"
+"\n"
+"可选附加功能：你可以自己运行这个证明。点击右上角的\n"
+"右上角的 `</>` 按钮，将游戏切换到 \"编辑器模式\"。现在你可以看到你的证明\n"
+"被写成了几行代码。在各行代码之间移动光标，即可查看\n"
+"目标状态。现在，如果想保存代码，你就要将代码剪切并粘贴到其他地方\n"
+"，请将上述证明粘贴进去。移动光标\n"
+"进行研究。完成后，点击右上角的 `>_` 按钮，回到 \"打字机模式\"。\n"
+"回到 \"打字机模式\"。\n"
+"\n"
+"您已经完成了 \"教程世界\"！\n"
+"点击 \"离开世界 \"回到世界选择界面\n"
+"选择 \"加法世界\"，在这里您将学习\n"
+"`induction ` 策略。\n"
+
+#: Game.Levels.Tutorial
+msgid "Tutorial World"
+msgstr "教程世界"
+
+#: Game.Levels.Tutorial
+msgid ""
+"Welcome to tutorial world! In this world we learn the basics\n"
+"of proving theorems. The boss level of this world\n"
+"is the theorem `2 + 2 = 4`.\n"
+"\n"
+"You prove theorems by solving puzzles using tools called *tactics*.\n"
+"The aim is to prove the theorem by applying tactics\n"
+"in the right order.\n"
+"\n"
+"Let's learn some basic tactics. Click on \"Start\" below\n"
+"to begin your quest.\n"
+msgstr ""
+"欢迎来到教程世界！在这个世界中，我们学习证明定理的基础知识。这个世界的最终挑战是证明定理 `2 + 2 = 4`。\n"
+"\n"
+"你可以通过使用被称为*策略*的工具来解决谜题，从而证明定理。目标是通过以正确的顺序应用策略来证明定理。\n"
+"\n"
+"让我们学习一些基础策略。点击下方的“开始”按钮，开始你的探索。\n"
+
+#: Game.Levels.Addition.L01zero_add
+msgid "zero_add"
+msgstr "zero_add"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"\n"
+"In this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n"
+"\n"
+"Wait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\n"
+"This is `zero_add`, which is different.\n"
+"\n"
+"The difficulty with proving `0 + n = n` is that we do not have a *formula* for\n"
+"`0 + n` in general, we can only use `add_zero` and `add_succ` once\n"
+"we know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n"
+"\n"
+"The base case will require us to prove `0 + 0 = 0`, and the inductive step\n"
+"will ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because\n"
+"`0` and successor are the only way to make numbers, this will cover all the cases.\n"
+"\n"
+"See if you can do your first induction proof in Lean.\n"
+"\n"
+"(By the way, if you are still in the \"Editor mode\" from the last world, you can swap\n"
+"back to \"Typewriter mode\" by clicking the `>_` button in the top right.)\n"
+msgstr ""
+"\n"
+"在这个关卡中，我们将证明 $0+n=n$，其中 $n$ 是一个秘密的自然数。\n"
+"\n"
+"等等，我们不是已经知道这个了吗？不！我们知道的是 $n+0=n$，但那是 `add_zero`。这里的 `zero_add` 是不同的。\n"
+"\n"
+"证明 `0 + n = n` 的难点在于我们没有一个一般的*公式*来表示 `0 + n`，我们只能在知道 `n` 是 `0` 还是后继数后，使用 `add_zero` 和 `add_succ`。`induction` 策略会分解成这两种情况。\n"
+"\n"
+"基础情况将要求我们证明 `0 + 0 = 0`，归纳步骤将要求我们证明如果 `0 + d = d` 那么 `0 + succ d = succ d`。因为 `0` 和后继数是构造数字的唯一方式，这将涵盖所有情况。\n"
+"\n"
+"看看你是否能在 Lean 中完成你的第一个归纳证明。\n"
+"\n"
+"(顺便说一句，如果你还在上一个世界的 \"编辑器模式 \"下，你可以通过点击 \"编辑器模式 \"下的\n"
+"点击右上角的 `>_` 按钮换回 \"模式\"）。\n"
+"\n"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"`zero_add x` is the proof of `0 + x = x`.\n"
+"\n"
+"`zero_add` is a `simp` lemma, because replacing `0 + x` by `x`\n"
+"is almost always what you want to do if you're simplifying an expression."
+msgstr ""
+"`zero_add x` 是 `0 + x = x` 的证明。\n"
+"\n"
+"`zero_add` 是一个有 `simp` 标记的引理，因为如果你正在简化一个表达式，几乎总是想要将 `0 + x` 替换为 `x`。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid "For all natural numbers $n$, we have $0 + n = n$."
+msgstr "对于所有自然数 $n$，我们有 $0 + n = n$。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"You can start a proof by induction on `n` by typing:\n"
+"`induction n with d hd`."
+msgstr ""
+"你可以通过输入以下内容来开始对 `n` 进行归纳证明：\n"
+"`induction n with d hd`。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"Now you have two goals. Once you proved the first, you will jump to the second one.\n"
+"This first goal is the base case $n = 0$.\n"
+"\n"
+"Recall that you can rewrite the proof of any lemma which is visible\n"
+"in your inventory, or of any assumption displayed above the goal,\n"
+"as long as it is of the form `X = Y`."
+msgstr ""
+"现在你有两个目标。一旦你证明了第一个，你会自动跳到第二个。\n"
+"第一个目标是基础情形 $n = 0$。\n"
+"\n"
+"回想一下，你可以使用任何在你的清单中可见的引理的证明，或者任何显示在目标上方的假设\n"
+"（只要它是形如 `X = Y` 的形式）来重写目标。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid "try rewriting `add_zero`."
+msgstr "尝试重写 `add_zero`。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"Now for to the second goal. Here you have the induction hypothesis\n"
+"`«{hd}» : 0 + «{d}» = «{d}»`, and you need to prove that `0 + succ «{d}» = succ «{d}»`."
+msgstr ""
+"现在来到第二个目标。这里你有归纳假设\n"
+"`«{hd}» : 0 + «{d}» = «{d}»`，你需要证明 `0 + succ «{d}» = succ «{d}»`。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid "Use `add_succ`."
+msgstr "使用 `add_succ`。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"At this point you see the term `0 + «{d}»`, so you can use the\n"
+"induction hypothesis with `rw [«{hd}»]`."
+msgstr "在这一点上，你看到了项 `0 + «{d}»`，所以你可以通过 `rw [«{hd}»]` 来使用归纳假设。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"## Summary\n"
+"\n"
+"If `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\n"
+"attempts to prove the goal by induction on `n`, with the inductive\n"
+"variable in the successor case being `d`, and the inductive hypothesis being `hd`.\n"
+"\n"
+"### Example:\n"
+"If the goal is\n"
+"```\n"
+"0 + n = n\n"
+"```\n"
+"\n"
+"then\n"
+"\n"
+"`induction n with d hd`\n"
+"\n"
+"will turn it into two goals. The first is `0 + 0 = 0`;\n"
+"the second has an assumption `hd : 0 + d = d` and goal\n"
+"`0 + succ d = succ d`.\n"
+"\n"
+"Note that you must prove the first\n"
+"goal before you can access the second one."
+msgstr ""
+"## 小结\n"
+"\n"
+"如果 `n : ℕ` 是一个对象，并且目标提到了 `n`，那么 `induction n with d hd`\n"
+"尝试通过对 `n` 进行归纳来证明目标，其中后继数情况下的归纳变量是 `d`，归纳假设是 `hd`。\n"
+"\n"
+"### 例子:\n"
+"如果目标是\n"
+"```\n"
+"0 + n = n\n"
+"```\n"
+"\n"
+"那么\n"
+"\n"
+"`induction n with d hd`\n"
+"\n"
+"将把它变成两个目标。第一个是 `0 + 0 = 0`；\n"
+"第二个有一个假设 `hd : 0 + d = d` 和目标\n"
+"`0 + succ d = succ d` 。\n"
+"\n"
+"注意你必须先证明第一个然后才能证第二个。"
+
+#: Game.Levels.Addition.L01zero_add
+msgid ""
+"\n"
+"  This lemma would have been easy if we had known that `x + y = y + x`. That theorem\n"
+"  is called `add_comm` and it is *true*, but unfortunately its proof *uses* both\n"
+"  `add_zero` and `zero_add`!\n"
+"\n"
+"  Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`.\n"
+msgstr ""
+"\n"
+"如果我们知道 `x + y = y + x` ，那么证明这个引理就会很容易。那个定理\n"
+"  被称为 `add_comm`  并且它是 *成立的* ，但不幸的是它的证明 *用到了* \n"
+"  `add_zero` 和 `zero_add`！\n"
+"\n"
+"  让我们继续我们证明 `add_comm`，即 `x + y = y + x` 的旅程。\n"
+
+#: Game.Levels.Addition.L02succ_add
+msgid "succ_add"
+msgstr "succ_add"
+
+#: Game.Levels.Addition.L02succ_add
+msgid ""
+"\n"
+"Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add a b`\n"
+"is the proof that `(succ a) + b = succ (a + b)` for `a` and `b` numbers.\n"
+"This result is what's standing in the way of `x + y = y + x`. Again\n"
+"we have the problem that we are adding `b` to things, so we need\n"
+"to use induction to split into the cases where `b = 0` and `b` is a successor.\n"
+msgstr ""
+"\n"
+"哦不！在前往 `add_comm` 的路上，一个野生的 `succ_add` 出现了。\n"
+"`succ_add a b` 是 `(succ a) + b = succ (a + b)` 的证明，对于数字 `a` 和 `b`。\n"
+"这个结果是证明 `x + y = y + x` 的中间步骤。这里我们再次遇到了向事物中加入 `b` 的问题，\n"
+"所以我们需要使用归纳法来分解成 `b = 0` 和 `b` 是后继数的情况。\n"
+
+#: Game.Levels.Addition.L02succ_add
+msgid "`succ_add a b` is a proof that `succ a + b = succ (a + b)`."
+msgstr "`succ_add a b` 是 `succ a + b = succ (a + b)` 的证明。"
+
+#: Game.Levels.Addition.L02succ_add
+msgid ""
+"For all natural numbers $a, b$, we have\n"
+"$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$."
+msgstr ""
+"对于所有自然数 $a, b$，我们有\n"
+"$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$。"
+
+#: Game.Levels.Addition.L02succ_add
+msgid ""
+"You might want to think about whether induction\n"
+"on `a` or `b` is the best idea."
+msgstr "你可能想考虑一下，对 `a` 还是 `b` 进行归纳证明才是最好的主意。"
+
+#: Game.Levels.Addition.L02succ_add
+msgid ""
+"Induction on `a` will not work here. You are still stuck with an `+ b`.\n"
+"I suggest you delete this line and try a different approach."
+msgstr ""
+"对 `a` 的归纳在这里不起作用。你仍然卡在 `+ b` 上。\n"
+"我建议你删除这一行，换一种方法。"
+
+#: Game.Levels.Addition.L02succ_add
+msgid ""
+"Note that `succ a + «{d}»` means `(succ a) + «{d}»`. Put your cursor\n"
+"on any `succ` in the goal or assumptions to see what exactly it's eating."
+msgstr "请注意，`succ a + «{d}»` 的意思是 `(succ a) + «{d}»`。将你的光标放在目标或假设中的任何 `succ` 上，以查看它确切的含义。"
+
+#: Game.Levels.Addition.L02succ_add
+msgid ""
+"\n"
+"Well done! You now have enough tools to tackle the main boss of this level.\n"
+msgstr ""
+"\n"
+"做得好！现在你有足够的工具来对付这个关卡的大Boss了。\n"
+
+#: Game.Levels.Addition.L03add_comm
+msgid "add_comm (level boss)"
+msgstr "add_comm（关卡Boss）"
+
+#: Game.Levels.Addition.L03add_comm
+msgid ""
+"\n"
+"[boss battle music]\n"
+"\n"
+"Look in your inventory to see the proofs you have available.\n"
+"These should be enough.\n"
+msgstr ""
+"\n"
+"【Boss战音乐】\n"
+"\n"
+"查看您的库存以查看您拥有的可用定理。\n"
+"这些应该足够了。\n"
+
+#: Game.Levels.Addition.L03add_comm
+msgid "`add_comm x y` is a proof of `x + y = y + x`."
+msgstr "`add_comm x y` 是 `x + y = y + x` 的证明。"
+
+#: Game.Levels.Addition.L03add_comm
+msgid ""
+"On the set of natural numbers, addition is commutative.\n"
+"In other words, if `a` and `b` are arbitrary natural numbers, then\n"
+"$a + b = b + a$."
+msgstr ""
+"在自然数集上，加法是可交换的。\n"
+"换句话说，如果 `a` 和 `b` 是任意自然数，那么\n"
+"$a + b = b + a$。"
+
+#: Game.Levels.Addition.L03add_comm
+msgid "Induction on `a` or `b` -- it's all the same in this one."
+msgstr "对 `a` 或 `b` 进行归纳证明 —— 它们都是相同的。"
+
+#: Game.Levels.Addition.L04add_assoc
+msgid "add_assoc (associativity of addition)"
+msgstr "add_assoc（加法结合律）"
+
+#: Game.Levels.Addition.L04add_assoc
+msgid ""
+"\n"
+"  We've been adding up two numbers; in this level we will add up three.\n"
+"\n"
+"  What does $x+y+z$ *mean*? It could either mean $(x+y)+z$, or it\n"
+"  could mean $x+(y+z)$. In Lean, $x+y+z$ means $(x+y)+z$.\n"
+"\n"
+"  But why do we care which one it means; $(x+y)+z$ and $x+(y+z)$ are *equal*!\n"
+"\n"
+"  That's true, but we didn't prove it yet. Let's prove it now by induction.\n"
+msgstr ""
+"\n"
+"我们已经学会了将两个数相加；在这个层级中，我们将学习如何将三个数相加。\n"
+"\n"
+"$x+y+z$ *意味着*什么？它可以意味着 $(x+y)+z$，也可以意味着 $x+(y+z)$。在 Lean 中，$x+y+z$ 表示 $(x+y)+z$。\n"
+"\n"
+"但我们为什么要在意它意味着哪一个；$(x+y)+z$ 和 $x+(y+z)$ 是*相等的*！\n"
+"\n"
+"确实如此，但我们还没有证明它。现在让我们通过归纳来证明它。\n"
+
+#: Game.Levels.Addition.L04add_assoc
+msgid ""
+"`add_assoc a b c` is a proof\n"
+"that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\n"
+"as `a + b + c`, because the notation for addition is defined to be left\n"
+"associative."
+msgstr ""
+"`add_assoc a b c` 是一个 `(a + b) + c = a + (b + c)` 的证明。\n"
+"请注意，在 Lean `(a + b) + c` 中显示\n"
+"为 `a + b + c`，因为加法符号被定义为左\n"
+"结合的。"
+
+#: Game.Levels.Addition.L04add_assoc
+msgid ""
+"On the set of natural numbers, addition is associative.\n"
+"In other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n"
+"$ (a + b) + c = a + (b + c). $"
+msgstr ""
+"在自然数集上，加法服从结合律。\n"
+"换句话说，如果 $a, b$ 和 $c$ 是任意自然数，我们有\n"
+"$ (a + b) + c = a + (b + c)$ 。"
+
+#: Game.Levels.Addition.L04add_assoc
+msgid ""
+"Remember that when Lean writes `a + b + c`, it means `(a + b) + c`.\n"
+"If you are not sure where the brackets are in an expression, just hover\n"
+"your cursor over it and look at what gets highlighted. For example,\n"
+"hover over both `+` symbols on the left hand side of the goal and\n"
+"you'll see where the invisible brackets are."
+msgstr ""
+"记住，当 Lean 写作 `a + b + c` 时，它的意思是 `(a + b) + c`。\n"
+"如果你不确定表达式中的括号在哪里，只需将光标悬停在它上面，\n"
+"看看什么被高亮显示。例如，将光标悬停在目标左侧的两个 `+` 符号上，\n"
+"你就会看到看不见的括号在哪里。"
+
+#: Game.Levels.Addition.L04add_assoc
+msgid ""
+"\n"
+"A passing mathematician congratulates you on proving that naturals\n"
+"are an additive commutative monoid.\n"
+"\n"
+"Let's practice using `add_assoc` and `add_comm` in one more level,\n"
+"before we leave addition world.\n"
+msgstr ""
+"\n"
+"一个路过的数学家祝贺你证明了自然数是一个加法交换幺半群。\n"
+"\n"
+"在我们离开加法世界之前，让我们在另一关里练习使用 `add_assoc` 和 `add_comm`。\n"
+
+#: Game.Levels.Addition.L05add_right_comm
+msgid "add_right_comm"
+msgstr "add_right_comm"
+
+#: Game.Levels.Addition.L05add_right_comm
+msgid ""
+"\n"
+"`add_comm b c` is a proof that `b + c = c + b`. But if your goal\n"
+"is `a + b + c = a + c + b` then `rw [add_comm b c]` will not\n"
+"work! Because the goal means `(a + b) + c = (a + c) + b` so there\n"
+"is no `b + c` term *directly* in the goal.\n"
+"\n"
+"Use associativity and commutativity to prove `add_right_comm`.\n"
+"You don't need induction. `add_assoc` moves brackets around,\n"
+"and `add_comm` moves variables around.\n"
+"\n"
+"Remember that you can do more targetted rewrites by\n"
+"adding explicit variables as inputs to theorems. For example `rw [add_comm b]`\n"
+"will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\n"
+"will only do rewrites of the form `b + c = c + b`.\n"
+msgstr ""
+"\n"
+"`add_comm b c` 是一个 `b + c = c + b` 的证明。但如果您的目标是 `a + b + c = a + c + b`，那么 `rw [add_comm b c]` 将不起作用！因为目标是 `(a + b) + c = (a + c) + b`，所以目标中*直接*没有 `b + c` 项。\n"
+"\n"
+"使用结合律和交换律来证明 `add_right_comm`。您不需要使用归纳法。`add_assoc` 移动括号，`add_comm` 移动变量。\n"
+"\n"
+"请记住，您可以通过将显式变量添加为定理的输入来进行更有针对性的重写。\n"
+"例如，`rw [add_comm b]` 只会重写形如 `b + ? = ? + b` 的形式，而 `rw [add_comm b c]` 只会重写形如 `b + c = c + b` 的形式。\n"
+
+#: Game.Levels.Addition.L05add_right_comm
+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`."
+msgstr ""
+"`add_right_comm a b c` 是 `(a + b) + c = (a + c) + b` 的证明。\n"
+"\n"
+"在 Lean 中，`a + b + c` 意味着 `(a + b) + c`，所以这个结果被显示为 `a + b + c = a + c + b`。"
+
+#: Game.Levels.Addition.L05add_right_comm
+msgid ""
+"If $a, b$ and $c$ are arbitrary natural numbers, we have\n"
+"$(a + b) + c = (a + c) + b$."
+msgstr ""
+"如果 $a, b$ 和 $c$ 是任意自然数，我们有\n"
+"$(a + b) + c = (a + c) + b$。"
+
+#: Game.Levels.Addition.L05add_right_comm
+msgid ""
+"\n"
+"You've now seen all the tactics you need to beat the final boss of the game.\n"
+"You can begin the journey towards this boss by entering Multiplication World.\n"
+"\n"
+"Or you can go off the beaten track and learn some new tactics in Implication\n"
+"World. These tactics let you prove more facts about addition, such as\n"
+"how to deduce `a = 0` from `x + a = x`.\n"
+"\n"
+"Click \"Leave World\" and make your choice.\n"
+msgstr ""
+"\n"
+"你现在已经掌握了击败游戏最终 BOSS 所需的所有策略。\n"
+"你可以进入乘法世界，开始征服 BOSS 的冒险之旅。\n"
+"\n"
+"或者，你可以离开常规路线，在蕴涵世界中学习一些新的策略。\n"
+"这些策略可以让你证明更多关于加法的事实，例如从 `x + a = x` 推导 `a = 0`。\n"
+"\n"
+"点击“离开世界”，做出你的选择吧。\n"
+
+#: Game.Levels.Addition
+msgid "Addition World"
+msgstr "加法世界"
+
+#: Game.Levels.Addition
+msgid ""
+"\n"
+"Welcome to Addition World! In this world we'll learn the `induction` tactic.\n"
+"This will enable us to defeat the boss level of this world, namely `x + y = y + x`.\n"
+"\n"
+"The tactics `rw`, `rfl` and `induction` are the only tactics you'll need to\n"
+"beat all the levels in Addition World, Multiplication World, and Power World.\n"
+"Power World contains the final boss of the game.\n"
+"\n"
+"There are plenty more tactics in this game, but you'll only need to know them if you\n"
+"want to explore the game further (for example if you decide to 100%\n"
+"the game).\n"
+msgstr ""
+"\n"
+"欢迎来到加法世界！在这个世界中，我们将学习 `induction` 策略。这将使我们能够击败这个世界的老大，即 `x + y = y + x`。\n"
+"\n"
+"`rw`、`rfl` 和 `induction` 是你需要掌握的唯一策略，才能通过加法世界、乘法世界和幂世界的所有关卡。幂世界包含游戏的最终boss。\n"
+"\n"
+"这个游戏中还有更多的策略，但如果你想进一步探索游戏（例如如果你决定完成游戏的100%），你只需要了解它们。\n"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid "mul_one"
+msgstr "mul_one"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid ""
+"\n"
+"\n"
+"See the new \"*\" tab in your lemmas, containing `mul_zero` and `mul_succ`.\n"
+"Right now these are the only facts we know about multiplication.\n"
+"Let's prove nine more.\n"
+"\n"
+"Let's start with a warm-up: no induction needed for this one,\n"
+"because we know `1` is a successor.\n"
+msgstr ""
+"\n"
+"查看引理区中的新“*”标签，包含 `mul_zero` 和 `mul_succ`。\n"
+"目前这些是我们唯一知道的关于乘法的事实。\n"
+"让我们再证明九个。\n"
+"\n"
+"让我们从一个热身开始：这个不需要归纳，\n"
+"因为我们知道 `1` 是一个后继数。\n"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid ""
+"`Mul a b`, with notation `a * b`, is the usual\n"
+"  product of natural numbers. Internally it is\n"
+"  via two axioms:\n"
+"\n"
+"  * `mul_zero a : a * 0 = 0`\n"
+"\n"
+"  * `mul_succ a b : a * succ b = a * b + a`\n"
+"\n"
+"Other theorems about naturals, such as `zero_mul`,\n"
+"are proved by induction from these two basic theorems."
+msgstr ""
+"`Mul a b`，其符号表示为 `a * b`，是自然数的常规乘积。它是通过两条规则定义的：\n"
+"\n"
+"* `mul_zero a : a * 0 = 0`\n"
+"\n"
+"* `mul_succ a b : a * succ b = a * b + a`\n"
+"\n"
+"关于自然数的其他定理，比如 `zero_mul`，都是通过从这两个基本定理进行归纳证明得到的。"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid "`mul_zero m` is the proof that `m * 0 = 0`."
+msgstr "`mul_zero m` 是 `m * 0 = 0` 的证明。"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid "`mul_succ a b` is the proof that `a * succ b = a * b + a`."
+msgstr "`mul_succ a b` 是 `a * succ b = a * b + a` 的证明。"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid "`mul_one m` is the proof that `m * 1 = m`."
+msgstr "`mul_one m` 是 `m * 1 = m` 的证明。"
+
+#: Game.Levels.Multiplication.L01mul_one
+msgid "For any natural number $m$, we have $ m \times 1 = m$."
+msgstr "对于任何自然数 $m$，我们有 $ m \times 1 = m$。"
+
+#: Game.Levels.Multiplication.L02zero_mul
+msgid "zero_mul"
+msgstr "zero_mul"
+
+#: Game.Levels.Multiplication.L02zero_mul
+msgid ""
+"\n"
+"Our first challenge is `mul_comm x y : x * y = y * x`,\n"
+"and we want to prove it by induction. The zero\n"
+"case will need `mul_zero` (which we have)\n"
+"and `zero_mul` (which we don't), so let's\n"
+"start with this.\n"
+msgstr ""
+"\n"
+"我们的第一个挑战是`mul_comm x y : x * y = y * x`，\n"
+"我们想通过归纳法来证明这一点。在证明0的目标下我们需要 `mul_zero` （我们有）\n"
+"和 `zero_mul` （我们没有），所以让我们\n"
+"从这个开始。\n"
+
+#: Game.Levels.Multiplication.L02zero_mul
+msgid ""
+"`zero_mul x` is the proof that `0 * x = 0`.\n"
+"\n"
+"Note: `zero_mul` is a `simp` lemma."
+msgstr ""
+"`zero_mul x` 是 `0 * x = 0` 的证明。\n"
+"\n"
+"注意：`zero_mul` 是一个 `simp` 引理。"
+
+#: Game.Levels.Multiplication.L02zero_mul
+msgid "For all natural numbers $m$, we have $ 0 \times m = 0$."
+msgstr "对于所有自然数 $m$，我们有 $ 0 \times m = 0$。"
+
+#: Game.Levels.Multiplication.L03succ_mul
+msgid "succ_mul"
+msgstr "succ_mul"
+
+#: Game.Levels.Multiplication.L03succ_mul
+msgid ""
+"\n"
+"Similarly we have `mul_succ`\n"
+"but we're going to need `succ_mul` (guess what it says -- maybe you\n"
+"are getting the hang of Lean's naming conventions).\n"
+"\n"
+"The last level from addition world might help you in this level.\n"
+"If you can't remember what it is, you can go back to the\n"
+"home screen by clicking the house icon and then taking a look.\n"
+"You won't lose any progress.\n"
+msgstr ""
+"\n"
+"同样，我们有 `mul_succ`，\n"
+"但我们需要 `succ_mul`（猜猜它是什么意思 —— 也许你已经掌握了 Lean 的命名范式）。\n"
+"\n"
+"加法世界中的最后一关会在这个关卡中帮助你。\n"
+"如果你忘记了它是什么，你可以通过点击房屋图标回到主界面，然后看一看。\n"
+"你不会失去任何进展。\n"
+
+#: Game.Levels.Multiplication.L03succ_mul
+msgid ""
+"`succ_mul a b` is the proof that `succ a * b = a * b + b`.\n"
+"\n"
+"It could be deduced from `mul_succ` and `mul_comm`, however this argument\n"
+"would be circular because the proof of `mul_comm` uses `mul_succ`."
+msgstr ""
+"`succ_mul a b` 是 `succ a * b = a * b + b` 的证明。\n"
+"\n"
+"可以从 `mul_succ` 和 `mul_comm` 推导出来，但是这个是循环论证，\n"
+"因为 `mul_comm` 的证明使用了 `mul_succ`。"
+
+#: Game.Levels.Multiplication.L03succ_mul
+msgid ""
+"For all natural numbers $a$ and $b$, we have\n"
+"$(\\operatorname{succ}\\ a) \times b = a\times b + b$."
+msgstr ""
+"对于所有自然数 $a$ 和 $b$，我们有\n"
+"$(\\operatorname{succ}\\ a) \times b = a\times b + b$。"
+
+#: Game.Levels.Multiplication.L04mul_comm
+msgid "mul_comm"
+msgstr "mul_comm"
+
+#: Game.Levels.Multiplication.L04mul_comm
+msgid ""
+"\n"
+"The first sub-boss of Multiplication World is `mul_comm x y : x * y = y * x`.\n"
+"\n"
+"When you've proved this theorem we will have \"spare\" proofs\n"
+"such as `zero_mul`, which is now easily deducible from `mul_zero`.\n"
+"But we'll keep hold of these proofs anyway, because it's convenient\n"
+"to have exactly the right tool for a job.\n"
+msgstr ""
+"\n"
+"乘法世界的第一个小 Boss 是 `mul_comm x y : x * y = y * x`。\n"
+"\n"
+"当你证明了这个定理后，我们将有一些“多余”的证明\n"
+"例如 `zero_mul`，它现在可以轻松地从 `mul_zero` 中推导出来。\n"
+"但无论如何我们都会保留这些证明，因为\n"
+"拥有适合工作的工具会很方便。\n"
+
+#: Game.Levels.Multiplication.L04mul_comm
+msgid ""
+"`mul_comm` is the proof that multiplication is commutative. More precisely,\n"
+"`mul_comm a b` is the proof that `a * b = b * a`."
+msgstr ""
+"`mul_comm` 是乘法可交换的证明。更确切地说，\n"
+"`mul_comm a b` 是 `a * b = b * a` 的证明。"
+
+#: Game.Levels.Multiplication.L04mul_comm
+msgid "Multiplication is commutative."
+msgstr "乘法是可交换的。"
+
+#: Game.Levels.Multiplication.L05one_mul
+msgid "one_mul"
+msgstr "one_mul"
+
+#: Game.Levels.Multiplication.L05one_mul
+msgid ""
+"\n"
+"You can prove $1\times m=m$ in at least three ways.\n"
+"Either by induction, or by using `succ_mul`, or\n"
+"by using commutativity. Which do you think is quickest?\n"
+msgstr ""
+"\n"
+"您可以至少通过三种方式证明 $1\times m=m$。\n"
+"通过归纳法，或使用 `succ_mul`，或\n"
+"通过使用交换律。你认为哪个最快？\n"
+
+#: Game.Levels.Multiplication.L05one_mul
+msgid "`one_mul m` is the proof `1 * m = m`."
+msgstr "`one_mul m` 是证明 `1 * m = m`。"
+
+#: Game.Levels.Multiplication.L05one_mul
+msgid "For any natural number $m$, we have $ 1 \times m = m$."
+msgstr "对于任何自然数 $m$，我们有 $ 1 \times m = m$。"
+
+#: Game.Levels.Multiplication.L05one_mul
+msgid ""
+"\n"
+"Here's my solution:\n"
+"```\n"
+"rw [mul_comm, mul_one]\n"
+"rfl\n"
+"```\n"
+msgstr ""
+"\n"
+"这是我的解法：\n"
+"```\n"
+"rw [mul_comm, mul_one]\n"
+"rfl\n"
+"```\n"
+
+#: Game.Levels.Multiplication.L06two_mul
+msgid "two_mul"
+msgstr "two_mul"
+
+#: Game.Levels.Multiplication.L06two_mul
+msgid ""
+"\n"
+"This level is more important than you think; it plays\n"
+"a useful role when battling a big boss later on.\n"
+msgstr ""
+"\n"
+"这个关卡比你想象的更重要；在之后与一个大boss战斗时，它将帮助你。\n"
+
+#: Game.Levels.Multiplication.L06two_mul
+msgid "`two_mul m` is the proof that `2 * m = m + m`."
+msgstr "`two_mul m` 是 `2 * m = m + m` 的证明。"
+
+#: Game.Levels.Multiplication.L06two_mul
+msgid "For any natural number $m$, we have $ 2 \times m = m+m$."
+msgstr "对于任何自然数 $m$，我们有 $ 2 \times m = m+m$。"
+
+#: Game.Levels.Multiplication.L06two_mul
+msgid ""
+"\n"
+"Here's my solution:\n"
+"```\n"
+"rw [two_eq_succ_one, succ_mul, one_mul]\n"
+"rfl\n"
+"```\n"
+msgstr ""
+"\n"
+"这是我的解法：\n"
+"```\n"
+"rw [two_eq_succ_one, succ_mul, one_mul]\n"
+"rfl\n"
+"```\n"
+
+#: Game.Levels.Multiplication.L07mul_add
+msgid "mul_add"
+msgstr "mul_add"
+
+#: Game.Levels.Multiplication.L07mul_add
+msgid ""
+"\n"
+"Our next goal is \"left and right distributivity\",\n"
+"meaning $a(b+c)=ab+ac$ and $(b+c)a=ba+ca$. Rather than\n"
+"these slightly pompous names, the name of the proofs\n"
+"of the proof in Lean are descriptive. Let's start with\n"
+"`mul_add a b c`, the proof of `a * (b + c) = a * b + a * c`.\n"
+"Note that the left hand side contains a multiplication\n"
+"and then an addition.\n"
+msgstr ""
+"\n"
+"我们的下一个目标是“左右分配律”，\n"
+"意思是 $a(b+c)=ab+ac$ 和 $(b+c)a=ba+ca$。\n"
+"这样的名字略显浮夸。在Lean中的证明名字一般不是这样的，大都是描述性的。\n"
+"让我们从\n"
+"`mul_add a b c`，也就是 `a * (b + c) = a * b + a * c` 开始证明。\n"
+"请注意，左侧包含乘法\n"
+"然后是加法。\n"
+
+#: Game.Levels.Multiplication.L07mul_add
+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`."
+msgstr ""
+"乘法在左侧对加法具有分配性。\n"
+"\n"
+"`mul_add a b c` 是 `a * (b + c) = a * b + a * c` 的证明。"
+
+#: Game.Levels.Multiplication.L07mul_add
+msgid ""
+"Multiplication is distributive over addition on the left.\n"
+"In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
+"$a(b + c) = ab + ac$."
+msgstr ""
+"乘法对左边的加法具有分配性。\n"
+"换句话说，对于所有自然数 $a$、$b$ 和 $c$，我们有\n"
+"$a(b + c) = ab + ac$。"
+
+#: Game.Levels.Multiplication.L07mul_add
+msgid ""
+"You can do induction on any of the three variables. Some choices\n"
+"are harder to push through than others. Can you do the inductive step in\n"
+"5 rewrites only?"
+msgstr "你可以对任何三个变量中的任何一个进行归纳。有些选择比其他选择更难以推进。你能仅用5次改写完成归纳步骤吗？"
+
+#: Game.Levels.Multiplication.L07mul_add
+msgid ""
+"Induction on `a` is the most troublesome, then `b`,\n"
+"and `c` is the easiest."
+msgstr ""
+"对 `a` 的归纳最麻烦，然后是 `b`、\n"
+"而 `c` 是最简单的。"
+
+#: Game.Levels.Multiplication.L07mul_add
+msgid ""
+"\n"
+"Here's my solution:\n"
+"```\n"
+"induction c with d hd\n"
+"rw [add_zero, mul_zero, add_zero]\n"
+"rfl\n"
+"rw [add_succ, mul_succ, hd, mul_succ, add_assoc]\n"
+"rfl\n"
+"```\n"
+"\n"
+"Inducting on `a` or `b` also works, but takes longer.\n"
+msgstr ""
+"\n"
+"这是一个解决方案，不唯一：\n"
+"```\n"
+"induction c with d hd\n"
+"rw [add_zero, mul_zero, add_zero]\n"
+"rfl\n"
+"rw [add_succ, mul_succ, hd, mul_succ, add_assoc]\n"
+"rfl\n"
+"```\n"
+"\n"
+"在 `a` 或 `b` 上进行数学归纳也可以，但需要多步骤。\n"
+
+#: Game.Levels.Multiplication.L08add_mul
+msgid "add_mul"
+msgstr "add_mul"
+
+#: Game.Levels.Multiplication.L08add_mul
+msgid ""
+"\n"
+"`add_mul` is just as fiddly to prove by induction; but there's a trick\n"
+"which avoids it. Can you spot it?\n"
+msgstr ""
+"\n"
+"用归纳法证明 `add_mul` 也很麻烦，但有个小窍门可以避免这个问题。\n"
+"可以避免这个问题。你能发现吗？\n"
+
+#: Game.Levels.Multiplication.L08add_mul
+msgid "`add_mul a b c` is a proof that $(a+b)c=ac+bc$."
+msgstr "`add_mul a b c` 是 $(a+b)c=ac+bc$ 的证明。"
+
+#: Game.Levels.Multiplication.L08add_mul
+msgid ""
+"Addition is distributive over multiplication.\n"
+"In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
+"$(a + b) \times c = ac + bc$."
+msgstr ""
+"加法和乘法有分配律。换句话说，对于所有自然数 $a$、$b$ 和 $c$，\n"
+"我们有 $(a + b) \\times c = ac + bc$。"
+
+#: Game.Levels.Multiplication.L08add_mul
+msgid ""
+"\n"
+"Here's my proof:\n"
+"```\n"
+"rw [mul_comm, mul_add]\n"
+"repeat rw [mul_comm c]\n"
+"rfl\n"
+"```\n"
+msgstr ""
+"\n"
+"这是我的证明：\n"
+"```\n"
+"rw [mul_comm, mul_add]\n"
+"repeat rw [mul_comm c]\n"
+"rfl\n"
+"```\n"
+
+#: Game.Levels.Multiplication.L09mul_assoc
+msgid "mul_assoc"
+msgstr "mul_assoc"
+
+#: Game.Levels.Multiplication.L09mul_assoc
+msgid ""
+"\n"
+"We now have enough to prove that multiplication is associative,\n"
+"the boss level of multiplication world. Good luck!\n"
+msgstr ""
+"\n"
+"我们现在有足够的工具去证明乘法服从结合律，\n"
+"乘法世界的boss关。祝你好运！\n"
+
+#: Game.Levels.Multiplication.L09mul_assoc
+msgid ""
+"`mul_assoc a b c` is a proof that `(a * b) * c = a * (b * c)`.\n"
+"\n"
+"Note that when Lean says `a * b * c` it means `(a * b) * c`.\n"
+"\n"
+"Note that `(a * b) * c = a * (b * c)` cannot be proved by \"pure thought\":\n"
+"for example subtraction is not associative, as `(6 - 2) - 1` is not\n"
+"equal to `6 - (2 - 1)`."
+msgstr ""
+"`mul_assoc a b c` 是 `(a * b) * c = a * (b * c)` 的证明。\n"
+"\n"
+"请注意，当 Lean 表示 `a * b * c` 时，它的意思是 `(a * b) * c`。\n"
+"\n"
+"请注意，`(a * b) * c = a * (b * c)` 不能仅凭“空想”来证明：例如，减法不是结合的，因为 `(6 - 2) - 1` 不等于 `6 - (2 - 1)`。"
+
+#: Game.Levels.Multiplication.L09mul_assoc
+msgid ""
+"Multiplication is associative.\n"
+"In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
+"$(ab)c = a(bc)$."
+msgstr ""
+"乘法服从结合律。\n"
+"换句话说，对于所有自然数 $a$、$b$ 和 $c$，我们有\n"
+"$(ab)c = a(bc)$。"
+
+#: Game.Levels.Multiplication.L09mul_assoc
+msgid ""
+"\n"
+"A passing mathematician notes that you've proved\n"
+"that the natural numbers are a commutative semiring.\n"
+"\n"
+"If you want to begin your journey to the final boss, head for Power World.\n"
+msgstr ""
+"\n"
+"一个路过的数学家指出，你已经证明了自然数是一个交换半环。\n"
+"\n"
+"如果你想开始通往最终Boss的旅程，那就前往幂世界。\n"
+
+#: Game.Levels.Multiplication
+msgid "Multiplication World"
+msgstr "乘法世界"
+
+#: Game.Levels.Multiplication
+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"
+"`37 * d`. What should `37 * succ d` be? Well, that's $(d+1)$ $37$s,\n"
+"so it should be `37 * d + 37`.\n"
+"\n"
+"Here are the definitions in Lean.\n"
+"\n"
+"  * `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"
+"Let's get started.\n"
+msgstr ""
+"我们应该如何定义 `37 * x`？就像加法一样，我们需要在 $x=0$ 和 $x$ 是后继数时给出定义。\n"
+"\n"
+"0的情况很简单：我们定义 `37 * 0` 为 `0`。现在假设我们知道 `37 * d`。`37 * succ d` 应该是什么呢？嗯，那是 $d+1$ 个 $37$，它应该是 `37 * d + 37`。\n"
+"\n"
+"以下是 Lean 中的定义。\n"
+"\n"
+"  * `mul_zero a : a * 0 = 0`\n"
+"  * `mul_succ a d : a * succ d = a * d + a`\n"
+"\n"
+"在这个世界中，我们不仅要证明关于乘法的事实，如 `a * b = b * a`，我们还必须证明乘法与加法相互作用的事实，如 `a * (b + c) = a * b + a * c`。\n"
+"让我们开始吧。\n"
+
+#: Game.Levels.Power.L01zero_pow_zero
+msgid "zero_pow_zero"
+msgstr "zero_pow_zero"
+
+#: Game.Levels.Power.L01zero_pow_zero
+msgid ""
+"Mathematicians sometimes debate what `0 ^ 0` is;\n"
+"the answer depends, of course, on your definitions. In this\n"
+"game, `0 ^ 0 = 1`. See if you can prove it.\n"
+"\n"
+"Check out the *Pow* tab in your list of theorems\n"
+"to see the new proofs which are available."
+msgstr ""
+"数学家们有时会争论 `0 ^ 0` 是什么；\n"
+"答案当然取决于你的定义。在这个\n"
+"游戏中，`0 ^ 0 = 1`。看看你能否证明这一点。\n"
+"\n"
+"查看定理列表中的 *Pow* 选项卡\n"
+"标签，查看可用的新证明。"
+
+#: Game.Levels.Power.L01zero_pow_zero
+msgid ""
+"`Pow a b`, with notation `a ^ b`, is the usual\n"
+"  exponentiation of natural numbers. Internally it is\n"
+"  defined via two axioms:\n"
+"\n"
+"  * `pow_zero a : a ^ 0 = 1`\n"
+"\n"
+"  * `pow_succ a b : a ^ succ b = a ^ b * a`\n"
+"\n"
+"Note in particular that `0 ^ 0 = 1`."
+msgstr ""
+"`Pow a b`，其符号表示为 `a ^ b`，是自然数的常规指数运算。在内部，它是通过两个公理定义的：\n"
+"\n"
+"* `pow_zero a : a ^ 0 = 1`\n"
+"\n"
+"* `pow_succ a b : a ^ succ b = a ^ b * a`\n"
+"\n"
+"特别要注意的是 `0 ^ 0 = 1`。"
+
+#: Game.Levels.Power.L01zero_pow_zero
+msgid ""
+"`pow_zero a : a ^ 0 = 1` is one of the two axioms\n"
+"defining exponentiation in this game."
+msgstr ""
+"`pow_zero a : a ^ 0 = 1` 是两个公理之一\n"
+"在这个游戏中定义指数。"
+
+#: Game.Levels.Power.L01zero_pow_zero
+msgid ""
+"Mathematicians sometimes argue that `0 ^ 0 = 0` is also\n"
+"a good convention. But it is not a good convention in this\n"
+"game; all the later levels come out beautifully with the\n"
+"convention that `0 ^ 0 = 1`."
+msgstr ""
+"数学家有时会争论说 0 ^ 0 = 0 也是一个很好的约定。\n"
+"但在本游戏中，这不是一个好的约定；所有后面的关卡也全都遵循 0 ^ 0 = 1 的约定。"
+
+#: Game.Levels.Power.L01zero_pow_zero
+msgid "$0 ^ 0 = 1$"
+msgstr "$0 ^ 0 = 1$"
+
+#: Game.Levels.Power.L02zero_pow_succ
+msgid "zero_pow_succ"
+msgstr "zero_pow_succ"
+
+#: Game.Levels.Power.L02zero_pow_succ
+msgid ""
+"We've just seen that `0 ^ 0 = 1`, but if `n`\n"
+"is a successor, then `0 ^ n = 0`. We prove that here."
+msgstr ""
+"我们刚刚看到 `0 ^ 0 = 1`，但如果 `n` 是后继数，\n"
+"则 `0 ^ n = 0`。我们将在这里证明这一点。"
+
+#: Game.Levels.Power.L02zero_pow_succ
+msgid ""
+"`pow_succ a b : a ^ (succ b) = a ^ b * a` is one of the\n"
+"two axioms defining exponentiation in this game."
+msgstr "`pow_succ a b : a ^ (succ b) = a ^ b * a` 是定义这个游戏中幂的两个公理中的一个。"
+
+#: Game.Levels.Power.L02zero_pow_succ
+msgid ""
+"Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if\n"
+"$n$ is a successor."
+msgstr "虽然在这个游戏中 $0^0=1$，但如果 $n>0$，即如果 $n$ 是后继数，那么 $0^n=0$。"
+
+#: Game.Levels.Power.L02zero_pow_succ
+msgid "For all numbers $m$, $0 ^{\\operatorname{succ} (m)} = 0$."
+msgstr "对于所有自然数 $m$、$0 ^{\\operatorname{succ} (m)} = 0$。"
+
+#: Game.Levels.Power.L03pow_one
+msgid "pow_one"
+msgstr "pow_one"
+
+#: Game.Levels.Power.L03pow_one
+msgid ""
+"`pow_one a` says that `a ^ 1 = a`.\n"
+"\n"
+"Note that this is not quite true by definition: `a ^ 1` is\n"
+"defined to be `a ^ 0 * a` so it's `1 * a`, and to prove\n"
+"that this is equal to `a` you need to use induction somewhere."
+msgstr ""
+"`pow_one a` 表示 `a ^ 1 = a`。\n"
+"\n"
+"请注意，这并不是完全根据定义来的：`a ^ 1` 被定义为 `a ^ 0 * a`，所以它是 `1 * a`，要证明这等于 `a`，你需要在某处使用数学归纳。"
+
+#: Game.Levels.Power.L03pow_one
+msgid "For all naturals $a$, $a ^ 1 = a$."
+msgstr "对于所有自然数 $a$、$a ^ 1 = a$。"
+
+#: Game.Levels.Power.L04one_pow
+msgid "one_pow"
+msgstr "one_pow"
+
+#: Game.Levels.Power.L04one_pow
+msgid "`one_pow n` is a proof that $1^n=1$."
+msgstr "`one_pow n` 是 $1^n=1$ 的证明。"
+
+#: Game.Levels.Power.L04one_pow
+msgid "For all naturals $m$, $1 ^ m = 1$."
+msgstr "对于所有自然数 $m$、$1 ^ m = 1$。"
+
+#: Game.Levels.Power.L05pow_two
+msgid "pow_two"
+msgstr "pow_two"
+
+#: Game.Levels.Power.L05pow_two
+msgid "Note: this lemma will be useful for the final boss!"
+msgstr "注意：这个引理对于解决最终的 Boss 很有用！"
+
+#: Game.Levels.Power.L05pow_two
+msgid "`pow_two a` says that `a ^ 2 = a * a`."
+msgstr "`pow_two a` 代表了 `a ^ 2 = a * a`。"
+
+#: Game.Levels.Power.L05pow_two
+msgid "For all naturals $a$, $a ^ 2 = a \times a$."
+msgstr "对于所有自然数 $a$、$a ^ 2 = a \times a$。"
+
+#: Game.Levels.Power.L06pow_add
+msgid "pow_add"
+msgstr "pow_add"
+
+#: Game.Levels.Power.L06pow_add
+msgid ""
+"Let's now begin our approach to the final boss,\n"
+"by proving some more subtle facts about powers."
+msgstr "现在让我们开始通过证明一些关于幂的更微妙的事实来接近最终的boss。"
+
+#: Game.Levels.Power.L06pow_add
+msgid "`pow_add a m n` is a proof that $a^{m+n}=a^ma^n.$"
+msgstr "`pow_add a m n` 是 $a^{m+n}=a^ma^n$ 的证明。"
+
+#: Game.Levels.Power.L06pow_add
+msgid "For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m  a ^ n$."
+msgstr "对于所有自然数 $a$、$m$、$n$，我们有 $a^{m + n} = a ^ m  a ^ n$ 。"
+
+#: Game.Levels.Power.L07mul_pow
+msgid "mul_pow"
+msgstr "mul_pow"
+
+#: Game.Levels.Power.L07mul_pow
+msgid ""
+"\n"
+"The music gets ever more dramatic, as we explore\n"
+"the interplay between exponentiation and multiplication.\n"
+"\n"
+"If you're having trouble exchanging the right `x * y`\n"
+"because `rw [mul_comm]` swaps the wrong multiplication,\n"
+"then read the documentation of `rw` for tips on how to fix this.\n"
+msgstr ""
+"\n"
+"当我们探索时，音乐变得更加戏剧化\n"
+"求幂和乘法之间的相互作用。\n"
+"\n"
+"如果您在更换正确的 `x * y` 时遇到问题\n"
+"因为 `rw [mul_comm]` 交换了错误的乘法，\n"
+"然后阅读 `rw` 的文档以获取有关如何解决此问题的提示。\n"
+
+#: Game.Levels.Power.L07mul_pow
+msgid "`mul_pow a b n` is a proof that $(ab)^n=a^nb^n.$"
+msgstr "`mul_pow a b n` 是 $(ab)^n=a^nb^n.$ 的证明"
+
+#: Game.Levels.Power.L07mul_pow
+msgid "For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$."
+msgstr "对于所有的自然数 $a$、$b$、$n$，我们有 $(ab) ^ n = a ^ nb ^ n$。"
+
+#: Game.Levels.Power.L08pow_pow
+msgid "pow_pow"
+msgstr "pow_pow"
+
+#: Game.Levels.Power.L08pow_pow
+msgid ""
+"\n"
+"One of the best named levels in the game, a savage `pow_pow`\n"
+"sub-boss appears as the music reaches a frenzy. What\n"
+"else could there be to prove about powers after this?\n"
+msgstr ""
+"\n"
+"游戏中最名副其实的关卡之一。\n"
+"随着音乐达到狂热，一个凶猛的 `pow_pow` 小boss出现了。\n"
+"在这之后，还有什么关于幂的性质需要证明呢？\n"
+
+#: Game.Levels.Power.L08pow_pow
+msgid "`pow_pow a m n` is a proof that $(a^m)^n=a^{mn}.$"
+msgstr "`pow_pow a m n` 是 $(a^m)^n=a^{mn}$ 的证明。"
+
+#: Game.Levels.Power.L08pow_pow
+msgid "For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$."
+msgstr "对于所有天然 $a$、$m$、$n$，我们有 $(a ^ m) ^ n = a ^ {mn}$。"
+
+#: Game.Levels.Power.L08pow_pow
+msgid ""
+"\n"
+"The music dies down. Is that it?\n"
+"\n"
+"Course it isn't, you can\n"
+"clearly see that there are two worlds left.\n"
+"\n"
+"A passing mathematician says that mathematicians don't have a name\n"
+"for the structure you just constructed. You feel cheated.\n"
+"\n"
+"Suddenly the music starts up again. This really is the final boss.\n"
+msgstr ""
+"\n"
+"背景音乐渐渐平息。是这样吗？\n"
+"\n"
+"当然不是，你可以\n"
+"清楚地看到剩下两个世界。\n"
+"\n"
+"路过的数学家说数学家没有名字\n"
+"对于您刚刚构建的结构。你感觉被欺骗了。\n"
+"\n"
+"突然音乐再次响起。这确实是最终boss。\n"
+
+#: Game.Levels.Power.L09add_sq
+msgid "add_sq"
+msgstr "add_sq"
+
+#: Game.Levels.Power.L09add_sq
+msgid ""
+"\n"
+"[final boss music]\n"
+msgstr ""
+"\n"
+"[最终Boss背景音乐]\n"
+"\n"
+
+#: Game.Levels.Power.L09add_sq
+msgid "`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$"
+msgstr "`add_sq a b` 是 $(a+b)^2=a^2+b^2+2ab$ 的证明。"
+
+#: Game.Levels.Power.L09add_sq
+msgid ""
+"For all numbers $a$ and $b$, we have\n"
+"$$(a+b)^2=a^2+b^2+2ab.$$"
+msgstr ""
+"对于所有数字 $a$ 和 $b$，我们有\n"
+"$$(a+b)^2=a^2+b^2+2ab.$$"
+
+#: Game.Levels.Power.L09add_sq
+msgid ""
+"\n"
+"It's all over! You have proved a theorem which has tripped up\n"
+"schoolkids for generations (some of them think $(a+b)^2=a^2+b^2$:\n"
+"this is \"the freshman's dream\").\n"
+"\n"
+"How many rewrites did you use? I can do it in 12.\n"
+"\n"
+"But wait! This boss is stirring...and mutating into a second more powerful form!\n"
+msgstr ""
+"\n"
+"一切都结束了！你已经证明了一个困扰了几代学生的定理\n"
+"（他们中的一些人认为 $(a+b)^2=a^2+b^2$ ：这就是“新生的白日梦”）。\n"
+"\n"
+"你用了多少次重写？我可以用12次做到。\n"
+"\n"
+"但等等！这个Boss被激怒了……并且变异成第二种更强大的形式！\n"
+
+#: Game.Levels.Power.L10FLT
+msgid "Fermat's Last Theorem"
+msgstr "费马大定理"
+
+#: Game.Levels.Power.L10FLT
+msgid ""
+"\n"
+"We now have enough to state a mathematically accurate, but slightly\n"
+"clunky, version of Fermat's Last Theorem.\n"
+"\n"
+"Fermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\n"
+"ot =z^m$.\n"
+"If you didn't do inequality world yet then we can't talk about $m \\geq 3$,\n"
+"so we have to resort to the hack of using `n + 3` for `m`,\n"
+"which guarantees it's big enough. Similarly instead of `x > 0` we\n"
+"use `a + 1`.\n"
+"\n"
+"This level looks superficially like other levels we have seen,\n"
+"but the shortest solution known to humans would translate into\n"
+"many millions of lines of Lean code. The author of this game,\n"
+"Kevin Buzzard, is working on translating the proof by Wiles\n"
+"and Taylor into Lean, although this task will take many years.\n"
+"\n"
+"## CONGRATULATIONS!\n"
+"\n"
+"You've finished the main quest of the natural number game!\n"
+"If you would like to learn more about how to use Lean to\n"
+"prove theorems in mathematics, then take a look\n"
+"at [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\n"
+"an interactive textbook which you can read in your browser,\n"
+"and which explains how to work with many more mathematical concepts in Lean.\n"
+msgstr ""
+"\n"
+"我们现在已经有足够的条件来陈述一个数学上准确但有些笨拙的费马大定理了。\n"
+"\n"
+"费马大定理指出，如果 $x,y,z>0$ 且 $m \\geq 3$，那么 $x^m+y^m \\not = z^m$。\n"
+"如果你还没学习过不等式世界，那么我们不能讨论 $m \\geq 3$，所以我们不得不采用使用 `n + 3` 代替 `m` 的方法，这保证了它足够大。同样，我们用 `a + 1` 代替 `x > 0`。\n"
+"\n"
+"这一关表面上看起来像我们见过的其他关卡，但人类已知的最短解法也将转化为数百万行的 Lean 代码。\n"
+"这个游戏的作者，Kevin Buzzard，正在将 Wiles 和 Taylor 的证明翻译成 Lean，尽管这项任务将花费许多年。\n"
+"\n"
+"## 祝贺！\n"
+"\n"
+"你已经完成了自然数游戏的主线任务！\n"
+"如果你想了解更多关于如何使用 Lean 来证明数学定理的信息，请查看 [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/)，\n"
+"这是一本互动教科书，你可以在浏览器中阅读它，它解释了如何在 Lean 中处理更多的数学概念。\n"
+
+#: Game.Levels.Power.L10FLT
+msgid ""
+"`xyzzy` is an ancient magic spell, believed to be the origin of the\n"
+"modern word `sorry`. The game won't complain - or notice - if you\n"
+"prove anything with `xyzzy`."
+msgstr "`xyzzy` 是一个古老的魔法咒语，被认为是现代词汇 `sorry` 的起源。游戏不会发现——或者注意到你用 `xyzzy` 证明任何东西。"
+
+#: Game.Levels.Power.L10FLT
+msgid ""
+"For all naturals $a$ $b$ $c$ and $n$, we have\n"
+"$$(a+1)^{n+3}+(b+1)^{n+3}\n"
+"ot=(c+1)^{n+3}.$$"
+msgstr ""
+"对于所有自然数 $a$ $b$ $c$ 和 $n$，我们有\n"
+"$$(a+1)^{n+3}+(b+1)^{n+3}\\not=(c+1)^{n+3}.$$"
+
+#: Game.Levels.Power.L10FLT
+msgid ""
+"\n"
+"Congratulations! You have proved Fermat's Last Theorem!\n"
+"\n"
+"Either that, or you used magic...\n"
+msgstr ""
+"\n"
+"恭喜！您已经证明了费马大定理！\n"
+"\n"
+"要么就是，要么你使用了魔法……\n"
+
+#: Game.Levels.Power
+msgid "Power World"
+msgstr "幂世界"
+
+#: Game.Levels.Power
+msgid ""
+"\n"
+"This world introduces exponentiation. If you want to define `37 ^ n`\n"
+"then, as always, you will need to know what `37 ^ 0` is, and\n"
+"what `37 ^ (succ d)` is, given only `37 ^ d`.\n"
+"\n"
+"You can probably guess the names of the general theorems:\n"
+"\n"
+"  * `pow_zero (a : ℕ) : a ^ 0 = 1`\n"
+"  * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n"
+"\n"
+"Using only these, can you get past the final boss level?\n"
+"\n"
+"The levels in this world were designed by Sian Carey, a UROP student\n"
+"at Imperial College London, funded by a Mary Lister McCammon Fellowship\n"
+"in the summer of 2019. Thanks to Sian and also thanks to Imperial\n"
+"College for funding her.\n"
+msgstr ""
+"\n"
+"这个世界引入了幂运算。如果你想定义 `37 ^ n`，那么像往常一样，你需要知道 `37 ^ 0` 是什么，以及在仅知 `37 ^ d` 的情况下，`37 ^ (succ d)` 是什么。\n"
+"\n"
+"你可能已经猜到了这些一般定理的名称：\n"
+"\n"
+"  * `pow_zero (a : ℕ) : a ^ 0 = 1`\n"
+"  * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n"
+"\n"
+"仅用这些定理，你能通过最后的boss关卡吗？\n"
+"\n"
+"这个世界中的关卡由帝国理工学院的 UROP 学生 Sian Carey 在 2019 年夏天设计，她的项目得到了 Mary Lister McCammon 奖学金的资助。感谢 Sian，也感谢帝国理工学院对她的资助。\n"
+
+#: Game.Levels.Implication.L01exact
+msgid "The `exact` tactic"
+msgstr "`exact` 策略"
+
+#: Game.Levels.Implication.L01exact
+msgid ""
+"## Summary\n"
+"\n"
+"If the goal is a statement `P`, then `exact h` will close the goal if `h` is a proof of `P`.\n"
+"\n"
+"### Example\n"
+"\n"
+"If the goal is `x = 37` and you have a hypothesis `h : x = 37`\n"
+"then `exact h` will solve the goal.\n"
+"\n"
+"### Example\n"
+"\n"
+"If the goal is `x + 0 = x` then `exact add_zero x` will close the goal.\n"
+"\n"
+"### Exact needs to be exactly right\n"
+"\n"
+"Note that `exact add_zero` will *not work* in the previous example;\n"
+"for `exact h` to work, `h` has to be *exactly* a proof of the goal.\n"
+"`add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,\n"
+"a proof of `? + 0 = ?` where `?` needs to be supplied by the user.\n"
+"This is in contrast to `rw` and `apply`, which will \"guess the inputs\"\n"
+"if necessary. If the goal is `x + 0 = x` then `rw [add_zero]`\n"
+"and `rw [add_zero x]` will both change the goal to `x = x`,\n"
+"because `rw` guesses the input to the function `add_zero`."
+msgstr ""
+"## 摘要\n"
+"\n"
+"如果目标是语句 `P`，那么如果 `h` 是 `P` 的证明，`exact h` 将关闭目标。\n"
+"\n"
+"#### 示例\n"
+"\n"
+"如果目标是 `x = 37`，假设是 `h : x = 37`\n"
+"则 `exact h` 将解决目标。\n"
+"\n"
+"### 示例\n"
+"\n"
+"如果目标是 `x + 0 = x`，那么 `exact add_zero x` 将关闭目标。\n"
+"\n"
+"### 精确需要完全正确\n"
+"\n"
+"请注意，`exact add_zero` 在上例中*不起作用；\n"
+"要让 `exact h` 起作用，`h` 必须*完全*是目标的证明。\n"
+"`add_zero` 是 `∀ n, n + 0 = n` 的证明，或者，如果你愿意的话、\n"
+"`? + 0 = ?` 的证明，其中 7qYkdnQ5WeV9ScjLHsz 需要由用户提供。\n"
+"这与 `rw` 和 `apply` 不同，它们会在必要时 \"猜测输入\"。\n"
+"如果需要的话。如果目标是 `x + 0 = x`，那么 `rw [add_zero]`\n"
+"和 `rw [add_zero x]` 都会将目标改为 `x = x`、\n"
+"因为 `rw` 猜到了函数 `add_zero` 的输入。"
+
+#: Game.Levels.Implication.L01exact
+msgid ""
+"\n"
+"In this world we'll learn how to prove theorems of the form $P\\implies Q$.\n"
+"In other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\n"
+"To do that we need to learn some more tactics.\n"
+"\n"
+"The `exact` tactic can be used to close a goal which is exactly one of\n"
+"the hypotheses.\n"
+msgstr ""
+"\n"
+"在这个世界中，我们将学习如何证明形式为 $P\\implies Q$ 的定理。\n"
+"换句话说，就是如何证明“如果 $P$ 为真，则 $Q$ 也为真”的形式的定理。\n"
+"为此，我们需要学习一些更多的策略。\n"
+"\n"
+"`exact` 策略可以用来解决一个存在于假设中的目标。\n"
+
+#: Game.Levels.Implication.L01exact
+msgid "Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$."
+msgstr "假设 $x+y=37$ 和 $3x+z=42$，我们有 $x+y=37$。"
+
+#: Game.Levels.Implication.L01exact
+msgid "The goal in this level is one of our hypotheses. Solve the goal by executing `exact h1`."
+msgstr "这一层的目标是我们的一个假设。通过执行 `exact h1` 来解决目标。"
+
+#: Game.Levels.Implication.L02exact2
+msgid "`exact` practice."
+msgstr "`exact` 练习。"
+
+#: Game.Levels.Implication.L02exact2
+msgid ""
+"If the goal is not *exactly* a hypothesis, we can sometimes\n"
+"use rewrites to fix things up."
+msgstr "如果目标并不 *完全* 是一个假设，我们有时可以使用重写来调整。"
+
+#: Game.Levels.Implication.L02exact2
+msgid "Assuming $0+x=(0+y)+2$, we have $x=y+2$."
+msgstr "假设 $0+x=(0+y)+2$，我们有 $x=y+2$。"
+
+#: Game.Levels.Implication.L02exact2
+msgid ""
+"You can use `rw [zero_add] at h` to rewrite at `«{h}»` instead\n"
+"of at the goal."
+msgstr "你可以使用 `rw [zero_add] at h` 来在 `«{h}»` 处进行重写，而不是在目标处进行。"
+
+#: Game.Levels.Implication.L02exact2
+msgid ""
+"Do that again!\n"
+"\n"
+"`rw [zero_add] at «{h}»` tries to fill in\n"
+"the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n"
+"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+msgstr ""
+"再做一次！\n"
+"\n"
+"`rw [zero_add] at «{h}»` 试图填充 `zero_add` 的参数（找到 `«{x}»`），然后替换它找到的所有 `0 + «{x}»` 出现的地方。因此，`0 + «{y}»`还没有被重写 。"
+
+#: Game.Levels.Implication.L02exact2
+msgid ""
+"Now you could finish with `rw [«{h}»]` then `rfl`, but `exact «{h}»`\n"
+"does it in one line."
+msgstr "现在你可以用 `rw [\"{h}\"]` 然后 `rfl` 来完成证明，但 `exact \"{h}\"` 可以在一行中做到同样的事。"
+
+#: Game.Levels.Implication.L02exact2
+msgid ""
+"Here's a two-line proof:\n"
+"```\n"
+"repeat rw [zero_add] at h\n"
+"exact h\n"
+"```\n"
+msgstr ""
+"这是一个两行证明：\n"
+"```\n"
+"repeat rw [zero_add] at h\n"
+"exact h\n"
+"```\n"
+
+#: Game.Levels.Implication.L03apply
+msgid "The `apply` tactic."
+msgstr "`apply` 策略。"
+
+#: Game.Levels.Implication.L03apply
+msgid ""
+"## Summary\n"
+"\n"
+"If `t : P → Q` is a proof that $P \\implies Q$, and `h : P` is a proof of `P`,\n"
+"then `apply t at h` will change `h` to a proof of `Q`. The idea is that if\n"
+"you know `P` is true, then you can deduce from `t` that `Q` is true.\n"
+"\n"
+"If the *goal* is `Q`, then `apply t` will \"argue backwards\" and change the\n"
+"goal to `P`. The idea here is that if you want to prove `Q`, then by `t`\n"
+"it suffices to prove `P`, so you can reduce the goal to proving `P`.\n"
+"\n"
+"### Example:\n"
+"\n"
+"`succ_inj x y` is a proof that `succ x = succ y → x = y`.\n"
+"\n"
+"So if you have a hypothesis `h : succ (a + 37) = succ (b + 42)`\n"
+"then `apply succ_inj at h` will change `h` to `a + 37 = b + 42`.\n"
+"You could write `apply succ_inj (a + 37) (b + 42) at h`\n"
+"but Lean is smart enough to figure out the inputs to `succ_inj`.\n"
+"\n"
+"### Example\n"
+"\n"
+"If the goal is `a * b = 7`, then `apply succ_inj` will turn the\n"
+"goal into `succ (a * b) = succ 7`."
+msgstr ""
+"## 小结\n"
+"\n"
+"如果 `t : P → Q` 是一个 $P\\implies Q$ 的证明，而 `h : P` 是一个 `P` 的证明，那么 `apply t at h` 会将 `h` 转换为证明 `Q`。其原理是，如果您知道 `P` 为真，那么您可以从 `t` 推断出 `Q` 为真。\n"
+"\n"
+"如果*目标*是 `Q`，那么 `apply t` 会“逆向推理”并将目标转换为 `P`。在这里，如果您想证明 `Q`，那么根据 `t`，只需证明 `P` 即可，因此您可以将目标简化为证明 `P`。\n"
+"\n"
+"### 示例：\n"
+"\n"
+"`succ_inj x y` 是一个 `succ x = succ y → x = y` 的证明。\n"
+"\n"
+"因此，如果您有一个假设 `h : succ (a + 37) = succ (b + 42)`，那么 `apply succ_inj at h` 会将 `h` 转换为 `a + 37 = b + 42`。您可以写 `apply succ_inj (a + 37) (b + 42) at h`，但 Lean 足够聪明，可以自行推断出 `succ_inj` 的输入。\n"
+"\n"
+"### 示例：\n"
+"\n"
+"如果目标是 `a * b = 7`，那么 `apply succ_inj` 会将目标转换为 `succ (a * b) = succ 7`。"
+
+#: Game.Levels.Implication.L03apply
+msgid ""
+"\n"
+"In this level one of our hypotheses is an *implication*. We can use this\n"
+"hypothesis with the `apply` tactic.\n"
+msgstr ""
+"\n"
+"在这个层级中，我们的一个假设是一个*蕴含式*。我们可以使用 `apply` 策略来利用这个假设。\n"
+
+#: Game.Levels.Implication.L03apply
+msgid "If $x=37$ and we know that $x=37\\implies y=42$ then we can deduce $y=42$."
+msgstr "如果 $x=37$ 并且我们知道 $x=37 \\implies y=42$，那么我们可以推导出 $y=42$。"
+
+#: Game.Levels.Implication.L03apply
+msgid "Start with `apply h2 at h1`. This will change `h1` to `y = 42`."
+msgstr "从 `apply h2 at h1` 开始。这将会把 `h1` 改为 `y = 42`。"
+
+#: Game.Levels.Implication.L03apply
+msgid "Now finish using the `exact` tactic."
+msgstr "现在使用 `exact` 策略完成证明。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid "succ_inj : the successor function is injective"
+msgstr "succ_inj ：后继数是单射的"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"\n"
+"If `a` and `b` are numbers, then `succ_inj a b` is a proof\n"
+"that `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*\n"
+"tab for more information.\n"
+"\n"
+"Peano had this theorem as an axiom, but in Algorithm World\n"
+"we will show how to prove it in Lean. Right now let's just assume it,\n"
+"and let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed\n"
+"by manipulating our hypothesis until it becomes the goal. I will\n"
+"walk you through this level.\n"
+msgstr ""
+"\n"
+"如果 `a` 和 `b` 是数字，那么 `succ_inj a b` 是一个证明，表明 `succ a = succ b` 意味着 `a = b`。点击 *Peano* 标签中的这个定理以获取更多信息。\n"
+"\n"
+"皮亚诺将这个定理作为一个公理，但在算法世界中我们将展示如何在 Lean 中证明它。\n"
+"现在让我们先假设它，然后让我们使用它证明 $x+1=4 \\implies x=3$。再一次，我们将通过操纵我们的假设直到它变成目标来进行。我将引导你通过这个层级。\n"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"# Statement\n"
+"\n"
+"If $a$ and $b$ are numbers, then\n"
+"`succ_inj a b` is the proof that\n"
+"$ (\\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
+"\n"
+"## More technical details\n"
+"\n"
+"There are other ways to think about `succ_inj`.\n"
+"\n"
+"You can think about `succ_inj` itself as a function which takes two\n"
+"numbers $$a$$ and $$b$$ as input, and outputs a proof of\n"
+"$ ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
+"\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"
+"\n"
+"`succ_inj` was postulated as an axiom by Peano, but\n"
+"in Lean it can be proved using `pred`, a mathematically\n"
+"pathological function."
+msgstr ""
+"# 陈述\n"
+"\n"
+"如果 \\( a \\) 和 \\( b \\) 是数字，那么\n"
+"`succ_inj a b` 是\n"
+"\\( (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b \\) 的证明。\n"
+"\n"
+"## 更多技术细节\n"
+"\n"
+"你可以用其他方式思考 `succ_inj`。\n"
+"\n"
+"你可以把 `succ_inj` 本身想象成一个函数，它接受两个数字 $$a$$ 和 $$b$$ 作为输入，并输出\n"
+"\\( (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b \\) 的证明。\n"
+"\n"
+"你可以把 `succ_inj` 本身看作是一个证明；它是 `succ` 是一个单射函数的证明。换句话说，\n"
+"`succ_inj` 是\n"
+"\\( \\forall a, b \\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b \\) 的证明。\n"
+"\n"
+"`succ_inj` 被皮亚诺假设为一个公理，但在 Lean 中可以使用 `pred` 来证明，这是一个在数学上有病态的函数。"
+
+#: Game.Levels.Implication.L04succ_inj Game.Levels.Implication.L05succ_inj2
+msgid "If $x+1=4$ then $x=3$."
+msgstr "如果 $x+1=4$ 则 $x=3$。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"Let's first get `h` into the form `succ x = succ 3` so we can\n"
+"apply `succ_inj`. First execute `rw [four_eq_succ_three] at h`\n"
+"to change the 4 on the right hand side."
+msgstr "首先让 `h` 变为 `succ x = succ 3` 的形式，这样我们就可以应用 `succ_inj`。首先执行 `rw [four_eq_succ_three] at h` 来改变右手边的4。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"Now rewrite `succ_eq_add_one` backwards at `h`\n"
+"to get the right hand side."
+msgstr "现在在 `h` 处反向重写 `succ_eq_add_one` 来得到右边式子。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"You can put a `←` in front of any theorem provided to `rw` to rewrite\n"
+"the other way around. Look at the docs for `rw` for an explanation. Type `←` with `\\l`."
+msgstr "你可以在提供给 `rw` 的任何定理前面放一个 `←` 来进行反向重写。查看 `rw` 的文档以获得解释。使用 `\\l` 输入 `←`。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid "Concretely: `rw [← succ_eq_add_one] at h`."
+msgstr "具体来说，就是：`rw [← succ_eq_add_one] at h`。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"Now let's `apply` our new theorem. Execute `apply succ_inj at h`\n"
+"to change `h` to a proof of `x = 3`."
+msgstr "现在让我们应用（ `apply` ）我们的新定理。执行 `apply succ_inj at h` 来将 `h` 变为证明 `x = 3` 的证据。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid "Now finish in one line."
+msgstr "现在再用一行完成证明。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid ""
+"And now we've deduced what we wanted to prove: the goal is one of our assumptions.\n"
+"Finish the level with `exact h`."
+msgstr ""
+"现在我们已经推导出了我们想要证明的了：目标是我们的假设之一。\n"
+"用 `exact h` 完成本关。"
+
+#: Game.Levels.Implication.L04succ_inj
+msgid "In the next level, we'll do the same proof but backwards."
+msgstr "在下一级别中，我们将进行相同的证明，但要从后往前证。"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid "Arguing backwards"
+msgstr "从后向前证明"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid ""
+"\n"
+"  In the last level, we manipulated the hypothesis `x + 1 = 4`\n"
+"  until it became the goal `x = 3`. In this level we'll manipulate\n"
+"  the goal until it becomes our hypothesis! In other words, we\n"
+"  will \"argue backwards\". The `apply` tactic can do this too.\n"
+"  Again I will walk you through this one (assuming you're in\n"
+"  command line mode).\n"
+msgstr ""
+"\n"
+"在最后一关，我们操纵了假设 `x + 1 = 4`\n"
+"  直到成为目标 `x = 3` 。在这一关我们将改写\n"
+"  目标，直到它成为我们的假设！换句话说，我们\n"
+"  会从后向前证明。 `apply` 策略也可以做到这一点。\n"
+"  我将再次引导您完成这一过程（假设您在\n"
+"  命令行模式）。\n"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid "Start with `apply succ_inj` to apply `succ_inj` to the *goal*."
+msgstr "从 `apply succ_inj` 开始，将 `succ_inj` 应用于 *goal* （目标）。"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid ""
+"Applying a proof of $P\\implies Q$ to the *goal* changes $Q$ to $P$.\n"
+"Now try `rw [succ_eq_add_one]` to make the goal more like the hypothesis."
+msgstr ""
+"应用一个 $P\\implies Q$ 的证明到*目标*上，会将 $Q$ 变为 $P$。\n"
+"现在尝试使用 `rw [succ_eq_add_one]` 来使目标更像假设。"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid ""
+"Now rewrite `four_eq_succ_three` backwards to make the goal\n"
+"equal to the hypothesis."
+msgstr "现在反方向重写 `four_eq_succ_three` 使目标等于假设。"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid "You can now finish with `exact h`."
+msgstr "现在您可以使用 `exact h` 来完成证明。"
+
+#: Game.Levels.Implication.L05succ_inj2
+msgid ""
+"Many people find `apply t at h` easy, but some find `apply t` confusing.\n"
+"If you find it confusing, then just argue forwards.\n"
+"\n"
+"You can read more about the `apply` tactic in its documentation, which you can view by\n"
+"clicking on the tactic in the list on the right."
+msgstr ""
+"许多人觉得 `apply t at h` 很容易，但有些人觉得 `apply t` 令人困惑。\n"
+"如果你觉得很困惑，那就用前一种吧。\n"
+"\n"
+"您可以在其文档中阅读有关 `apply` 策略的更多信息，您可以通过\n"
+"单击右侧列表中的策略的方式查看。"
+
+#: Game.Levels.Implication.L06intro
+msgid "intro"
+msgstr "intro"
+
+#: Game.Levels.Implication.L06intro
+msgid ""
+"## Summary\n"
+"\n"
+"If the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,\n"
+"and change the goal to `Q`. Mathematically, it says that to prove $P \\implies Q$,\n"
+"we can assume $P$ and then prove $Q$.\n"
+"\n"
+"### Example:\n"
+"\n"
+"If your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1 \\implies x=y$)\n"
+"then `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal\n"
+"will change to $x=y$."
+msgstr ""
+"## 小结\n"
+"\n"
+"如果目标是 `P → Q`，那么 `intro h` 将引入 `h : P` 作为假设，\n"
+"并将目标更改为 `Q`。从数学上讲，要证明 $P\\implies Q$，\n"
+"我们可以假设 $P$ ，然后证明 $Q$ 。\n"
+"\n"
+"### 例子：\n"
+"\n"
+"如果您的目标是 `x + 1 = y + 1 → x = y` （在Lean中这表示 $x+1=y+1\\implies x=y$ ）\n"
+"那么 `intro h` 会给你一个名为 `h` 的假设 $x+1=y+1$ ，目标\n"
+"也同时更改为 $x=y$。"
+
+#: Game.Levels.Implication.L06intro
+msgid ""
+"We have seen how to `apply` theorems and assumptions\n"
+"of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
+"To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\n"
+"in Lean. We do this with the `intro` tactic.\n"
+msgstr ""
+"我们已经看到了如何 `apply` 形式为 `P → Q` 的定理和假设。\n"
+"但如果我们的 *目标* 是形式为 `P → Q` 的呢？\n"
+"要证明这个目标，我们需要知道如何在 Lean 中表示 “假设 `P` 并推导出 `Q`”。我们用 `intro` 策略来做这件事。\n"
+
+#: Game.Levels.Implication.L06intro
+msgid "$x=37\\implies x=37$."
+msgstr "$x=37\\implies x=37$ 。"
+
+#: Game.Levels.Implication.L06intro
+msgid "Start with `intro h` to assume the hypothesis and call its proof `h`."
+msgstr "使用 `intro h` 来设假设为 `h`。"
+
+#: Game.Levels.Implication.L06intro
+msgid "Now `exact h` finishes the job."
+msgstr "现在，用 `exact h ` 完成证明。"
+
+#: Game.Levels.Implication.L07intro2
+msgid "intro practice"
+msgstr "入门练习（译注：翻译存疑，没刷过最新版本，有可能是 `intro` 策略的练习。）"
+
+#: Game.Levels.Implication.L07intro2
+msgid ""
+" Let's see if you can use the tactics we've learnt to prove $x+1=y+1\\implies x=y$.\n"
+"Try this one by yourself; if you need help then click on \"Show more help!\".\n"
+msgstr ""
+"让我们看看您能否利用我们学到的策略来证明 $x+1=y+1\\implies x=y$。\n"
+"如果您需要帮助，请点击 \"显示更多帮助！\"。\n"
+
+#: Game.Levels.Implication.L07intro2
+msgid "$x+1=y+1 \\implies x=y$."
+msgstr "$x+1=y+1\\implies x=y$。"
+
+#: Game.Levels.Implication.L07intro2
+msgid "Start with `intro h` to assume the hypothesis."
+msgstr "用 `intro h` 开始设假设。"
+
+#: Game.Levels.Implication.L07intro2
+msgid ""
+"Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\n"
+"change `succ x = succ y`."
+msgstr "现在 `repeat rw [← succ_eq_add_one] at h` 是改写 `succ x = succ y` 的最快方法。"
+
+#: Game.Levels.Implication.L07intro2
+msgid "Now `apply succ_inj at h` to cancel the `succ`s."
+msgstr "现在使用 `apply succ_inj at h` 来消去 `succ`。"
+
+#: Game.Levels.Implication.L07intro2
+msgid "Now `rw [h]` then `rfl` works, but `exact h` is quicker."
+msgstr "现在 `rw [h]` 和 `rfl` 可以完成证明，但 `exact h` 更快。"
+
+#: Game.Levels.Implication.L07intro2
+msgid ""
+"Here's a completely backwards proof:\n"
+"```\n"
+"intro h\n"
+"apply succ_inj\n"
+"repeat rw [succ_eq_add_one]\n"
+"exact h\n"
+"```\n"
+msgstr ""
+"这是一个完全逆向的证明过程：\n"
+"```\n"
+"intro h\n"
+"apply succ_inj\n"
+"repeat rw [succ_eq_add_one]\n"
+"exact h\n"
+"```\n"
+
+#: Game.Levels.Implication.L08ne
+msgid "≠"
+msgstr "≠"
+
+#: Game.Levels.Implication.L08ne
+msgid ""
+"We still can't prove `2 + 2 ≠ 5` because we have not talked about the\n"
+"definition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.\n"
+"Here `False` is a generic false proposition, and `→` is Lean's notation\n"
+"for \"implies\". In logic we learn\n"
+"that `True → False` is false, but `False → False` is true. Hence\n"
+"`X → False` is the logical opposite of `X`.\n"
+"\n"
+"Even though `a ≠ b` does not look like an implication,\n"
+"you should treat it as an implication. The next two levels will show you how.\n"
+"\n"
+"`False` is a goal which you cannot deduce from a consistent set of assumptions!\n"
+"So if your goal is `False` then you had better hope that your hypotheses\n"
+"are contradictory, which they are in this level.\n"
+msgstr ""
+"我们仍然不能证明 `2 + 2 ≠ 5`，因为我们还没有讨论 `≠` 的定义。在 Lean 中，`a ≠ b` 是 `a = b → False` 的*符号表示*。这里的 `False` 是一个通用的假命题，`→` 是 Lean 中表示“蕴含”的符号\n"
+"。\n"
+"在逻辑学中我们学到，`True → False` 是假的，但 `False → False` 是真的。因此，`X → false` 是 `X` 的逻辑取反。\n"
+"\n"
+"尽管 `a ≠ b` 看起来不像蕴含，你应该将其视为蕴含。接下来的两关将向你展示怎样使用它。\n"
+"\n"
+"`False` 是一个无法从一致的假设集中推导出的目标！所以如果你的目标是 `False`，那么你最好希望你的假设是矛盾的，就像在本关中一样。\n"
+
+#: Game.Levels.Implication.L08ne
+msgid ""
+"If $x=y$ and $x \n"
+"eq y$ then we can deduce a contradiction."
+msgstr ""
+"如果 $x=y$ 且 $x \n"
+"eq y$ 那么我们可以推出矛盾。"
+
+#: Game.Levels.Implication.L08ne
+msgid ""
+"Remember that `h2` is a proof of `x = y → False`. Try\n"
+"`apply`ing `h2` either `at h1` or directly to the goal."
+msgstr "记住，`h2` 是 `x = y → False` 的证明。尝试将 `h2` 应用（`apply`）于 `h1` 或直接应用于目标。"
+
+#: Game.Levels.Implication.L08ne
+msgid ""
+"`a ≠ b` is *notation* for `(a = b) → False`.\n"
+"\n"
+"The reason this is mathematically\n"
+"valid is that if `P` is a true-false statement then `P → False`\n"
+"is the logical opposite of `P`. Indeed `True → False` is false,\n"
+"and `False → False` is true!\n"
+"\n"
+"The upshot of this is that use can treat `a ≠ b` in exactly\n"
+"the same way as you treat any implication `P → Q`. For example,\n"
+"if your *goal* is of the form `a ≠ b` then you can make progress\n"
+"with `intro h`, and if you have a hypothesis `h` of the\n"
+"form `a ≠ b` then you can `apply h at h1` if `h1` is a proof\n"
+"of `a = b`."
+msgstr ""
+"`a ≠ b` 是由 `(a = b) → False` 定义的 。\n"
+"\n"
+"  这在数学上合法的原因是，如果 `P` 是一个真假陈述，那么 `P → False`\n"
+"  与 `P` 的逻辑相反。确实 `True → False` 是假的，\n"
+"  `False → False` 是真的！\n"
+"\n"
+"  这样做的结果是，\n"
+"  可用处理任何 `P → Q` 的方式处理 `a ≠ b`。例如，\n"
+"  如果 *目标* 的形式为 `a ≠ b` 那么您可以用 `intro h`取得进展；\n"
+"  如果你有一个假设 `h : a ≠ b` 那么你可以 `apply h at h1` 如果 `h1` 是\n"
+"  `a = b`的假设。"
+
+#: Game.Levels.Implication.L08ne
+msgid "Remember, `x ≠ y` is *notation* for `x = y → False`."
+msgstr "记住，`x ≠ y` 是 `x = y → False` 的 *符号表示* 。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid "zero_ne_succ"
+msgstr "zero_ne_succ"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid ""
+"`zero_ne_succ n` is the proof that `0 ≠ succ n`.\n"
+"\n"
+"In Lean, `a ≠ b` is *defined to mean* `a = b → False`. Hence\n"
+"`zero_ne_succ n` is really a proof of `0 = succ n → False`.\n"
+"Here `False` is a generic false statement. This means that\n"
+"you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`."
+msgstr ""
+"`zero_ne_succ n` 是 `0 ≠ succ n` 的证明。\n"
+"\n"
+"在 Lean 中，`a ≠ b` *被定义为* `a = b → False`。\n"
+"因此，`zero_ne_succ n` 实际上是 `0 = succ n → False` 的证明。\n"
+"这里的 `False` 是一个通用的假命题。这意味着如果 `h` 是 `0 = succ n` 的证明，你可以 `apply zero_ne_succ at h`。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid ""
+"\n"
+"As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to\n"
+"introduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.\n"
+"To learn about this result, click on it in the list of lemmas on the right.\n"
+msgstr ""
+"\n"
+"作为 `2 + 2 ≠ 5` 的热身，我们来证明 `0 ≠ 1`。为此，我们需要\n"
+"介绍一下Peano的最后一个公理`zero_ne_succ n`，证明`0 ≠ succ n`。\n"
+"要了解此结论，请在右侧的引理列表中单击它。\n"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid "`zero_ne_one` is a proof of `0 ≠ 1`."
+msgstr "`zero_ne_one` 是 `0 ≠ 1` 的证明。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid ""
+"$0\n"
+"eq1$."
+msgstr ""
+"$0\n"
+"eq1$ 。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid "Start with `intro h`."
+msgstr "从 `intro h` 开始。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid "Now change `1` to `succ 0` in `h`."
+msgstr "现在将 `h` 中的 `1` 改写为 `succ 0`。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+msgid "Now you can `apply zero_ne_succ at h`."
+msgstr "现在可以使用 `apply zero_ne_succ at h`。"
+
+#: Game.Levels.Implication.L09zero_ne_succ
+#: Game.Levels.AdvAddition.L01add_right_cancel
+msgid "Nice!"
+msgstr "好的！"
+
+#: Game.Levels.Implication.L10one_ne_zero
+msgid "1 ≠ 0"
+msgstr "1 ≠ 0"
+
+#: Game.Levels.Implication.L10one_ne_zero
+msgid ""
+"\n"
+"We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\n"
+"if we have a hypothesis `succ n = 0`? It's the wrong way around!\n"
+"\n"
+"The `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\n"
+"to `y ≠ x`. And `symm at h`\n"
+"does the same for a hypothesis `h`. We've proved $0 \n"
+"eq 1$ and called\n"
+"the proof `zero_ne_one`; now try proving $1 \n"
+"eq 0$.\n"
+msgstr ""
+"\n"
+"我们知道 `zero_ne_succ n` 是证明 `0 = succ n → False` 的证明。但是如果我们有一个假设 `succ n = 0` 呢？这恰好是反过来的！\n"
+"\n"
+"`symm` 策略可以将目标 `x = y` 改为 `y = x`，并将目标 `x ≠ y` 改为 `y ≠ x`。而 `symm at h` 对假设 `h` 也做同样的操作。\n"
+"我们已经证明了 $0 ≠ 1$，并将证明命名为 `zero_ne_one`；现在请尝试证明 $1 ≠ 0$。\n"
+
+#: Game.Levels.Implication.L10one_ne_zero
+msgid ""
+"## Summary\n"
+"\n"
+"The `symm` tactic will change a goal or hypothesis of\n"
+"the form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\n"
+"and on `X ↔ Y`.\n"
+"\n"
+"### Example\n"
+"\n"
+"If the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n"
+"\n"
+"### Example\n"
+"\n"
+"If `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`."
+msgstr ""
+"## 小结\n"
+"\n"
+"`symm` 策略会将形如 `X = Y` 的目标或假设转换为 `Y = X`。它也适用于 `X ≠ Y` 和 `X ↔ Y`。\n"
+"\n"
+"### 例子\n"
+"\n"
+"如果目标是 `2 + 2 = 4`，那么 `symm` 会将其转换为 `4 = 2 + 2`。\n"
+"\n"
+"### 例子\n"
+"\n"
+"如果 `h : 2 + 2 ≠ 5`，那么 `symm at h` 会将 `h` 转换为 `5 ≠ 2 + 2`。"
+
+#: Game.Levels.Implication.L10one_ne_zero
+msgid "`one_ne_zero` is a proof that `1 ≠ 0`."
+msgstr "`one_ne_zero` 是 `1 ≠ 0` 的证明。"
+
+#: Game.Levels.Implication.L10one_ne_zero
+msgid ""
+"$1\n"
+"eq0$."
+msgstr ""
+"$1\n"
+"eq0$ 。"
+
+#: Game.Levels.Implication.L10one_ne_zero
+msgid ""
+"What do you think of this two-liner:\n"
+"```\n"
+"symm\n"
+"exact zero_ne_one\n"
+"```\n"
+"\n"
+"`exact` doesn't just take hypotheses, it will eat any proof which exists\n"
+"in the system.\n"
+msgstr ""
+"你对这两行代码有什么看法？\n"
+"\n"
+"```\n"
+"symm\n"
+"exact zero_ne_one\n"
+"```\n"
+"\n"
+"请注意，`exact` 不仅限于使用假设，它可以接受系统中存在的任何证明。\n"
+
+#: Game.Levels.Implication.L11two_add_two_ne_five
+msgid "2 + 2 ≠ 5"
+msgstr "2 + 2 ≠ 5"
+
+#: Game.Levels.Implication.L11two_add_two_ne_five
+msgid ""
+" 2 + 2 ≠ 5 is boring to prove in full, given only the tools we have currently.\n"
+"To make it a bit less painful, I have unfolded all of the numerals for you.\n"
+"See if you can use `zero_ne_succ` and `succ_inj` to prove this.\n"
+msgstr ""
+"仅凭我们目前拥有的工具，完整证明 2 + 2 ≠ 5 是很无聊的。\n"
+"为了减轻您的痛苦，我为您展开了所有数字。\n"
+"看看是否可以使用 `zero_ne_succ` 和 `succ_inj` 来证明它。\n"
+
+#: Game.Levels.Implication.L11two_add_two_ne_five
+msgid "$2+2≠5$."
+msgstr "$2+2≠5$."
+
+#: Game.Levels.Implication.L11two_add_two_ne_five
+msgid ""
+"Here's my proof:\n"
+"```\n"
+"intro h\n"
+"rw [add_succ, add_succ, add_zero] at h\n"
+"repeat apply succ_inj at h\n"
+"apply zero_ne_succ at h\n"
+"exact h\n"
+"```\n"
+"\n"
+"Even though Lean is a theorem prover, right now it's pretty clear that we have not\n"
+"developed enough material to make it an adequate calculator. In Algorithm\n"
+"World, a more computer-sciency world, we will develop machinery which makes\n"
+"questions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.\n"
+"Alternatively you can do more mathematics in Advanced Addition World, where we prove\n"
+"the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\n"
+"decide your route."
+msgstr ""
+"这是一个证明：\n"
+"```\n"
+"intro h\n"
+"rw [add_succ, add_succ, add_zero] at h\n"
+"repeat apply succ_inj at h\n"
+"apply zero_ne_succ at h\n"
+"exact h\n"
+"```\n"
+"\n"
+"\n"
+"尽管 Lean 是一个定理证明器，但目前很明显我们还没有发展足够的素材使其成为一个足够的计算器。\n"
+"在算法世界中，一个更偏向计算机科学的世界，我们将开发使这类问题变得更容易的机制。\n"
+"证明像 $20 + 20 ≠ 41$ 这样的目标会变得很容易。\n"
+"或者你可以在高级加法世界中做更多数学，\n"
+"我们在那里证明了建立不等式理论所需的引理。点击“离开世界”并决定你的路线。"
+
+#: Game.Levels.Implication
+msgid "Implication World"
+msgstr "蕴含世界"
+
+#: Game.Levels.Implication
+msgid ""
+"\n"
+"We've proved that $2+2=4$; in Implication World we'll learn\n"
+"how to prove $2+2\n"
+"eq 5$.\n"
+"\n"
+"In Addition World we proved *equalities* like $x + y = y + x$.\n"
+"In this second tutorial world we'll learn some new tactics,\n"
+"enabling us to prove *implications*\n"
+"like $x+1=4 \\implies x=3.$\n"
+"\n"
+"We'll also learn two new fundamental facts about\n"
+"natural numbers, which Peano introduced as axioms.\n"
+"\n"
+"Click on \"Start\" to proceed.\n"
+msgstr ""
+"\n"
+"我们已经证明了 $2+2=4$；在《蕴涵世界》中，我们将学习\n"
+"如何证明 $2+2\n"
+"eq 5$。\n"
+"\n"
+"在 \"加法世界 \"中，我们将证明 $x + y = y + x$ 等*等式。\n"
+"在第二个教程世界中，我们将学习一些新的策略、\n"
+"使我们能够证明\n"
+"如 $x+1=4 \\implies x=3.$\n"
+"\n"
+"我们还将学习关于自然数的两个新的基本事实。\n"
+"自然数的两个新的基本事实。\n"
+"\n"
+"点击 \"开始 \"继续。\n"
+
+#: Game.Levels.Algorithm.L01add_left_comm
+msgid "add_left_comm"
+msgstr "add_left_comm"
+
+#: Game.Levels.Algorithm.L01add_left_comm
+msgid "`add_left_comm a b c` is a proof that `a + (b + c) = b + (a + c)`."
+msgstr "`add_left_comm a b c` 是 `a + (b + c) = b + (a + c)` 的证明。"
+
+#: Game.Levels.Algorithm.L01add_left_comm
+msgid ""
+"Having to rearrange variables manually using commutativity and\n"
+"associativity is very tedious. We start by reminding you of this. `add_left_comm`\n"
+"is a key component in the first algorithm which we'll explain, but we need\n"
+"to prove it manually.\n"
+"\n"
+"Remember that you can do precision commutativity rewriting\n"
+"with things like `rw [add_comm b c]`. And remember that\n"
+"`a + b + c` means `(a + b) + c`.\n"
+msgstr ""
+"我们首先提醒您一点，手动使用交换律和结合律来重新排列变量是非常繁琐的。\n"
+"`add_left_comm` 是我们将要解释的第一个算法中的关键组件，但我们需要手动证明它。\n"
+"\n"
+"请记住，您可以使用 `rw [add_comm b c]` 之类的命令进行精确的交换律重写。并记住 `a + b + c` 表示 `(a + b) + c`。\n"
+
+#: Game.Levels.Algorithm.L01add_left_comm
+msgid "If $a, b, c$ are numbers, then $a+(b+c)=b+(a+c)$."
+msgstr "如果 $a, b, c$ 是自然数，那么 $a+(b+c)=b+(a+c)$。"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid "making life easier"
+msgstr "让生活更轻松"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid ""
+"\n"
+"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"
+"In this level, `(a + b) + (c + d) = ((a + c) + d) + b`,\n"
+"let's forget about the brackets and just think about\n"
+"the variable order.\n"
+"To turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,\n"
+"and then swap `b` and `d`. But this is easier than you\n"
+"think with `add_left_comm`.\n"
+msgstr ""
+"\n"
+"在一些后续的世界中，我们将看到一些更棘手的层级，比如 `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`。需要移动括号，还需要交换变量。\n"
+"\n"
+"在这个层级中，`(a + b) + (c + d) = ((a + c) + d) + b`，让我们忘掉括号，只考虑变量的顺序。\n"
+"要将 `a+b+c+d` 转换成 `a+c+d+b`，我们需要交换 `b` 和 `c`，然后交换 `b` 和 `d`。但是使用 `add_left_comm` 比你想象的要简单。\n"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid ""
+"If $a, b$, $c$ and $d$ are numbers, we have\n"
+"$(a + b) + (c + d) = ((a + c) + d) + b.$"
+msgstr ""
+"如果 $a, b$、$c$ 和 $d$ 是自然数，我们有\n"
+"$(a + b) + (c + d) = ((a + c) + d) + b.$"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid "Start with `repeat rw [add_assoc]` to push all the brackets to the right."
+msgstr "从 `repeat rw [add_assoc]` 开始，将所有的括号推到右边。"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid ""
+"Now use `rw [add_left_comm b c]` to switch `b` and `c` on the left\n"
+"hand side."
+msgstr "现在使用 `rw [add_left_comm b c]` 将左侧的 `b` 和 `c` 交换。"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid "Finally use a targetted `add_comm` to switch `b` and `d`"
+msgstr "最后，使用有针对性的 `add_comm` 来交换 `b` 和 `d"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid "`rw [add_comm b d]`."
+msgstr "`rw [add_comm b d]`。"
+
+#: Game.Levels.Algorithm.L02add_algo1
+msgid ""
+"\n"
+"So that's the algorithm: now let's use automation to perform it\n"
+"automatically.\n"
+msgstr ""
+"\n"
+"所以这就是算法：现在让我们使用机器来自动执行它。\n"
+
+#: Game.Levels.Algorithm.L03add_algo2
+msgid "making life simple"
+msgstr "让生活变得简单"
+
+#: Game.Levels.Algorithm.L03add_algo2
+msgid ""
+"# Overview\n"
+"\n"
+"Lean's simplifier, `simp`, will rewrite every lemma\n"
+"tagged with `simp` and every lemma fed to it by the user, as much as it can.\n"
+"Furthermore, it will attempt to order variables into an internal order if fed\n"
+"lemmas such as `add_comm`, so that it does not go into an infinite loop."
+msgstr ""
+"＃ 概述\n"
+"\n"
+"Lean 的简化器 `simp` 将它将用每个用户提供给它的引理\n"
+"以及所有标记为 `simp` 的引理重写目标。\n"
+"此外，如果提供了如`add_comm`这样的引理，它将尝试将对变量排序，以避免陷入无限循环。"
+
+#: Game.Levels.Algorithm.L03add_algo2
+msgid ""
+"\n"
+"Lean's simplifier, `simp`, is \"`rw` on steroids\". It will rewrite every lemma\n"
+"tagged with `simp` and every lemma fed to it by the user, as much as it can.\n"
+"\n"
+"This level is not a level which you want to solve by hand.\n"
+"Get the simplifier to solve it for you.\n"
+msgstr ""
+"\n"
+"Lean 的简化器 `simp` 是加强版的 `rw` 。它将用每个用户提供给它的引理\n"
+"以及所有标记为 `simp` 的引理重写目标。\n"
+"\n"
+"这个关卡不是能轻松手动解决的关卡。\n"
+"使用简化器来为解决这个问题。\n"
+
+#: Game.Levels.Algorithm.L03add_algo2 Game.Levels.Algorithm.L04add_algo3
+msgid ""
+"If $a, b,\\ldots h$ are arbitrary natural numbers, we have\n"
+"$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$."
+msgstr ""
+"如果 $a, b,\\ldots h$ 是任意自然数，我们有\n"
+"$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$。"
+
+#: Game.Levels.Algorithm.L03add_algo2
+msgid "Solve this level in one line with `simp only [add_assoc, add_left_comm, add_comm]`"
+msgstr "用 `simp only [add_assoc, add_left_comm, add_comm]` 在一行中证明这一关"
+
+#: Game.Levels.Algorithm.L03add_algo2
+msgid ""
+"\n"
+"Let's now make our own tactic to do this.\n"
+msgstr ""
+"\n"
+"现在让我们制定自己的策略来做到这一点。\n"
+
+#: Game.Levels.Algorithm.L04add_algo3
+msgid "the simplest approach"
+msgstr "最简单的方法"
+
+#: Game.Levels.Algorithm.L04add_algo3
+msgid ""
+"# Overview\n"
+"\n"
+"Our home-made tactic `simp_add` will solve arbitrary goals of\n"
+"the form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`."
+msgstr ""
+"＃ 概述\n"
+"\n"
+"我们自制的策略 `simp_add` 将解决以下形式的任意目标：\n"
+" `a + (b + c) + (d + e) = e + (d + (c + b)) + a`。"
+
+#: Game.Levels.Algorithm.L04add_algo3
+msgid ""
+"\n"
+"You can make your own tactics in Lean.\n"
+"This code here\n"
+"```\n"
+"macro \"simp_add\" : tactic => `(tactic|(\n"
+"  simp only [add_assoc, add_left_comm, add_comm]))\n"
+"```\n"
+"was used to create a new tactic `simp_add`, which runs\n"
+"`simp only [add_assoc, add_left_comm, add_comm]`.\n"
+"Try running `simp_add` to solve this level!\n"
+msgstr ""
+"\n"
+"你可以在 Lean 中创建自己的策略。\n"
+"这里的代码\n"
+"```\n"
+"macro \"simp_add\" : tactic => `(tactic|(\n"
+"  simp only [add_assoc, add_left_comm, add_comm]))\n"
+"```\n"
+"被用来创建一个新的策略 `simp_add`，它会执行\n"
+"`simp only [add_assoc, add_left_comm, add_comm]`。\n"
+"尝试运行 `simp_add` 来解决这个关卡！\n"
+
+#: Game.Levels.Algorithm.L04add_algo3
+msgid ""
+"\n"
+"Let's now move on to a more efficient approach to questions\n"
+"involving numerals, such as `20 + 20 = 40`.\n"
+msgstr ""
+"\n"
+"现在让我们转向更有效的\n"
+"涉及数字问题的方法，例如证明 `20 + 20 = 40`。\n"
+
+#: Game.Levels.Algorithm.L05pred
+msgid "pred"
+msgstr "pred"
+
+#: Game.Levels.Algorithm.L05pred
+msgid ""
+"\n"
+"We now start work on an algorithm to do addition more efficiently. Recall that\n"
+"we defined addition by recursion, saying what it did on `0` and successors.\n"
+"It is an axiom of Lean that recursion is a valid\n"
+"way to define functions from types such as the naturals.\n"
+"\n"
+"Let's define a new function `pred` from the naturals to the naturals, which\n"
+"attempts to subtract 1 from the input. The definition is this:\n"
+"\n"
+"```\n"
+"pred 0 := 37\n"
+"pred (succ n) := n\n"
+"```\n"
+"\n"
+"We cannot subtract one from 0, so we just return a junk value. As well as this\n"
+"definition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\n"
+"Let's use this lemma to prove `succ_inj`, the theorem which\n"
+"Peano assumed as an axiom and which we have already used extensively without justification.\n"
+msgstr ""
+"\n"
+"我们现在开始研究一个更高效进行加法计算的算法。回想一下，我们通过递归定义了加法，说明了它对 `0` 和后继者的作用。Lean 的一个公理是递归是从像自然数这样的类型定义函数的有效方式。\n"
+"\n"
+"让我们定义一个从自然数到自然数的新函数 `pred`，它试图从输入中减去 1。定义如下：\n"
+"\n"
+"```\n"
+"pred 0 := 37\n"
+"pred (succ n) := n\n"
+"```\n"
+"\n"
+"我们不能从 0 中减去 1，所以我们只是返回一个无用的值。除了这个定义之外，我们还创建了一个新的引理 `pred_succ`，它说 `pred (succ n) = n`。让我们使用这个引理来证明 `succ_inj`，这是皮亚诺假设为公理的定理，我们在没有证明它的情况下已经广泛使用了。\n"
+
+#: Game.Levels.Algorithm.L05pred
+msgid "`pred_succ n` is a proof of `pred (succ n) = n`."
+msgstr "`pred_succ n` 是 `pred (succ n) = n` 的证明。"
+
+#: Game.Levels.Algorithm.L05pred
+msgid "If $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ then $a=b$."
+msgstr "如果 $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ 那么 $a=b$。"
+
+#: Game.Levels.Algorithm.L05pred
+msgid "Start with `rw [← pred_succ a]` and take it from there."
+msgstr "从 `rw [← pred_succ a]` 开始，然后再继续。"
+
+#: Game.Levels.Algorithm.L05pred
+msgid ""
+"\n"
+"Nice! You've proved `succ_inj`!\n"
+"Let's now prove Peano's other axiom, that successors can't be $0$.\n"
+msgstr ""
+"\n"
+"好的！您已经证明了 `succ_inj`！\n"
+"现在让我们证明皮亚诺的另一个公理，后继数不可能是 $0$。\n"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid "is_zero"
+msgstr "is_zero"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid ""
+"\n"
+"We define a function `is_zero` thus:\n"
+"\n"
+"```\n"
+"is_zero 0 := True\n"
+"is_zero (succ n) := False\n"
+"```\n"
+"\n"
+"We also create two lemmas, `is_zero_zero` and `is_zero_succ n`, saying that `is_zero 0 = True`\n"
+"and `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`, Peano's\n"
+"Last Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have\n"
+"this opposite version too, which can be proved in the same way. Note: you can\n"
+"cheat here by using `zero_ne_succ` but the point of this world is to show\n"
+"you how to *prove* results like that.\n"
+"\n"
+"If you can turn your goal into `True`, then the `triv` tactic will solve it.\n"
+msgstr ""
+"\n"
+"我们这样定义一个函数 `is_zero` ：\n"
+"\n"
+"```\n"
+"is_zero 0 := True\n"
+"is_zero (succ n) := False\n"
+"```\n"
+"\n"
+"我们还创建两个引理 `is_zero_zero` 和 `is_zero_succ n`，表示 `is_zero 0 = True`\n"
+"和 `is_zero (succ n) = False`。让我们使用这些引理来证明 `succ_ne_zero`，Peano 的\n"
+"最后的公理。实际上，我们之前一直在使用 `zero_ne_succ`，但是有一个逆向的版本会很方便。\n"
+"它可以用同样的方式证明。注意：你可以\n"
+"通过使用 `zero_ne_succ` 在这里作弊，但这个世界的重点是展示\n"
+"你如何 *证明* 这样的结果。\n"
+"\n"
+"如果你能把你的目标变成`True`，那么`triv` 策略（tactic）就能解决它。\n"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid "`is_zero_zero` is a proof of `is_zero 0 = True`."
+msgstr "`is_zero_zero` 是 `is_zero 0 = True` 的证明。"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid "`is_zero_succ a` is a proof of `is_zero (succ a) = False`."
+msgstr "`is_zero_succ a` 是 `is_zero (succ a) = False` 的证明。"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid "`succ_ne_zero a` is a proof of `succ a ≠ 0`."
+msgstr "`succ_ne_zero a` 是 `succ a ≠ 0` 的证明。"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid ""
+"# Summary\n"
+"\n"
+"`triv` will solve the goal `True`."
+msgstr ""
+"＃ 小结\n"
+"\n"
+"`triv` 将解决目标 `True`。"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid ""
+"$\\operatorname{succ}(a) \n"
+"eq 0$."
+msgstr ""
+"$\\operatorname{succ}(a) \n"
+"eq 0$."
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid ""
+"Start with `intro h` (remembering that `X ≠ Y` is just notation\n"
+"for `X = Y → False`)."
+msgstr "从 `intro h` 开始（记住 `X ≠ Y` 只是 `X = Y → False` 的符号表示）。"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid ""
+"We're going to change that `False` into `True`. Start by changing it into\n"
+"`is_zero (succ a)` by executing `rw [← is_zero_succ a]`."
+msgstr "我们将要把那个 `False` 变成 `True`。首先通过执行 `rw [← is_zero_succ a]` 把它变成 `is_zero (succ a)`。"
+
+#: Game.Levels.Algorithm.L06is_zero
+msgid ""
+"See if you can take it from here. Look at the new lemmas and tactic\n"
+"available on the right."
+msgstr "看看你是否可以从这里开始。查看右侧可用的新引理和策略。"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid "An algorithm for equality"
+msgstr "用于证明等价的算法"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid ""
+"\n"
+"Here we begin to\n"
+"develop an algorithm which, given two naturals `a` and `b`, returns the answer\n"
+"to \"does `a = b`?\"\n"
+"\n"
+"Here is the algorithm. First note that `a` and `b` are numbers, and hence\n"
+"are either `0` or successors.\n"
+"\n"
+"*) If `a` and `b` are both `0`, return \"yes\".\n"
+"\n"
+"*) If one is `0` and the other is `succ n`, return \"no\".\n"
+"\n"
+"*) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"\n"
+"\n"
+"Our job now is to *prove* that this algorithm always gives the correct answer. The proof that\n"
+"`0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof\n"
+"that `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then\n"
+"`succ m = succ n` is `rw [h]` and then `rfl`. This level is a proof of the one\n"
+"remaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`.\n"
+msgstr ""
+"\n"
+"我们开始开发一个算法，给定两个自然数 `a` 和 `b`，返回对“`a = b`？”的回答。\n"
+"\n"
+"这是算法。首先注意到 `a` 和 `b` 是数字，因此要么是 `0` 要么是后继者。\n"
+"\n"
+"*) 如果 `a` 和 `b` 都是 `0`，返回“是”。\n"
+"\n"
+"*) 如果一个是 `0` 而另一个是 `succ n`，返回“否”。\n"
+"\n"
+"*) 如果 `a = succ m` 且 `b = succ n`，那么返回对“`m = n`？”的答案。\n"
+"\n"
+"现在我们的任务是*证明*这个算法总能给出正确的答案。证明 `0 = 0` 是 `rfl`。证明 `0 ≠ succ n` 的是 `zero_ne_succ n`，证明 `succ m ≠ 0` 的是 `succ_ne_zero m`。如果有假设 `h : m = n`，那么证明 `succ m = succ n` 可以使用 `rw [h]` 然后 `rfl`。这一关是证明我们要做的剩余工作之一：如果 `a ≠ b`，那么 `succ a ≠ succ b`。\n"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid ""
+"# Summary\n"
+"\n"
+"If you have a hypothesis\n"
+"\n"
+"`h : a ≠ b`\n"
+"\n"
+"and goal\n"
+"\n"
+"`c ≠ d`\n"
+"\n"
+"then `contrapose! h` replaces the set-up with its so-called \"contrapositive\":\n"
+"a hypothesis\n"
+"\n"
+"`h : c = d`\n"
+"\n"
+"and goal\n"
+"\n"
+"`a = b`."
+msgstr ""
+"# 小结\n"
+"\n"
+"如果你有一个假设\n"
+"\n"
+"`h : a ≠ b`\n"
+"\n"
+"和目标\n"
+"\n"
+"`c ≠ d`\n"
+"\n"
+"那么 `contrapose! h` 将这个命题替换为所谓的“逆否命题”：\n"
+"一个假设\n"
+"\n"
+"`h : c = d`\n"
+"\n"
+"和目标\n"
+"\n"
+"`a = b`。"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid "`succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`."
+msgstr "`succ_ne_succ m n` 是 `m ≠ n → succ m ≠ succ n` 的证明。"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid ""
+"If $a \n"
+"eq b$ then $\\operatorname{succ}(a) \n"
+"eq\\operatorname{succ}(b)$."
+msgstr ""
+"如果 $a \n"
+"eq b$，那么 $\\operatorname{succ}(a) \n"
+"eq\\operatorname{succ}(b)$。"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid ""
+"Start with `contrapose! h`, to change the goal into its\n"
+"contrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`."
+msgstr "从 `contrapose! h` 开始，将目标转变为其逆否命题，即假设为 `succ m = succ m`，目标为 `m = n`。"
+
+#: Game.Levels.Algorithm.L07succ_ne_succ
+msgid ""
+"Can you take it from here? (note: if you try `contrapose! h` again, it will\n"
+"take you back to where you started!)"
+msgstr "你能处理接下来的证明吗？（注意：如果你再次尝试 `contrapose! h`，它会把你带回到开始的地方！）"
+
+#: Game.Levels.Algorithm.L08decide
+msgid "decide"
+msgstr "decide"
+
+#: Game.Levels.Algorithm.L08decide
+msgid ""
+"# Summary\n"
+"\n"
+"`decide` will attempt to solve a goal if it can find an algorithm which it\n"
+"can run to solve it.\n"
+"\n"
+"## Example\n"
+"\n"
+"A term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\n"
+"are equal or different. Hence, once this term is made and made into an `instance`,\n"
+"the `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`."
+msgstr ""
+"# 小结\n"
+"\n"
+"如果 `decide` 可以找到一种算法来解决目标，它将尝试解决该目标。\n"
+"\n"
+"## 示例\n"
+"\n"
+"类型为 `DecidableEq ℕ` 的项是用于判断两个自然数是否相等或不同的算法（的实现函数）。\n"
+"因此，一旦这个项被创建并成为一个 `instance`，`decide` 策略就可以使用它来解决形式为 `a = b` 或 `a ≠ b` 的目标。"
+
+#: Game.Levels.Algorithm.L08decide
+msgid ""
+"\n"
+"Implementing the algorithm for equality of naturals, and the proof that it is correct,\n"
+"looks like this:\n"
+"\n"
+"```\n"
+"instance instDecidableEq : DecidableEq ℕ\n"
+"| 0, 0 => isTrue <| by\n"
+"  show 0 = 0\n"
+"  rfl\n"
+"| succ m, 0 => isFalse <| by\n"
+"  show succ m ≠ 0\n"
+"  exact succ_ne_zero m\n"
+"| 0, succ n => isFalse <| by\n"
+"  show 0 ≠ succ n\n"
+"  exact zero_ne_succ n\n"
+"| succ m, succ n =>\n"
+"  match instDecidableEq m n with\n"
+"  | isTrue (h : m = n) => isTrue <| by\n"
+"    show succ m = succ n\n"
+"    rw [h]\n"
+"    rfl\n"
+"  | isFalse (h : m ≠ n) => isFalse <| by\n"
+"    show succ m ≠ succ n\n"
+"    exact succ_ne_succ m n h\n"
+"```\n"
+"\n"
+"This Lean code is a formally verified algorithm for deciding equality\n"
+"between two naturals. I've typed it in already, behind the scenes.\n"
+"Because the algorithm is formally verified to be correct, we can\n"
+"use it in Lean proofs. You can run the algorithm with the `decide` tactic.\n"
+msgstr ""
+"\n"
+"实现自然数等式的算法，以及证明它是正确的，看起来像这样：\n"
+"\n"
+"```\n"
+"instance instDecidableEq : DecidableEq ℕ\n"
+"| 0, 0 => isTrue <| by\n"
+"  show 0 = 0\n"
+"  rfl\n"
+"| succ m, 0 => isFalse <| by\n"
+"  show succ m ≠ 0\n"
+"  exact succ_ne_zero m\n"
+"| 0, succ n => isFalse <| by\n"
+"  show 0 ≠ succ n\n"
+"  exact zero_ne_succ n\n"
+"| succ m, succ n =>\n"
+"  match instDecidableEq m n with\n"
+"  | isTrue (h : m = n) => isTrue <| by\n"
+"    show succ m = succ n\n"
+"    rw [h]\n"
+"    rfl\n"
+"  | isFalse (h : m ≠ n) => isFalse <| by\n"
+"    show succ m ≠ succ n\n"
+"    exact succ_ne_succ m n h\n"
+"```\n"
+"\n"
+"这段 Lean 代码是一个用于判断两个自然数之间等式的正式验证算法。\n"
+"我已经在游戏幕后输入了它。因为这个算法已经正式验证为正确，我们可以在 Lean 证明中使用它。\n"
+"你可以用 `decide` 策略运行这个算法。\n"
+
+#: Game.Levels.Algorithm.L08decide
+msgid "$20+20=40$."
+msgstr "$20+20=40$."
+
+#: Game.Levels.Algorithm.L08decide
+msgid ""
+"You can read more about the `decide` tactic by clicking\n"
+"on it in the top right."
+msgstr "你可以通过点击右上角的 `decide` 来了解更多关于 `decide` 策略的信息。"
+
+#: Game.Levels.Algorithm.L09decide2
+msgid "decide again"
+msgstr "还是`decide`"
+
+#: Game.Levels.Algorithm.L09decide2
+msgid ""
+"\n"
+"We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.\n"
+msgstr ""
+"\n"
+"我们前面给出的 `2 + 2 ≠ 5` 证明并不令人满意，现在给出一个更好的证明。\n"
+
+#: Game.Levels.Algorithm.L09decide2
+msgid ""
+"$2+2 \n"
+"eq 5.$"
+msgstr ""
+"$2+2 \n"
+"eq 5.$"
+
+#: Game.Levels.Algorithm.L09decide2
+msgid ""
+"Congratulations! You've finished Algorithm World. These algorithms\n"
+"will be helpful for you in Even-Odd World."
+msgstr ""
+"恭喜！您已经完成了《算法世界》。这些算法\n"
+"将对您在奇偶世界中有所帮助。"
+
+#: Game.Levels.Algorithm
+msgid "Algorithm World"
+msgstr "算法世界"
+
+#: Game.Levels.Algorithm
+msgid ""
+"\n"
+"Proofs like $2+2=4$ and $a+b+c+d+e=e+d+c+b+a$ are very tedious to do by hand.\n"
+"In Algorithm World we learn how to get the computer to do them for us.\n"
+"\n"
+"Click on \"Start\" to proceed.\n"
+msgstr ""
+"\n"
+"像 $2+2=4$ 和 $a+b+c+d+e=e+d+c+b+a$ 这样的证明如果手工完成会非常繁琐。在算法世界中，我们将学习如何让计算机帮我们完成它们。\n"
+"\n"
+"点击“开始”继续。\n"
+
+#: Game.Levels.AdvAddition.L01add_right_cancel
+msgid "add_right_cancel"
+msgstr "add_right_cancel"
+
+#: Game.Levels.AdvAddition.L01add_right_cancel
+msgid "`add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$"
+msgstr "`add_right_cancel a b n` 是 $a+n=b+n \\implies a=b$ 的定理。"
+
+#: Game.Levels.AdvAddition.L01add_right_cancel
+msgid ""
+"In this world I will mostly leave you on your own.\n"
+"\n"
+"`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$.\n"
+msgstr ""
+"在这个世界中，探险将主要由您独自完成。\n"
+"\n"
+"`add_right_cancel a b n` 是定理 $a+n=b+n\\implies a=b$。\n"
+
+#: Game.Levels.AdvAddition.L01add_right_cancel
+msgid "$a+n=b+n\\implies a=b$."
+msgstr "$a+n=b+n\\implies a=b$。"
+
+#: Game.Levels.AdvAddition.L01add_right_cancel
+msgid "Start with induction on `n`."
+msgstr "从对 `n` 的归纳开始。"
+
+#: Game.Levels.AdvAddition.L02add_left_cancel
+msgid "add_left_cancel"
+msgstr "add_left_cancel"
+
+#: Game.Levels.AdvAddition.L02add_left_cancel
+msgid "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$"
+msgstr "`add_left_cancel a b n` 是 $n+a=n+b \\implies a=b$ 的定理名字。"
+
+#: Game.Levels.AdvAddition.L02add_left_cancel
+msgid ""
+"`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.\n"
+"You can prove it by induction on `n` or you can deduce it from `add_right_cancel`.\n"
+msgstr "`add_left_cancel a b n` 是定理 $n+a=n+b\\implies a=b$。你可以通过对 `n` 进行归纳来证明它，或者你可以从 `add_right_cancel` 推导出它。\n"
+
+#: Game.Levels.AdvAddition.L02add_left_cancel
+msgid "$n+a=n+b\\implies a=b$."
+msgstr "$n+a=n+b\\implies a=b$ 。"
+
+#: Game.Levels.AdvAddition.L02add_left_cancel
+msgid ""
+"How about this for a proof:\n"
+"```\n"
+"repeat rw [add_comm n]\n"
+"exact add_right_cancel a b n\n"
+"```\n"
+msgstr ""
+"下面这个证明怎么样：\n"
+"```\n"
+"repeat rw [add_comm n]\n"
+"exact add_right_cancel a b n\n"
+"```\n"
+
+#: Game.Levels.AdvAddition.L03add_left_eq_self
+msgid "add_left_eq_self"
+msgstr "add_left_eq_self"
+
+#: Game.Levels.AdvAddition.L03add_left_eq_self
+msgid "`add_left_eq_self x y` is the theorem that $x + y = y \\implies x=0.$"
+msgstr "`add_left_eq_self x y` 是 $x + y = y\\implies x=0$ 的定理名字。"
+
+#: Game.Levels.AdvAddition.L03add_left_eq_self
+msgid ""
+"\n"
+"`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$\n"
+msgstr ""
+"\n"
+"`add_left_eq_self x y` 是 $x + y = y\\implies x=0$ 的定理名字。\n"
+
+#: Game.Levels.AdvAddition.L03add_left_eq_self
+msgid "$x + y = y\\implies x=0.$"
+msgstr "$x + y = y\\implies x=0$ 。"
+
+#: Game.Levels.AdvAddition.L03add_left_eq_self
+msgid ""
+"Did you use induction on `y`?\n"
+"Here's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\n"
+"If you want to inspect it, you can go into editor mode by clicking `</>` in the top right\n"
+"and then just cut and paste the proof and move your cursor around it\n"
+"to see the hypotheses and goal at any given point\n"
+"(although you'll lose your own proof this way). Click `>_` to get\n"
+"back to command line mode.\n"
+"```\n"
+"nth_rewrite 2 [← zero_add y]\n"
+"exact add_right_cancel x 0 y\n"
+"```\n"
+msgstr ""
+"你是否对 `y` 使用了归纳法？\n"
+"这里有一个使用 `add_right_cancel` 证明 `add_left_eq_self`的两行证明。如果你想查看它，你可以通过点击右上角的 `</>` 进入编辑器模式，然后只需剪切和粘贴证明，并在其周围移动你的光标，以查看在任何给定点的假设和目标（尽管这样做你会失去自己的证明）。点击 `>_` 返回命令行模式。\n"
+"```\n"
+"nth_rewrite 2 [← zero_add y]\n"
+"exact add_right_cancel x 0 y\n"
+"```\n"
+
+#: Game.Levels.AdvAddition.L04add_right_eq_self
+msgid "add_right_eq_self"
+msgstr "add_right_eq_self"
+
+#: Game.Levels.AdvAddition.L04add_right_eq_self
+msgid "`add_right_eq_self x y` is the theorem that $x + y = x \\implies y=0.$"
+msgstr "`add_right_eq_self x y` 是表示 $x + y = x\\implies y=0$ 的定理。"
+
+#: 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"
+"Two ways to do it spring to mind; I'll mention them when you've solved it.\n"
+msgstr ""
+"`add_right_eq_self x y` 是 $x + y = x\\implies y=0.$ 的定理。\n"
+"我想到了两种方法，等你解出来了我再提。\n"
+
+#: Game.Levels.AdvAddition.L04add_right_eq_self
+msgid "$x+y=x\\implies y=0$."
+msgstr "$x+y=x\\implies y=0$."
+
+#: Game.Levels.AdvAddition.L04add_right_eq_self
+msgid ""
+"Here's a proof using `add_left_eq_self`:\n"
+"```\n"
+"rw [add_comm]\n"
+"intro h\n"
+"apply add_left_eq_self at h\n"
+"exact h\n"
+"```\n"
+"\n"
+"and here's an even shorter one using the same idea:\n"
+"```\n"
+"rw [add_comm]\n"
+"exact add_left_eq_self y x\n"
+"```\n"
+"\n"
+"Alternatively you can just prove it by induction on `x`\n"
+"(the dots in the proof just indicate the two goals and\n"
+"can be omitted):\n"
+"\n"
+"```\n"
+"  induction x with d hd\n"
+"  · intro h\n"
+"    rw [zero_add] at h\n"
+"    assumption\n"
+"  · intro h\n"
+"    rw [succ_add] at h\n"
+"    apply succ_inj at h\n"
+"    apply hd at h\n"
+"    assumption\n"
+"```\n"
+msgstr ""
+"这里是使用 `add_left_eq_self` 的一个证明：\n"
+"```\n"
+"rw [add_comm]\n"
+"intro h\n"
+"apply add_left_eq_self at h\n"
+"exact h\n"
+"```\n"
+"\n"
+"这里是一个使用相同思路的更短的证明：\n"
+"```\n"
+"rw [add_comm]\n"
+"exact add_left_eq_self y x\n"
+"```\n"
+"\n"
+"或者，你也可以通过对 `x` 进行归纳来证明它\n"
+"（证明中的 `.` 只是表示两个目标，\n"
+"可以省略）：\n"
+"\n"
+"```\n"
+"  induction x with d hd\n"
+"  · intro h\n"
+"    rw [zero_add] at h\n"
+"    assumption\n"
+"  · intro h\n"
+"    rw [succ_add] at h\n"
+"    apply succ_inj at h\n"
+"    apply hd at h\n"
+"    assumption\n"
+"```\n"
+
+#: Game.Levels.AdvAddition.L05add_right_eq_zero
+msgid "add_right_eq_zero"
+msgstr "add_right_eq_zero"
+
+#: 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"
+"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"
+"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"
+"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.\n"
+"\n"
+msgstr ""
+"在这一关中，让我们证明其中一个事实，而在下一关证明另一个。\n"
+"\n"
+"## 一种新的策略：`cases`\n"
+"\n"
+"`cases` 策略会将一个对象或假设分解为可能的创建方式。\n"
+"\n"
+"例如，有时你想分别处理 `b = 0` 和 `b = succ d` 这两种情况，但不需要与 `induction b with d hd` 一起来的归纳假设 `hd`。在这种情况下，你可以使用 `cases b with d`。制造一个数字有两种方式：它要么是零，要么是后继者。所以你最终会得到两个目标，一个是 `b = 0`，另一个是 `b = succ d`。\n"
+"\n"
+"另一个例子：如果你有一个假设 `h : False`，那么你就完成证明了，因为从 `False` 可以推出任何声明。这里 `cases h` 将关闭目标，因为没有 *任何* 方法可以证明 `False`！所以你最终会没有目标，意味着你已经证明了一切。\n"
+
+#: Game.Levels.AdvAddition.L05add_right_eq_zero
+msgid ""
+"## Summary\n"
+"\n"
+"If `n` is a number, then `cases n with d` will break the goal into two goals,\n"
+"one with `n = 0` and the other with `n = succ d`.\n"
+"\n"
+"If `h` is a proof (for example a hypothesis), then `cases h with...` will break the\n"
+"proof up into the pieces used to prove it.\n"
+"\n"
+"## Example\n"
+"\n"
+"If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,\n"
+"one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This\n"
+"corresponds to the mathematical idea that every natural number is either `0`\n"
+"or a successor.\n"
+"\n"
+"## Example\n"
+"\n"
+"If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal\n"
+"into two goals, one with a hypothesis `hp : P` and the other with a\n"
+"hypothesis `hq : Q`.\n"
+"\n"
+"## Example\n"
+"\n"
+"If `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,\n"
+"because there are no ways to make a proof of `False`! And if you have no goals left,\n"
+"you have finished the level.\n"
+"\n"
+"## Example\n"
+"\n"
+"If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`\n"
+"and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is\n"
+"`∃ c, b = a + c`."
+msgstr ""
+"## 小结\n"
+"\n"
+"如果 `n` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n = 0`，另一个是 `n = succ d`。\n"
+"\n"
+"如果 `h` 是一个证明（例如一个假设），那么 `cases h with...` 会将证明分解成用来证明它的各个部分。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果 `n : ℕ` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n` 被替换为 0，另一个是 `n` 被替换为 `succ d`。这对应于数学上的观点，即每个自然数要么是 `0`，要么是一个后继数。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果 `h : P ∨ Q` 是一个假设，那么 `cases h with hp hq` 会将一个目标变成两个目标，一个有假设 `hp : P`，另一个有假设 `hq : Q`。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果 `h : False` 是一个假设，那么 `cases h` 会将一个目标变成没有目标，因为没有方法可以证明 `False`！如果你没有剩余的目标，你就完成了这个关卡。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果 `h : a ≤ b` 是一个假设，那么 `cases h with c hc` 会创建一个新的数字 `c` 和一个证明 `hc : b = a + c`。这是因为 `a ≤ b` 的*定义*是 `∃ c, b = a + c`。"
+
+#: Game.Levels.AdvAddition.L05add_right_eq_zero
+msgid "A proof that $a+b=0 \\implies a=0$."
+msgstr "一个 $a+b=0 \\implies a=0$ 的证明。"
+
+#: Game.Levels.AdvAddition.L05add_right_eq_zero
+msgid "If $a+b=0$ then $a=0$."
+msgstr "如果 $a+b=0$ 那么 $a=0$。"
+
+#: Game.Levels.AdvAddition.L05add_right_eq_zero
+msgid ""
+"Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,\n"
+"so start with `cases b with d`."
+msgstr ""
+"在这里，我们想要分别处理 `b = 0` 和 `b ≠ 0` 的情况，\n"
+"所以从 `cases b with d` 开始。"
+
+#: Game.Levels.AdvAddition.L05add_right_eq_zero
+msgid "Well done!"
+msgstr "做得好！"
+
+#: Game.Levels.AdvAddition.L06add_left_eq_zero
+msgid "add_left_eq_zero"
+msgstr "add_left_eq_zero"
+
+#: Game.Levels.AdvAddition.L06add_left_eq_zero
+msgid ""
+"You can just mimic the previous proof to do this one -- or you can figure out a way\n"
+"of using it.\n"
+msgstr ""
+"你可以模仿之前的证明来完成这个——或者你可以想出一种方法\n"
+"使用之前的证明。\n"
+
+#: Game.Levels.AdvAddition.L06add_left_eq_zero
+msgid "A proof that $a+b=0 \\implies b=0$."
+msgstr "一个$a+b=0 \\implies b=0$的证明。"
+
+#: Game.Levels.AdvAddition.L06add_left_eq_zero
+msgid "If $a+b=0$ then $b=0$."
+msgstr "如果 $a+b=0$ 那么 $b=0$。"
+
+#: Game.Levels.AdvAddition.L06add_left_eq_zero
+msgid ""
+"How about this for a proof:\n"
+"\n"
+"```\n"
+"rw [add_comm]\n"
+"exact add_right_eq_zero b a\n"
+"```\n"
+"\n"
+"That's the end of Advanced Addition World! You'll need these theorems\n"
+"for the next world, `≤` World. Click on \"Leave World\" to access it.\n"
+msgstr ""
+"这个证明怎么样：\n"
+"\n"
+"```\n"
+"rw [add_comm]\n"
+"exact add_right_eq_zero b a\n"
+"```\n"
+"\n"
+"这里就是高级加法世界的结尾了！你将带着这些定理\n"
+"进入下一个世界，`≤` 世界。点击“离开世界”来访问它。\n"
+
+#: Game.Levels.AdvAddition
+msgid "Advanced Addition World"
+msgstr "高级加法世界"
+
+#: Game.Levels.AdvAddition
+msgid ""
+"\n"
+"In Advanced Addition World we will prove some basic\n"
+"addition facts such as $x+y=x\\implies y=0$. The theorems\n"
+"proved in this world will be used to build\n"
+"a theory of inequalities in `≤` World.\n"
+"\n"
+"Click on \"Start\" to proceed.\n"
+msgstr ""
+"\n"
+"在高级加法世界中，我们将证明一些基本的加法事实，如 $x+y=x\\implies y=0$。在这个世界中证明的定理将被用来在 `≤` 世界中构建不等式理论。\n"
+"\n"
+"点击“开始”继续。\n"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid "The `use` tactic"
+msgstr "`use` 策略"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid ""
+"## Summary\n"
+"\n"
+"The `use` tactic makes progress with goals which claim something *exists*.\n"
+"If the goal claims that some `x` exists with some property, and you know\n"
+"that `x = 37` will work, then `use 37` will make progress.\n"
+"\n"
+"Because `a ≤ b` is notation for \"there exists `c` such that `b = a + c`\",\n"
+"you can make progress on goals of the form `a ≤ b` by `use`ing the\n"
+"number which is morally `b - a`."
+msgstr ""
+"## 小结\n"
+"\n"
+"`use` 策略能用在声称某些东西 *存在* 的目标上。\n"
+"如果目标声称某些 `x` 存在并具有某些属性，并且您知道\n"
+"`x = 37` 将起作用，那么使用 `use 37` 来改写目标。\n"
+"\n"
+"因为 `a ≤ b` 是用 “存在 `c` 使得 `b = a + c`” 定义的，\n"
+"所以可以通过`use (b - a)` 在 `a ≤ b` 形式的目标上取得进展。"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid ""
+"`a ≤ b` is *notation* for `∃ c, b = a + c`.\n"
+"\n"
+"Because this game doesn't have negative numbers, this definition\n"
+"is mathematically valid.\n"
+"\n"
+"This means that if you have a goal of the form `a ≤ b` you can\n"
+"make progress with the `use` tactic, and if you have a hypothesis\n"
+"`h : a ≤ b`, you can make progress with `cases h with c hc`."
+msgstr ""
+"`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。\n"
+"\n"
+"因为这个游戏没有负数，这个定义在数学上是有效的。\n"
+"\n"
+"这意味着如果你有一个形式为 `a ≤ b` 的目标，你可以用 `use` 策略来取得进展，如果你有一个假设 `h : a ≤ b`，你可以用 `cases h with c hc` 来取得进展。"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid ""
+"\n"
+"`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\n"
+"means \"there exists\". So `a ≤ b` means that there exists\n"
+"a number `c` such that `b = a + c`. This definition works\n"
+"because there are no negative numbers in this game.\n"
+"\n"
+"To *prove* an \"exists\" statement, use the `use` tactic.\n"
+"Let's see an example.\n"
+msgstr ""
+"\n"
+"`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。这个“倒 E”代表“存在”。所以 `a ≤ b` 意味着存在一个数字 `c` 使得 `b = a + c`。这个定义有效是因为在这个游戏中没有负数。\n"
+"\n"
+"要*证明*一个“存在”陈述，可以使用 `use` 策略。\n"
+"让我们看一个例子。\n"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid ""
+"`le_refl x` is a proof of `x ≤ x`.\n"
+"\n"
+"The reason for the name is that this lemma is \"reflexivity of $\\le$\""
+msgstr ""
+"`le_refl x` 是 `x ≤ x` 的证明。\n"
+"\n"
+"这个引理是 “$\\le$ 的自反性” 因此这么命名 。"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid "If $x$ is a number, then $x \\le x$."
+msgstr "如果 $x$ 是数字，那么 $x \\le x$。"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid ""
+"The reason `x ≤ x` is because `x = x + 0`.\n"
+"So you should start this proof with `use 0`."
+msgstr ""
+"之所以 `x ≤ x` 是因为 `x = x + 0`。\n"
+"所以你应该用 `use 0` 开始这个证明。"
+
+#: Game.Levels.LessOrEqual.L01le_refl
+msgid "You can probably take it from here."
+msgstr "你可以从这里开始。"
+
+#: Game.Levels.LessOrEqual.L02zero_le
+msgid "0 ≤ x"
+msgstr "0 ≤ x"
+
+#: Game.Levels.LessOrEqual.L02zero_le
+msgid ""
+"\n"
+"To solve this level, you need to `use` a number `c` such that `x = 0 + c`.\n"
+msgstr ""
+"\n"
+"要通过本关卡，您需要 `use` 一个数字 `c` 使得 `x = 0 + c`。\n"
+
+#: Game.Levels.LessOrEqual.L02zero_le
+msgid "`zero_le x` is a proof that `0 ≤ x`."
+msgstr "`zero_le x` 是 `0 ≤ x` 的证明。"
+
+#: Game.Levels.LessOrEqual.L02zero_le
+msgid "If $x$ is a number, then $0 \\le x$."
+msgstr "如果 $x$ 是自然数，则 $0 \\le x$。"
+
+#: Game.Levels.LessOrEqual.L03le_succ_self
+msgid "x ≤ succ x"
+msgstr "x ≤ succ x"
+
+#: Game.Levels.LessOrEqual.L03le_succ_self
+msgid "`le_succ_self x` is a proof that `x ≤ succ x`."
+msgstr "`le_succ_self x` 是 `x ≤ succ x` 的证明。"
+
+#: Game.Levels.LessOrEqual.L03le_succ_self
+msgid ""
+"If you `use` the wrong number, you get stuck with a goal you can't prove.\n"
+"What number will you `use` here?"
+msgstr ""
+"如果你使用错误的数字，你将卡在一个无法证明的目标中。\n"
+"你将在这里使用哪个数字？"
+
+#: Game.Levels.LessOrEqual.L03le_succ_self
+msgid "If $x$ is a number, then $x \\le \\operatorname{succ}(x)$."
+msgstr "如果 $x$ 是自然数，则 $x \\le \\operatorname{succ}(x)$。"
+
+#: Game.Levels.LessOrEqual.L03le_succ_self
+msgid ""
+"\n"
+"Here's a two-liner:\n"
+"```\n"
+"use 1\n"
+"exact succ_eq_add_one x\n"
+"```\n"
+"\n"
+"This works because `succ_eq_add_one x` is a proof of `succ x = x + 1`.\n"
+msgstr ""
+"\n"
+"这是两行的证明：\n"
+"```\n"
+"use 1\n"
+"exact succ_eq_add_one x\n"
+"```\n"
+"\n"
+"这是有效的，因为 `succ_eq_add_one x` 是 `succ x = x + 1` 的证明。\n"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid "x ≤ y and y ≤ z implies x ≤ z"
+msgstr "x ≤ y 且 y ≤ z 意味着 x ≤ z"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid ""
+"`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.\n"
+"More precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,\n"
+"If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.\n"
+"\n"
+"## A note on associativity\n"
+"\n"
+"In Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However\n"
+"`→` is right associative. This means that `x ≤ y → y ≤ z → x ≤ z` in Lean means\n"
+"exactly that `≤` is transitive. This is different to how mathematicians use\n"
+"$P \\implies Q \\implies R$; for them, this usually means that $P \\implies Q$\n"
+"and $Q \\implies R$."
+msgstr ""
+"`le_trans x y z` 证明了如果 `x ≤ y` 和 `y ≤ z` 那么 `x ≤ z`。\n"
+"更确切地说，它是 `x ≤ y → (y ≤ z → x ≤ z)` 的证明。换句话说\n"
+"If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.\n"
+"\n"
+"## 关于关联性的说明\n"
+"\n"
+"在 Lean 中，`a + b + c` 表示 `(a + b) + c`，因为 `+` 是左关联。但是\n"
+"`→` 是右关联式。这意味着Lean中的 `x ≤ y → y ≤ z → x ≤ z` 表示\n"
+"`≤` 是传递式的。这与数学家使用\n"
+"$P\\implies Q\\implies R$ 的用法不同；对他们来说，这通常意味着 $P\\implies Q$\n"
+"和 $Q\\implies R$。"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid ""
+"\n"
+"In this level, we see inequalities as *hypotheses*. We have not seen this before.\n"
+"The `cases` tactic can be used to take `hxy` apart.\n"
+msgstr ""
+"\n"
+"在本关，我们将不等视为 *假设* 。我们以前没有见过这个。\n"
+"`cases` 策略可用于拆解 `hxy` 假设。\n"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid "If $x \\leq y$ and $y \\leq z$, then $x \\leq z$."
+msgstr "如果 $x \\leq y$ 且 $y \\leq z$，那么 $x \\leq z$。"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid "Start with `cases hxy with a ha`."
+msgstr "从 `cases hxy with a ha` 开始。"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid ""
+"Now `ha` is a proof that `y = x + a`, and `hxy` has vanished. Similarly, you can destruct\n"
+"`hyz` into its parts with `cases hyz with b hb`."
+msgstr "现在 `ha` 是 `y = x + a` 的证明，而 `hxy` 已经消失了。同样，你可以通过 `cases hyz with b hb` 将 `hyz` 分解。"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid "Now you need to figure out which number to `use`. See if you can take it from here."
+msgstr "现在你需要弄清楚使用（ `use` ）哪个数字。看看你是否可以从这里继续。"
+
+#: Game.Levels.LessOrEqual.L04le_trans
+msgid ""
+"\n"
+"A passing mathematician remarks that with reflexivity and transitivity out of the way,\n"
+"you have proved that `≤` is a *preorder* on `ℕ`.\n"
+msgstr ""
+"\n"
+"一个路过的数学家指出，随着自反性和传递性的解决，你已经证明了 `≤` 是 `ℕ` 上的一个*预序*。\n"
+
+#: Game.Levels.LessOrEqual.L05le_zero
+msgid "x ≤ 0 → x = 0"
+msgstr "x ≤ 0 → x = 0"
+
+#: Game.Levels.LessOrEqual.L05le_zero
+msgid "`le_zero x` is a proof of `x ≤ 0 → x = 0`."
+msgstr "`le_zero x` 是 `x ≤ 0 → x = 0` 的证明。"
+
+#: Game.Levels.LessOrEqual.L05le_zero
+msgid ""
+"\n"
+"It's \"intuitively obvious\" that there are no numbers less than zero,\n"
+"but to prove it you will need a result which you showed in advanced\n"
+"addition world.\n"
+msgstr ""
+"\n"
+"没有小于零的数，这是 \"直觉上显而易见的\"、\n"
+"但是在高级加法世界要你需要证明这一点。\n"
+
+#: Game.Levels.LessOrEqual.L05le_zero
+msgid "`le_zero x` is a proof of the implication `x ≤ 0 → x = 0`."
+msgstr "`le_zero x` 是一个蕴含式 `x ≤ 0 → x = 0` 的证明。"
+
+#: Game.Levels.LessOrEqual.L05le_zero
+msgid "If $x \\leq 0$, then $x=0$."
+msgstr "如果是 $x \\leq 0$，那么 $x=0$。"
+
+#: Game.Levels.LessOrEqual.L05le_zero
+msgid ""
+"You want to use `add_right_eq_zero`, which you already\n"
+"proved, but you'll have to start with `symm at` your hypothesis."
+msgstr "你想使用 `add_right_eq_zero`，这是你已经证明过的，但你需要从对你的假设使用 `symm at` 开始。"
+
+#: Game.Levels.LessOrEqual.L06le_antisymm
+msgid "x ≤ y and y ≤ x implies x = y"
+msgstr "x ≤ y 且 y ≤ x 意味着 x = y"
+
+#: Game.Levels.LessOrEqual.L06le_antisymm
+msgid "`le_antisymm x y` is a proof that if `x ≤ y` and `y ≤ x` then `x = y`."
+msgstr "`le_antisymm x y` 是如果 `x ≤ y` 和 `y ≤ x` 则 `x = y` 的证明。"
+
+#: Game.Levels.LessOrEqual.L06le_antisymm
+msgid ""
+"\n"
+"This level asks you to prove *antisymmetry* of $\\leq$.\n"
+"In other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.\n"
+"It's the trickiest one so far. Good luck!\n"
+msgstr ""
+"\n"
+"这一关卡要求你证明 $\\leq$ 的 *反对称性* 。换句话说，如果 $x \\leq y$ 且 $y \\leq x$，那么 $x = y$。\n"
+"这是本游戏到目前最棘手的证明之一。祝你好运！\n"
+
+#: Game.Levels.LessOrEqual.L06le_antisymm
+msgid "If $x \\leq y$ and $y \\leq x$, then $x = y$."
+msgstr "如果 $x \\leq y$ 且 $y \\leq x$，则 $x = y$。"
+
+#: Game.Levels.LessOrEqual.L06le_antisymm
+msgid ""
+"\n"
+"Here's my proof:\n"
+"```\n"
+"cases hxy with a ha\n"
+"cases hyx with b hb\n"
+"rw [ha]\n"
+"rw [ha, add_assoc] at hb\n"
+"symm at hb\n"
+"apply add_right_eq_self at hb\n"
+"apply add_right_eq_zero at hb\n"
+"rw [hb, add_zero]\n"
+"rfl\n"
+"```\n"
+"\n"
+"A passing mathematician remarks that with antisymmetry as well,\n"
+"you have proved that `≤` is a *partial order* on `ℕ`.\n"
+"\n"
+"The boss level of this world is to prove\n"
+"that `≤` is a total order. Let's learn two more easy tactics\n"
+"first.\n"
+msgstr ""
+"\n"
+"这是我的证明：\n"
+"```\n"
+"cases hxy with a ha\n"
+"cases hyx with b hb\n"
+"rw [ha]\n"
+"rw [ha, add_assoc] at hb\n"
+"symm at hb\n"
+"apply add_right_eq_self at hb\n"
+"apply add_right_eq_zero at hb\n"
+"rw [hb, add_zero]\n"
+"rfl\n"
+"```\n"
+"\n"
+"\n"
+"一位路过的数学家评论说，你已经运用“反对称性”证明了 `≤` 在 `ℕ` 上是一个*偏序*。\n"
+"\n"
+"这个世界中的 Boss 关卡是证明 `≤` 是一个全序。我们先学习两个更简单的策略。\n"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid "Dealing with `or`"
+msgstr "处理 `or`"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid ""
+"# Summary\n"
+"The `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.\n"
+"Use it when your hypotheses guarantee that the reason that `P ∨ Q`\n"
+"is true is because in fact `P` is true.\n"
+"\n"
+"Internally this tactic is just `apply`ing a theorem\n"
+"saying that $P \\implies P \\lor Q.$\n"
+"\n"
+"Note that this tactic can turn a solvable goal into an unsolvable\n"
+"one."
+msgstr ""
+"# 小结\n"
+"`left` 策略将目标 `P ∨ Q` 转换为目标 `P`。当您的假设保证 `P ∨ Q` 为真的原因是由于 `P` 为真时，请使用它。\n"
+"\n"
+"在内部，这个策略只是应用了一个定理，该定理是 $P\\implies P\\lor Q$ 。\n"
+"\n"
+"请注意，此策略可能会将一个可解决的目标转换为不可解决的目标。"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid ""
+"# Summary\n"
+"The `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\n"
+"Use it when your hypotheses guarantee that the reason that `P ∨ Q`\n"
+"is true is because in fact `Q` is true.\n"
+"\n"
+"Internally this tactic is just `apply`ing a theorem\n"
+"saying that $Q \\implies P \\lor Q.$\n"
+"\n"
+"Note that this tactic can turn a solvable goal into an unsolvable\n"
+"one."
+msgstr ""
+"＃ 小结\n"
+"`right` 策略将 `P ∨ Q` 的目标更改为 `Q` 的目标。\n"
+"当您的假设`Q` 为真是 `P ∨ Q`为真的原因时使用它。\n"
+"\n"
+"在策略内部，它只是 `apply` （应用） 了 $Q \\implies P \\lor Q$ 这个定理\n"
+"\n"
+"请注意，这种策略可以将可解决的目标变成无法解决的目标。"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid ""
+"\n"
+"Totality of `≤` is the boss level of this world, and it's coming up next. It says that\n"
+"if `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.\n"
+"But we haven't talked about `or` at all. Here's a run-through.\n"
+"\n"
+"1) The notation for \"or\" is `∨`. You won't need to type it, but you can\n"
+"type it with `\\or`.\n"
+"\n"
+"2) If you have an \"or\" statement in the *goal*, then two tactics made\n"
+"progress: `left` and `right`. But don't choose a direction unless your\n"
+"hypotheses guarantee that it's the correct one.\n"
+"\n"
+"3) If you have an \"or\" statement as a *hypothesis* `h`, then\n"
+"`cases h with h1 h2` will create two goals, one where you went left,\n"
+"and the other where you went right.\n"
+msgstr ""
+"\n"
+"\"`≤`的完全性是这个世界的老大级别，接下来就是它了。它表明如果`a`和`b`是自然数，\n"
+"那么要么`a ≤ b`，要么`b ≤ a`。但我们根本没有讨论过`或`。这里有一个简要说明。\n"
+"\n"
+"1) “或”的符号是`∨`。你不需要直接打它，你可以用`\\or`来输入它。\n"
+"\n"
+"2) 如果你在 *目标* 中有一个“或”语句，那么有两个策略可以取得进展：`left`和`right`。\n"
+"但除非你的知道哪边是真的，否则不要选择一个方向。\n"
+"\n"
+"3) 如果你在 *假设* 中有一个“或”语句`h`，那么`cases h with h1 h2`会创建两个目标，一个假设左边是真的，另一个假设右边是真的。\n"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid "If $x=37$ or $y=42$, then $y=42$ or $x=37$."
+msgstr "如果 $x=37$ 或 $y=42$，那么 $y=42$ 或 $x=37$。"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid "We don't know whether to go left or right yet. So start with `cases h with hx hy`."
+msgstr "我们还不确定是向左还是向右。所以从 `cases h with hx hy` 开始。"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid ""
+"Now we can prove the `or` statement by proving the statement on the right,\n"
+"so use the `right` tactic."
+msgstr ""
+"现在我们可以通过证明右边的声明来证明 `or` 语句，\n"
+"所以使用 `right` 策略。"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid "This time, use the `left` tactic."
+msgstr "这一次，使用 `left` 策略。"
+
+#: Game.Levels.LessOrEqual.L07or_symm
+msgid ""
+"\n"
+"Ready for the boss level of this world?\n"
+msgstr ""
+"\n"
+"准备好迎接这个世界的Boss关了吗？\n"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "x ≤ y or y ≤ x"
+msgstr "x ≤ y 或 y ≤ x"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "`le_total x y` is a proof that `x ≤ y` or `y ≤ x`."
+msgstr "`le_total x y` 是 `x ≤ y` 或 `y ≤ x` 的证明。"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid ""
+"\n"
+"This is I think the toughest level yet. Tips: if `a` is a number\n"
+"then `cases a with b` will split into cases `a = 0` and `a = succ b`.\n"
+"And don't go left or right until your hypotheses guarantee that\n"
+"you can prove the resulting goal!\n"
+"\n"
+"I've left hidden hints; if you need them, retry from the beginning\n"
+"and click on \"Show more help!\"\n"
+msgstr ""
+"\n"
+"我认为这是迄今为止最难的关卡。提示：如果 `a` 是一个数字，那么 `cases a with b` 会分解为 `a = 0` 和 `a = succ b` 两种情况。不要在你的假设不能保证你能证明最终目标之前选择证明左边或右边！\n"
+"\n"
+"我留下了一些隐藏的提示；如果你需要，请从头开始重试并点击“显示更多帮助”！\n"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "If $x$ and $y$ are numbers, then either $x \\leq y$ or $y \\leq x$."
+msgstr "如果 $x$ 和 $y$ 是自然数，则 $x \\leq y$ 或 $y \\leq x$。"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "Start with `induction y with d hd`."
+msgstr "从`induction y with d hd`开始。"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "Try `cases hd with h1 h2`."
+msgstr "尝试 `cases hd with h1 h2`。"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "Now `cases h2 with e he`."
+msgstr "现在使用 `cases h2 with e he`。"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid "You still don't know which way to go, so do `cases e with a`."
+msgstr "你仍然不知道该走哪个分支，所以要做 `cases e with a`。"
+
+#: Game.Levels.LessOrEqual.L08le_total
+msgid ""
+"\n"
+"Very well done.\n"
+"\n"
+"A passing mathematician remarks that with you've just proved that `ℕ` is totally\n"
+"ordered.\n"
+"\n"
+"The final few levels in this world are much easier.\n"
+msgstr ""
+"\n"
+"太棒了！\n"
+"\n"
+"一位路过的数学家评论说，您刚刚证明了自然数集 `ℕ` 是全序的。\n"
+"\n"
+"剩下的关卡会更容易一些。\n"
+
+#: Game.Levels.LessOrEqual.L09succ_le_succ
+msgid "succ x ≤ succ y → x ≤ y"
+msgstr "succ x ≤ succ y → x ≤ y"
+
+#: Game.Levels.LessOrEqual.L09succ_le_succ
+msgid "`succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`."
+msgstr "`succ_le_succ x y` 是如果 `succ x ≤ succ y` 那么 `x ≤ y` 的证明。"
+
+#: Game.Levels.LessOrEqual.L09succ_le_succ
+msgid ""
+"\n"
+"We've proved that `x ≤ 0` implies `x = 0`. The last two levels\n"
+"in this world will prove which numbers are `≤ 1` and `≤ 2`.\n"
+"This lemma will be helpful for them.\n"
+msgstr ""
+"\n"
+"我们已经证明 `x ≤ 0` 蕴涵 `x = 0`。\n"
+"在这个世界的最后两关将证明哪些数字是 `≤ 1` 和 `≤ 2` 的。\n"
+"这个引理对证明它们将是有帮助的。\n"
+
+#: Game.Levels.LessOrEqual.L09succ_le_succ
+msgid "If $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ then $x \\leq y$."
+msgstr "如果 $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ 那么 $x \\leq y$。"
+
+#: Game.Levels.LessOrEqual.L09succ_le_succ
+msgid ""
+"\n"
+"Here's my proof:\n"
+"```\n"
+"cases hx with d hd\n"
+"use d\n"
+"rw [succ_add] at hd\n"
+"apply succ_inj at hd\n"
+"exact hd\n"
+"```\n"
+msgstr ""
+"\n"
+"这是一个证明（不唯一）：\n"
+"```\n"
+"cases hx with d hd\n"
+"use d\n"
+"rw [succ_add] at hd\n"
+"apply succ_inj at hd\n"
+"exact hd\n"
+"```\n"
+
+#: Game.Levels.LessOrEqual.L10le_one
+msgid "x ≤ 1"
+msgstr "x≤1"
+
+#: Game.Levels.LessOrEqual.L10le_one
+msgid "`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`."
+msgstr "`le_one x` 是“如果 `x ≤ 1` 那么 `x = 0` 或 `x = 1` ”的证明。"
+
+#: Game.Levels.LessOrEqual.L10le_one
+msgid ""
+"\n"
+"We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.\n"
+"Now we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`.\n"
+msgstr ""
+"\n"
+"我们已经看到了 `le_zero`，这是如果 `x ≤ 0` 那么 `x = 0` 的证明。\n"
+"现在我们将证明如果 `x ≤ 1` 那么 `x = 0` 或 `x = 1`。\n"
+
+#: Game.Levels.LessOrEqual.L10le_one
+msgid "If $x \\leq 1$ then either $x = 0$ or $x = 1$."
+msgstr "如果 $x \\leq 1$ 那么 $x = 0$ 或 $x = 1$。"
+
+#: Game.Levels.LessOrEqual.L10le_one
+msgid ""
+"\n"
+"Here's my proof:\n"
+"```\n"
+"cases x with y\n"
+"left\n"
+"rfl\n"
+"rw [one_eq_succ_zero] at hx ⊢\n"
+"apply succ_le_succ at hx\n"
+"apply le_zero at hx\n"
+"rw [hx]\n"
+"right\n"
+"rfl\n"
+"```\n"
+"\n"
+"If you solved this level then you should be fine with the next level!\n"
+msgstr ""
+"\n"
+"这是我的证明：\n"
+"```\n"
+"cases x with y\n"
+"left\n"
+"rfl\n"
+"rw [one_eq_succ_zero] at hx ⊢\n"
+"apply succ_le_succ at hx\n"
+"apply le_zero at hx\n"
+"rw [hx]\n"
+"right\n"
+"rfl\n"
+"```\n"
+"\n"
+"如果你解决了这个关卡，那么你应该可以顺利进入下一个关卡！\n"
+
+#: Game.Levels.LessOrEqual.L11le_two
+msgid "le_two"
+msgstr "le_two"
+
+#: Game.Levels.LessOrEqual.L11le_two
+msgid "`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`."
+msgstr "`le_two x` 证明了如果 `x ≤ 2` 则 `x = 0` 或 `x = 1` 或 `x = 2`。"
+
+#: Game.Levels.LessOrEqual.L11le_two
+msgid ""
+"\n"
+"We'll need this lemma to prove that two is prime!\n"
+"\n"
+"You'll need to know that `∨` is right associative. This means that\n"
+"`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`.\n"
+"This affects how `left` and `right` work.\n"
+msgstr ""
+"\n"
+"我们需要这个引理来证明二是质数！\n"
+"\n"
+"你需要知道 `∨` 是右结合的。这意味着 `x = 0 ∨ x = 1 ∨ x = 2` 实际上意味着 `x = 0 ∨ (x = 1 ∨ x = 2)`。这会影响 `left` 和 `right` 的工作方式。\n"
+
+#: Game.Levels.LessOrEqual.L11le_two
+msgid "If $x \\leq 2$ then $x = 0$ or $1$ or $2$."
+msgstr "如果是 $x \\leq 2$，那么 $x = 0$ 或 $1$ 或 $2$。"
+
+#: Game.Levels.LessOrEqual.L11le_two
+msgid ""
+"\n"
+"Nice!\n"
+"\n"
+"The next step in the development of order theory is to develop\n"
+"the theory of the interplay between `≤` and multiplication.\n"
+"If you've already done Multiplication World, you're now ready for\n"
+"Advanced Multiplication World. Click on \"Leave World\" to access it.\n"
+msgstr ""
+"\n"
+"很棒！\n"
+"\n"
+"发展序理论的下一步是发展 `≤` 与乘法之间相互作用的理论。\n"
+"如果你已经完成了乘法世界，那么就可以进入高级乘法世界。点击 \"离开世界 \"进入。\n"
+
+#: Game.Levels.LessOrEqual
+msgid "≤ World"
+msgstr "≤ 世界"
+
+#: Game.Levels.LessOrEqual
+msgid ""
+"\n"
+"In this world we define `a ≤ b` and prove standard facts\n"
+"about it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"\n"
+"\n"
+"The definition of `a ≤ b` is \"there exists a number `c`\n"
+"such that `b = a + c`. \" So we're going to have to learn\n"
+"a tactic to prove \"exists\" theorems, and another one\n"
+"to use \"exists\" hypotheses.\n"
+"\n"
+"Click on \"Start\" to proceed.\n"
+msgstr ""
+"\n"
+"在这个世界中，我们定义 `a ≤ b` 并证明关于它的一些事实，例如“如果 `a ≤ b` 且 `b ≤ c` 那么 `a ≤ c`。”\n"
+"\n"
+"`a ≤ b` 的定义是“存在一个数字 `c` 使得 `b = a + c`。”所以我们将不得不学习一种策略来证明“存在”定理，以及另一种策略来使用“存在”假设。\n"
+"\n"
+"点击“开始”继续。\n"
+
+#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
+msgid "mul_le_mul_right"
+msgstr "mul_le_mul_right"
+
+#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
+msgid "`mul_le_mul_right a b t` is a proof that `a ≤ b → a * t ≤ b * t`."
+msgstr "`mul_le_mul_right a b t` 是 `a ≤ b → a * t ≤ b * t` 的证明。"
+
+#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
+msgid "Let's warm up with an easy one, which works even if `t = 0`."
+msgstr "让我们用一个简单的问题来热热身，即使 `t = 0` 也可以。"
+
+#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
+msgid ""
+"My proof:\n"
+"```\n"
+"cases h with d hd\n"
+"use d * t\n"
+"rw [hd, add_mul]\n"
+"rfl\n"
+"```\n"
+msgstr ""
+"我的证明：\n"
+"```\n"
+"cases h with d hd\n"
+"use d * t\n"
+"rw [hd, add_mul]\n"
+"rfl\n"
+"```\n"
+"\n"
+
+#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+msgid "mul_left_ne_zero"
+msgstr "mul_left_ne_zero"
+
+#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+msgid "`mul_left_ne_zero a b` is a proof that `a * b ≠ 0 → b ≠ 0`."
+msgstr "`mul_left_ne_zero a b` 是`a * b ≠ 0 → b ≠ 0` 的证明。"
+
+#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+msgid ""
+"If you have completed Algorithm World then you can use the `contrapose!` tactic\n"
+"here. If not then I'll talk you through a manual approach."
+msgstr ""
+"如果你已经完成了算法世界，那么你可以在这里使用 `contrapose!` 策略。\n"
+"如果没有，那么我会指导你使用一种手动方法。"
+
+#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+msgid ""
+"We want to reduce this to a hypothesis `b = 0` and a goal `a * b = 0`,\n"
+"which is logically equivalent but much easier to prove. Remember that `X ≠ 0`\n"
+"is notation for `X = 0 → False`. Click on `Show more help!` if you need hints."
+msgstr ""
+"我们想将这个问题简化为假设 `b = 0` 和目标 `a * b = 0`，这在逻辑上是等价的，但更容易证明。\n"
+"记住，`X ≠ 0` 是 `X = 0 → False` 的符号表示。如果你需要提示，请点击`Show more help!`（显示更多帮助！）。"
+
+#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+msgid "Start with `intro hb`."
+msgstr "从 `intro hb` 开始。"
+
+#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+msgid "Now `apply h` and you can probably take it from here."
+msgstr "现在使用 `apply h`，你也许可以从这里开始证明。"
+
+#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+msgid "eq_succ_of_ne_zero"
+msgstr "eq_succ_of_ne_zero"
+
+#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+msgid ""
+"# Summary\n"
+"\n"
+"The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\n"
+"truth tables).\n"
+"\n"
+"## Example\n"
+"\n"
+"If you have `False` as a hypothesis, then `tauto` will solve\n"
+"the goal. This is because a false hypothesis implies any hypothesis.\n"
+"\n"
+"## Example\n"
+"\n"
+"If your goal is `True`, then `tauto` will solve the goal.\n"
+"\n"
+"## Example\n"
+"\n"
+"If you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\n"
+"solve the goal because it can prove `False` from your hypotheses, and thus\n"
+"prove the goal (as `False` implies anything).\n"
+"\n"
+"## Example\n"
+"\n"
+"If you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n"
+"`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n"
+"\n"
+"## Example\n"
+"\n"
+"If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n"
+"`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\n"
+"If you switch the goal and hypothesis in this example, `tauto` would solve it too."
+msgstr ""
+"# 小结\n"
+"\n"
+"`tauto` 策略将解决任何可以纯粹通过逻辑解决的目标（即，通过真值表）。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你有一个假设为 `False`，那么 `tauto` 将解决目标。这是因为一个假的假设意味着任何假设。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你的目标是 `True`，那么 `tauto` 将解决目标。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你有两个假设 `h1 : a = 37` 和 `h2 : a ≠ 37`，那么 `tauto` 将解决目标，因为它可以从你的假设中证明 `False`，从而证明目标（因为 `False` 意味着任何事情）。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你有一个假设 `h : a ≠ a`，那么 `tauto` 将解决目标，因为 `tauto` 足够聪明以知道 `a = a` 是真的，这提供了我们寻求的矛盾。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你有一个形式为 `a = 0 → a * b = 0` 的假设，而你的目标是 `a * b ≠ 0 → a ≠ 0`，那么 `tauto` 将解决目标，因为目标在逻辑上等同于假设。\n"
+"如果你在这个示例中交换目标和假设，`tauto` 也会解决它。\n"
+"如果你有两个假设 `h1 : a = 37` 和 `h2 : a ≠ 37` 那么 `tauto` 将解决目标\n"
+"就能解决这个目标，因为它能从你的假设中证明 `False`，从而\n"
+"证明目标（因为 `False` 意味着任何事情）。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你有一个假设 `h : a ≠ a` 那么 `tauto` 就能证明这个目标，因为\n"
+"`tauto` 足够聪明，知道 `a = a` 为真，这就给出了我们所寻求的矛盾。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你有一个形式为 `a = 0 → a * b = 0` 的假设，而你的目标是 `a * b ≠ 0 → a ≠ 0`，那么\n"
+"`tauto` 将证明目标，因为目标在逻辑上等同于假设。\n"
+"如果把这个例子中的目标和假设换一下，`tauto` 也会解决它。"
+
+#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+msgid "`eq_succ_of_ne_zero a` is a proof that `a ≠ 0 → ∃ n, a = succ n`."
+msgstr "`eq_succ_of_ne_zero a` 是 `a≠0 → ∃ n, a = succ n` 的证明。"
+
+#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+msgid ""
+"Multiplication usually makes a number bigger, but multiplication by zero can make\n"
+"it smaller. Thus many lemmas about inequalities and multiplication need the\n"
+"hypothesis `a ≠ 0`. Here is a key lemma enables us to use this hypothesis.\n"
+"To help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\n"
+"on the right to see what it does.\n"
+msgstr ""
+"乘法通常会使一个数字变大，但是乘以零可以使它变小。因此，关于不等式和乘法的许多引理需要假设 `a ≠ 0`。\n"
+"这里有一个关键的引理使我们能够使用这个假设。我们可以使用 `tauto` 策略帮助我们进行证明。点击右侧的策略名称查看它的作用。\n"
+
+#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+msgid "Start with `cases a with d` to do a case split on `a = 0` and `a = succ d`."
+msgstr "从用 `cases a with d` 开始，对 `a = 0` 和 `a = succ d` 进行类讨论。"
+
+#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+msgid ""
+"In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\n"
+"from a false statement. The `tauto` tactic will close this goal."
+msgstr "在“基础情形”中，我们有一个假设 `ha : 0 ≠ 0`，你可以从一个错误的声明中推导出任何东西。`tauto` 策略将关闭这个目标。"
+
+#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
+msgid "one_le_of_ne_zero"
+msgstr "one_le_of_ne_zero"
+
+#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
+msgid "`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`."
+msgstr "`one_le_of_ne_zero a` 是 `a≠0 → 1≤a` 的证明。"
+
+#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
+msgid "The previous lemma can be used to prove this one.\n"
+msgstr "先前的引理可以用来证明这个引理。\n"
+
+#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
+msgid "Use the previous lemma with `apply eq_succ_of_ne_zero at ha`."
+msgstr "通过`apply eq_succ_of_ne_zero at ha`来使用前面的引理。"
+
+#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
+msgid "Now take apart the existence statement with `cases ha with n hn`."
+msgstr "现在用 `cases ha with n hn` 分类讨论存在性声明。"
+
+#: Game.Levels.AdvMultiplication.L05le_mul_right
+msgid "le_mul_right"
+msgstr "le_mul_right"
+
+#: Game.Levels.AdvMultiplication.L05le_mul_right
+msgid ""
+"`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.\n"
+"\n"
+"It's one way of saying that a divisor of a positive number\n"
+"has to be at most that number."
+msgstr ""
+"`le_mul_right a b` 是 `a * b ≠ 0 → a ≤ a * b` 的证明。\n"
+"\n"
+"这是表达一个正数的除数不会大于这个数的一种方式。"
+
+#: Game.Levels.AdvMultiplication.L05le_mul_right
+msgid ""
+"\n"
+"In Prime Number World we will be proving that $2$ is prime.\n"
+"To do this, we will have to rule out things like $2 ≠ 37 × 42.$\n"
+"We will do this by proving that any factor of $2$ is at most $2$,\n"
+"which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n"
+"until it becomes the goal, using pretty much everything which we've proved in this world so far.\n"
+msgstr ""
+"\n"
+"在质数世界中，我们将证明 $2$ 是质数。为此，我们必须排除像 $2 ≠ 37 × 42$ 这样的情况。\n"
+"我们将通过证明 $2$ 的任何因数最多是 $2$ 来做到这一点，我们将使用这个引理来实现。\n"
+"我脑海中的证明会操作假设，直到它变成目标，几乎使用我们到目前为止在这个世界中已经证明的所有内容。\n"
+
+#: Game.Levels.AdvMultiplication.L05le_mul_right
+msgid ""
+"Here's what I was thinking of:\n"
+"```\n"
+"apply mul_left_ne_zero at h\n"
+"apply one_le_of_ne_zero at h\n"
+"apply mul_le_mul_right 1 b a at h\n"
+"rw [one_mul, mul_comm] at h\n"
+"exact h\n"
+"```\n"
+msgstr ""
+"我是这么想的：\n"
+"```\n"
+"apply mul_left_ne_zero at h\n"
+"apply one_le_of_ne_zero at h\n"
+"apply mul_le_mul_right 1 b a at h\n"
+"rw [one_mul, mul_comm] at h\n"
+"exact h\n"
+"```\n"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid "mul_right_eq_one"
+msgstr "mul_right_eq_one"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid ""
+"# Summary\n"
+"\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"
+"\n"
+"`have ha : a = 0`\n"
+"\n"
+"then you will get a new goal `a = 0` to prove, and after you've proved\n"
+"it you will have a new hypothesis `ha : a = 0` in your original goal.\n"
+"\n"
+"## Example\n"
+"\n"
+"If you already have a proof of what you want to `have`, you\n"
+"can just create it immediately. For example, if you have `a` and `b`\n"
+"number objects, then\n"
+"\n"
+"`have h2 : succ a = succ b → a = b := succ_inj a b`\n"
+"\n"
+"will directly add a new hypothesis `h2 : succ a = succ b → a = b`\n"
+"to the context, because you just supplied the proof of it (`succ_inj a b`).\n"
+"\n"
+"## Example\n"
+"\n"
+"If you have a proof to hand, then you don't even need to state what you\n"
+"are proving. example\n"
+"\n"
+"`have h2 := succ_inj a b`\n"
+"\n"
+"will add `h2 : succ a = succ b → a = b` as a hypothesis."
+msgstr ""
+"# 小结\n"
+"\n"
+"`have` 策略可以用来向一个层级添加新的假设，但当然，你必须证明它们。\n"
+"\n"
+"## 示例\n"
+"\n"
+"最简单的使用方式是这样的。如果你在你的上下文中有 `a` 并且你执行了\n"
+"\n"
+"`have ha : a = 0`\n"
+"\n"
+"那么你将得到一个新的目标 `a = 0` 来证明，一旦你证明了它，你将在你原始的目标中有一个新的假设 `ha : a = 0`。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你已经有了你想要 `have` 的证明，你可以立即创建它。例如，如果你有 `a` 和 `b` 这两个数字对象，那么\n"
+"\n"
+"`have h2 : succ a = succ b → a = b := succ_inj a b`\n"
+"\n"
+"将直接向上下文中添加一个新的假设 `h2 : succ a = succ b → a = b`，因为你刚刚提供了它的证明（`succ_inj a b`）。\n"
+"\n"
+"## 示例\n"
+"\n"
+"如果你手头有证明，那么你甚至不需要声明你在证明什么。例如\n"
+"\n"
+"`have h2 := succ_inj a b`\n"
+"\n"
+"将会添加假设 `h2 : succ a = succ b → a = b`。"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid "`mul_right_eq_one a b` is a proof that `a * b = 1 → a = 1`."
+msgstr "`mul_right_eq_one a b`证明了`a * b = 1 → a = 1`。"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid ""
+"\n"
+"This level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition\n"
+"World's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the\n"
+"lemma `le_one` from `≤` world.\n"
+"\n"
+"We'll prove it using a new and very useful tactic called `have`.\n"
+msgstr ""
+"\n"
+"在这个关卡，我们证明了 `x * y = 1 → x = 1`，这是高级加法世界中 `x + y = 0 → x = 0` 的乘法类比。策略是证明 `x ≤ 1`，然后使用来自 `≤` 世界的引理 `le_one`。\n"
+"\n"
+"我们将使用一个新的非常有用的策略叫做 `have` 来证明它。\n"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid ""
+"We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0`\n"
+"which we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\n"
+"e`).\n"
+"You'll be asked to\n"
+"prove it, and then you'll have a new hypothesis which you can apply\n"
+"`le_mul_right` to."
+msgstr ""
+"我们想使用 `le_mul_right`，但我们需要一个我们还没有的假设 `x * y ≠ 0`。\n"
+"现在执行 `have h2 : x * y ≠ 0`（你可以用 `\\ne` 输入 `≠`）。\n"
+"你将被要求证明它，然后你将有一个新的假设，你可以应用 `le_mul_right` 到这个假设上。"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid "Now you can `apply le_mul_right at h2`."
+msgstr "现在，您可以`apply le_mul_right at h2`。"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid "Now `rw [h] at h2` so you can `apply le_one at hx`."
+msgstr "现在`rw [h] at h2`，这样就可以`apply le_one at hx`。"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid ""
+"Now `cases h2 with h0 h1` and deal with the two\n"
+"cases separately."
+msgstr "现在使用 `cases h2 with h0 h1` a，并分类讨论这两种情况。"
+
+#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
+msgid "`tauto` is good enough to solve this goal."
+msgstr "`tauto` 足以证明这一目标。"
+
+#: Game.Levels.AdvMultiplication.L07mul_ne_zero
+msgid "mul_ne_zero"
+msgstr "mul_ne_zero"
+
+#: Game.Levels.AdvMultiplication.L07mul_ne_zero
+msgid "`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`."
+msgstr "`mul_ne_zero a b` 是如果 `a ≠ 0` 且 `b ≠ 0`，那么 `a * b ≠ 0`证明。"
+
+#: Game.Levels.AdvMultiplication.L07mul_ne_zero
+msgid ""
+"\n"
+"This level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy\n"
+"is to write both `a` and `b` as `succ` of something, deduce that `a * b` is\n"
+"also `succ` of something, and then `apply zero_ne_succ`.\n"
+msgstr ""
+"\n"
+"这个关卡要证明如果 `a ≠ 0` 且 `b ≠ 0`，那么 `a * b ≠ 0`。\n"
+"一种策略是将 `a` 和 `b` 都写成某物的 `succ`（后继），推断出 `a * b` 也是某物的 `succ`，然后应用 `zero_ne_succ`。\n"
+
+#: Game.Levels.AdvMultiplication.L07mul_ne_zero
+msgid "Start with `apply eq_succ_of_ne_zero at ha` and `... at hb`"
+msgstr "以`在 ha 处应用 eq_succ_of_ne_zero` 和`......在 hb` 开头"
+
+#: Game.Levels.AdvMultiplication.L08mul_eq_zero
+msgid "mul_eq_zero"
+msgstr "mul_eq_zero"
+
+#: Game.Levels.AdvMultiplication.L08mul_eq_zero
+msgid "`mul_eq_zero a b` is a proof that if `a * b = 0` then `a = 0` or `b = 0`."
+msgstr "`mul_eq_zero a b` 证明如果 `a * b = 0` 则 `a = 0` 或 `b = 0`。"
+
+#: Game.Levels.AdvMultiplication.L08mul_eq_zero
+msgid ""
+"\n"
+"This level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is\n"
+"logically equivalent to the last level, so there is a very short proof.\n"
+msgstr ""
+"\n"
+"这个关卡要证明如果 `a * b = 0` 那么 `a = 0` 或者 `b = 0`。这在逻辑上等同上一个关卡，所以有一个非常简短的证明。\n"
+
+#: Game.Levels.AdvMultiplication.L08mul_eq_zero
+msgid "Start with `have h2 := mul_ne_zero a b`."
+msgstr "从 `have h2 := mul_ne_zero a b` 开始。"
+
+#: Game.Levels.AdvMultiplication.L08mul_eq_zero
+msgid ""
+"Now the goal can be deduced from `h2` by pure logic, so use the `tauto`\n"
+"tactic."
+msgstr "现在，目标可以通过纯粹的逻辑从 `h2` 推导出来，所以使用 `tauto` 策略。"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid "mul_left_cancel"
+msgstr "mul_left_cancel"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid "`mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`."
+msgstr "`mul_left_cancel a b c` 证明了如果 `a ≠ 0` 且 `a * b = a * c` 则 `b = c` 。"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid ""
+"\n"
+"In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\n"
+"several reasons. One of these is that\n"
+"we need to introduce a new idea: we will need to understand the concept of\n"
+"mathematical induction a little better.\n"
+"\n"
+"Starting with `induction b with d hd` is too naive, because in the inductive step\n"
+"the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\n"
+"so the induction hypothesis does not apply!\n"
+"\n"
+"Assume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n"
+"\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,\n"
+"because we now have the flexibility to change `c`.\"\n"
+msgstr ""
+"\n"
+"在这个关卡中，我们证明了如果 `a * b = a * c` 且 `a ≠ 0` 那么 `b = c`。这是有些难的，因为几个原因。其中之一是我们需要引入一个新的想法：我们需要更好地理解数学归纳法的概念。\n"
+"\n"
+"从 `induction b with d hd` 开始太天真了，因为在归纳步骤中，假设是 `a * d = a * c → d = c`，但我们所知的是 `a * succ d = a * c`，所以归纳假设不适用！\n"
+"\n"
+"现在假设 `a ≠ 0` 是固定的。我们想要通过对 `b` 进行归纳来证明的实际声明是“对于所有的 `c`，如果 `a * b = a * c` 那么 `b = c`。这*可以*通过归纳来证明，因为我们现在有了改变 `c` 的灵活性。”\n"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid "The way to start this proof is `induction b with d hd generalizing c`."
+msgstr "开始证明的方法是 `induction b with d hd generalizing c`。"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid ""
+"Use `mul_eq_zero` and remember that `tauto` will solve a goal\n"
+"if there are hypotheses `a = 0` and `a ≠ 0`."
+msgstr "使用 `mul_eq_zero` 并记住，如果存在假设 `a = 0` 和 `a ≠ 0`，那么 `tauto` 将解决一个目标。"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid ""
+"The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\".\n"
+"You can `apply` it `at` any hypothesis of the form `a * d = a * ?`. "
+msgstr "归纳假设 `hd` 是“对于所有自然数 `c`，`a * d = a * c → d = c`”的证明。你可以在任何形式为 `a * d = a * ?` 的假设上应用（`apply`）它。"
+
+#: Game.Levels.AdvMultiplication.L09mul_left_cancel
+msgid "Split into cases `c = 0` and `c = succ e` with `cases c with e`."
+msgstr "用 `c cases c with e` 分成 `c = 0` 和 `c = succ e` 两种情况讨论。"
+
+#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
+msgid "mul_right_eq_self"
+msgstr "mul_right_eq_self"
+
+#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
+msgid "`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`."
+msgstr "`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`."
+
+#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
+msgid ""
+"The lemma proved in the final level of this world will be helpful\n"
+"in Divisibility World.\n"
+msgstr "在这个世界的最后一个层级证明的引理将在可除性世界中很有帮助。\n"
+
+#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
+msgid "Reduce to the previous lemma with `nth_rewrite 2 [← mul_one a] at h`"
+msgstr "使用 `nth_rewrite 2 [← mul_one a] at h` 将问题简化为之前的引理。"
+
+#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
+msgid "You can now `apply mul_left_cancel at h`"
+msgstr "现在您可以 `apply mul_left_cancel at h` 。"
+
+#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
+msgid ""
+"\n"
+"A two-line proof is\n"
+"\n"
+"```\n"
+"nth_rewrite 2 [← mul_one a] at h\n"
+"exact mul_left_cancel a b 1 ha h\n"
+"```\n"
+"\n"
+"We now have all the tools necessary to set up the basic theory of divisibility of naturals.\n"
+msgstr ""
+"\n"
+"这里有个两行的证明\n"
+"\n"
+"```\n"
+"nth_rewrite 2 [← mul_one a] at h\n"
+"exact mul_left_cancel a b 1 ha h\n"
+"```\n"
+"\n"
+"现在我们拥有了建立自然数可除性基本理论所需的所有工具。\n"
+
+#: Game.Levels.AdvMultiplication
+msgid "Advanced Multiplication World"
+msgstr "高级乘法世界"
+
+#: Game.Levels.AdvMultiplication
+msgid ""
+"\n"
+"Advanced *Addition* World proved various implications\n"
+"involving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\n"
+"These lemmas were used to prove basic facts about ≤ in ≤ World.\n"
+"\n"
+"In Advanced Multiplication World we prove analogous\n"
+"facts about multiplication, such as `x * y = 1 → x = 1`, and\n"
+"`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\n"
+"us for Divisibility World.\n"
+"\n"
+"Multiplication World is more complex than Addition World. In the same\n"
+"way, Advanced Multiplication world is more complex than Advanced Addition\n"
+"World. One reason for this is that certain intermediate results are only\n"
+"true under the additional hypothesis that one of the variables is non-zero.\n"
+"This causes some unexpected extra twists.\n"
+msgstr ""
+"\n"
+"高级 *加法* 世界证明了涉及加法的各种引理，例如 `x + y = 0 → x = 0` 和 `x + y = x → y = 0`。这些引理被用来证明 ≤ 世界中关于 ≤ 的基本事实。\n"
+"\n"
+"在高级乘法世界中，我们证明了关于乘法的类似事实，例如 `x * y = 1 → x = 1`，以及 `x * y = x → y = 1`（在后一个结果中假设 `x ≠ 0`）。这将为我们进入可除性世界做准备。\n"
+"\n"
+"乘法世界比加法世界更为复杂。同样，高级乘法世界比高级加法世界更为复杂。其中一个原因是某些中间结果只在额外假设下为真，即变量之一非零。这导致了一些意想不到的额外转折。\n"
+
+#: Game
+msgid "Natural Number Game"
+msgstr "自然数游戏"
+
+#: Game
+msgid ""
+"\n"
+"# 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"
+"numbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\n"
+"that `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\n"
+"And at the end we'll see if we can prove Fermat's Last Theorem.\n"
+"We'll do this by solving levels of a computer puzzle game called Lean.\n"
+"\n"
+"# Read this.\n"
+"\n"
+"Learning how to use an interactive theorem prover takes time.\n"
+"Tests show that the people who get the most out of this game are\n"
+"those who read the help texts like this one.\n"
+"\n"
+"To start, click on \"Tutorial World\".\n"
+"\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. A new version\n"
+"of Advanced Multiplication World is in preparation, and worlds\n"
+"such as Prime Number World and more will be appearing during October and\n"
+"November 2023.\n"
+"\n"
+"## More\n"
+"\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.\n"
+msgstr ""
+"\n"
+"# 欢迎来到自然数游戏\n"
+"#### 数学证明的入门。\n"
+"\n"
+"在这个游戏中，我们将从零开始构建自然数 `{0,1,2,3,4,...}` 的基本理论。我们的第一个目标是证明 `2 + 2 = 4`。接下来我们将证明 `x + y = y + x`。最后我们将看看我们是否能证明费马大定理。我们将通过解决一个名为 Lean 的计算机谜题游戏中的关卡来实现这一点。\n"
+"\n"
+"# 请阅读这个。\n"
+"\n"
+"学习如何使用交互式定理证明器需要时间。\n"
+"测试表明，最能从这个游戏中受益的人是那些像这样阅读帮助文本的人。\n"
+"\n"
+"开始，请点击“教程世界”。\n"
+"\n"
+"注意：这是游戏的新 Lean 4 版本，包含了老 Lean 3 版本中没有的几个世界。高级乘法世界的新版本正在准备中，像素数世界等更多世界将在 2023 年 10 月和 11 月期间出现。\n"
+"\n"
+"## 更多信息\n"
+"\n"
+"点击右上角的三条线，选择“游戏信息”来获取资源、链接，以及与 Lean 社区互动的方式。\n"
+
+#: Game
+msgid ""
+"\n"
+"*Game version: 4.2*\n"
+"\n"
+"*Recent additions: Inequality world, algorithm world*\n"
+"\n"
+"## Progress saving\n"
+"\n"
+"The game stores your progress in your local browser storage.\n"
+"If you delete it, your progress will be lost!\n"
+"\n"
+"Warning: In most browsers, deleting cookies will also clear the local storage\n"
+"(or \"local site data\"). Make sure to download your game progress first!\n"
+"\n"
+"## Credits\n"
+"\n"
+"* **Creators:** Kevin Buzzard, Jon Eugster\n"
+"* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n"
+"* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n"
+"* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n"
+"* **Additional thanks:** All the student beta testers, all the schools\n"
+"who invited Kevin to speak, and all the schoolkids who asked him questions\n"
+"about the material.\n"
+"\n"
+"## Resources\n"
+"\n"
+"* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n"
+"* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n"
+"\n"
+"## Problems?\n"
+"\n"
+"Please ask any questions about this game in the\n"
+"[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\n"
+"the stream \"New Members\". The community will happily help. Note that\n"
+"the Lean Zulip chat is a professional research forum.\n"
+"Please use your full real name there, stay on topic, and be nice. If you're\n"
+"looking for somewhere less formal (e.g. you want to post natural number\n"
+"game memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n"
+"\n"
+"Alternatively, if you experience issues / bugs you can also open github issues:\n"
+"\n"
+"* For issues with the game engine, please open an\n"
+"[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n"
+"* For issues about the game's content, please open an\n"
+"[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.\n"
+"\n"
+msgstr ""
+"\n"
+"*游戏版本：4.2*\n"
+"\n"
+"*最近新增：不等式世界，算法世界*\n"
+"\n"
+"## 进度保存\n"
+"\n"
+"游戏会将你的进度存储在本地浏览器存储中。\n"
+"如果你删除它，你的进度将会丢失！\n"
+"\n"
+"警告：在大多数浏览器中，删除 cookie 也会清除本地存储（或“本地网站数据”）。确保首先下载你的游戏进度！\n"
+"\n"
+"## 致谢\n"
+"\n"
+"* **创建者：** Kevin Buzzard, Jon Eugster\n"
+"* **原始 Lean3 版本：** Kevin Buzzard, Mohammad Pedramfar\n"
+"* **游戏引擎：** Alexander Bentkamp, Jon Eugster, Patrick Massot\n"
+"* **额外关卡：** Sian Carey, Ivan Farabella, Archie Browne.\n"
+"* **特别感谢：** 所有学生测试者，所有邀请 Kevin 发表演讲的学校，以及向他提出关于材料问题的所有学生。\n"
+"\n"
+"## 资源\n"
+"\n"
+"* [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛\n"
+"* [原始 Lean3 版本](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)（不再维护）\n"
+"\n"
+"## 有问题吗？\n"
+"\n"
+"请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新成员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使用您的全名，保持话题相关，且友好。如果你正在寻找一个不那么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean Discord](https://discord.gg/WZ9bs9UCvx)。\n"
+"\n"
+"另外，如果你遇到问题/漏洞，你也可以在 github 上提出问题：\n"
+"\n"
+"* 对于游戏引擎的问题，请在 [lean4game](https://github.com/leanprover-community/lean4game/issues) 仓库提出问题。\n"
+"* 对于游戏内容的问题，请在 [NNG](https://github.com/hhu-adam/NNG4/issues) 仓库提出问题。\n"
+
+#: Game
+msgid "The classical introduction game for Lean."
+msgstr "经典的Lean入门游戏。"
+
+#: Game
+msgid ""
+"In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\n"
+"learning the basics about theorem proving in Lean.\n"
+"\n"
+"This is a good first introduction to Lean!"
+msgstr ""
+"在这个游戏中，你将根据皮亚诺公理重新构建自然数集 $\\mathbb{N}$，学习在 Lean 中证明定理的基础知识。\n"
+"\n"
+"这是对 Lean 的一个很好的初步介绍！"