diff --git a/.i18n/zh/Game.json b/.i18n/zh/Game.json
index 7ea0654..dff47b0 100644
--- a/.i18n/zh/Game.json
+++ b/.i18n/zh/Game.json
@@ -186,7 +186,7 @@
  "`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$":
  "`add_sq a b` 是 $(a+b)^2=a^2+b^2+2ab$ 的证明。",
  "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\nTwo ways to do it spring to mind; I'll mention them when you've solved it.":
- "`add_right_eq_self x y` 是 $x + y = x\\implies y=0.$ 的定理。\n我想到了两种方法，等你解出来了我再提。",
+ "`add_right_eq_self x y` 是 $x + y = x\\implies y=0$ 的定理。我想到了两种方法，等你解出来了我再提。",
  "`add_right_eq_self x y` is the theorem that $x + y = x \\implies y=0.$":
  "`add_right_eq_self x y` 是表示 $x + y = x\\implies y=0$ 的定理。",
  "`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n\nIn Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\nas `a + b + c = a + c + b`.":
@@ -290,7 +290,7 @@
  "We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0`\nwhich we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\\ne`).\nYou'll be asked to\nprove it, and then you'll have a new hypothesis which you can apply\n`le_mul_right` to.":
  "我们想使用 `le_mul_right`，但我们需要一个我们还没有的假设 `x * y ≠ 0`。\n现在执行 `have h2 : x * y ≠ 0`（你可以用 `\\ne` 输入 `≠`）。\n你将被要求证明它，然后你将有一个新的假设，你可以应用 `le_mul_right` 到这个假设上。",
  "We want to reduce this to a hypothesis `b = 0` and a goal `a * b = 0`,\nwhich is logically equivalent but much easier to prove. Remember that `X ≠ 0`\nis notation for `X = 0 → False`. Click on `Show more help!` if you need hints.":
- "我们想将这个问题简化为假设 `b = 0` 和目标 `a * b = 0`，这在逻辑上是等价的，但更容易证明。\n记住，`X ≠ 0` 是 `X = 0 → False` 的符号表示。如果你需要提示，请点击`Show more help!`（显示更多帮助！）。",
+ "我们想将这个问题简化为假设 `b = 0` 和目标 `a * b = 0`，这在逻辑上是等价的，但更容易证明。\n记住，`x ≠ 0` 是 `x = 0 → False` 的符号表示。如果你需要提示，请点击`显示更多帮助！`。",
  "We still can't prove `2 + 2 ≠ 5` because we have not talked about the\ndefinition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.\nHere `False` is a generic false proposition, and `→` is Lean's notation\nfor \"implies\". In logic we learn\nthat `True → False` is false, but `False → False` is true. Hence\n`X → False` is the logical opposite of `X`.\n\nEven though `a ≠ b` does not look like an implication,\nyou 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!\nSo if your goal is `False` then you had better hope that your hypotheses\nare contradictory, which they are in this level.":
  "我们仍然不能证明 `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`，那么你最好希望你的假设是矛盾的，就像在本关中一样。",
  "We now start work on an algorithm to do addition more efficiently. Recall that\nwe defined addition by recursion, saying what it did on `0` and successors.\nIt is an axiom of Lean that recursion is a valid\nway to define functions from types such as the naturals.\n\nLet's define a new function `pred` from the naturals to the naturals, which\nattempts to subtract 1 from the input. The definition is this:\n\n```\npred 0 := 37\npred (succ n) := n\n```\n\nWe cannot subtract one from 0, so we just return a junk value. As well as this\ndefinition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\nLet's use this lemma to prove `succ_inj`, the theorem which\nPeano assumed as an axiom and which we have already used extensively without justification.":
@@ -322,7 +322,7 @@
  "Try `rw [add_zero c]`.": "尝试使用 `rw [add_zero c]`。",
  "Try `cases «{hd}» with h1 h2`.": "尝试 `cases «{hd}» with h1 h2`。",
  "Totality of `≤` is the boss level of this world, and it's coming up next. It says that\nif `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.\nBut we haven't talked about `or` at all. Here's a run-through.\n\n1) The notation for \"or\" is `∨`. You won't need to type it, but you can\ntype it with `\\or`.\n\n2) If you have an \"or\" statement in the *goal*, then two tactics made\nprogress: `left` and `right`. But don't choose a direction unless your\nhypotheses guarantee that it's the correct one.\n\n3) 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,\nand the other where you went right.":
- "\"`≤`的完全性是这个世界的老大级别，接下来就是它了。它表明如果`a`和`b`是自然数，\n那么要么`a ≤ b`，要么`b ≤ a`。但我们根本没有讨论过`或`。这里有一个简要说明。\n\n1) “或”的符号是`∨`。你不需要直接打它，你可以用`\\or`来输入它。\n\n2) 如果你的 *目标* 是一个“或”命题，那么有两个策略可以取得进展：`left`和`right`。\n但除非你的知道哪边是真的，否则不要选择一个方向。\n\n3) 如果你在 *假设* 中有一个“或”命题`h`，那么`cases h with h1 h2`会创建两个目标，一个假设左边是真的，另一个假设右边是真的。",
+ "`≤`的完全性是这个世界的Boss关卡了，接下来就是它了。它表明如果`a`和`b`是自然数，\n那么`a ≤ b`或`b ≤ a`。但我们根本没有讨论过“或”（`or`）。这里有一个简要说明。\n\n1. “或”的符号是`∨`，你可以用`\\or`来输入它。\n2. 如果你的 *目标* 是一个“或”命题，那么有两个策略可以取得进展：`left`和`right`。\n但除非你的知道哪边是真的，否则不要选择一个方向。\n3. 如果你在 *假设* 中有一个“或”命题`h`，那么`cases h with h1 h2`会创建两个目标，一个假设左边是真的，另一个假设右边是真的。",
  "To solve this level, you need to `use` a number `c` such that `x = 0 + c`.":
  "要通过本关卡，您需要 `use` 一个数字 `c` 使得 `x = 0 + c`。",
  "Those of you interested in speedrunning the game may want to know\nthat `repeat rw [add_zero]` will do both rewrites at once.":
@@ -750,7 +750,7 @@
  "Advanced Multiplication World": "高级乘法世界",
  "Advanced Addition World": "高级加法世界",
  "Advanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts 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\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.":
- "高级 *加法* 世界证明了涉及加法的各种引理，例如 `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乘法世界比加法世界更为复杂。同样，高级乘法世界比高级加法世界更为复杂。其中一个原因是某些中间结果只在额外假设下为真，即变量之一非零。这导致了一些意想不到的额外转折。",
+ "高级 *加法* 世界证明了涉及加法的各种引理，例如 `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乘法世界比加法世界更为复杂。同样，高级乘法世界比高级加法世界更为复杂。其中一个原因是某些中间结果只在额外假设下为真，即变量之一非零。这导致了一些意想不到的转折。",
  "Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
  "加法和乘法有分配律。换句话说，对于所有自然数 $a$、$b$ 和 $c$，\n我们有 $(a + b) \\times c = ac + bc$。",
  "Addition World": "加法世界",
@@ -824,11 +824,11 @@
  "# Summary\nThe `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `P` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $P \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.":
  "## 概述\n`left` 策略将目标 `P ∨ Q` 转换为目标 `P`。当您的假设保证 `P ∨ Q` 为真的原因是由于 `P` 为真时，请使用它。\n\n在内部，这个策略只是应用了一个定理，该定理是 $P\\implies P\\lor Q$ 。\n\n请注意，此策略可能会将一个可解决的目标转换为不可解决的目标。",
  "# Summary\n\n`trivial` will solve the goal `True`.":
- "＃ 小结\n\n`trivial` 将解决目标 `True`。",
+ "## 概述\n\n`trivial` 将解决目标 `True`。",
  "# Summary\n\n`decide` will attempt to solve a goal if it can find an algorithm which it\ncan run to solve it.\n\n## Example\n\nA term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\nare equal or different. Hence, once this term is made and made into an `instance`,\nthe `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.":
- "# 小结\n\n如果 `decide` 可以找到一种算法来解决目标，它将尝试解决该目标。\n\n## 示例\n\n类型为 `DecidableEq ℕ` 的项是用于判断两个自然数是否相等或不同的算法（的实现函数）。\n因此，一旦这个项被创建并成为一个 `instance`，`decide` 策略就可以使用它来解决形式为 `a = b` 或 `a ≠ b` 的目标。",
+ "## 概述\n\n如果 `decide` 可以找到一种算法来解决目标，它将尝试解决该目标。\n\n### 示例\n\n类型为 `DecidableEq ℕ` 的项是用于判断两个自然数是否相等或不同的算法（的实现函数）。\n因此，一旦这个项被创建并成为一个 `instance`，`decide` 策略就可以使用它来解决形式为 `a = b` 或 `a ≠ b` 的目标。",
  "# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf 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\nIf 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.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.":
- "## 概述\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` 也会解决它。",
+ "## 概述\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` 也会解决它。",
  "# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.":
  "# 小结\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`。",
  "# Summary\n\nIf you have a hypothesis\n\n`h : a ≠ b`\n\nand goal\n\n`c ≠ d`\n\nthen `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\na hypothesis\n\n`h : c = d`\n\nand goal\n\n`a = b`.":
@@ -838,6 +838,6 @@
  "# Read this first\n\nEach level in this game involves proving a mathematical theorem (the \"Goal\").\nThe goal will be a statement about *numbers*. Some numbers in this game have known values.\nThose numbers have names like $37$. Other numbers will be secret. They're called things\nlike $x$ and $q$. We know $x$ is a number, we just don't know which one.\n\nIn this first level we're going to prove the theorem that $37x + q = 37x + q$.\nYou can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`\nare numbers.\n\nWe solve goals in Lean using *Tactics*, and the first tactic we're\ngoing to learn is called `rfl`, which proves all theorems of the form $X = X$.\n\nProve that $37x+q=37x+q$ by executing the `rfl` tactic.":
  "# 游戏指南\n\n在这个游戏的每个关卡中，你都将挑战证明一个数学定理，这里称之为“目标”。这些目标主要与*自然数*相关。游戏中，一些数具有明确的值，例如 $37$ 这类具体的数。然而，还有一些数是未知数，它们被称为 $x$、$q$ 等。虽然我们不知道 $x$ 的具体值，但我们知道它代表一个自然数。\n\n在游戏的第一关，我们的任务是证明定理 $37x + q = 37x + q$。你将在下方的*对象*中看到 `x q : ℕ`，这表示 `x` 和 `q` 都是自然数。\n\n为了在 Lean 中证明这些目标，我们将学习和使用各种*策略*。首先介绍的策略是 `rfl`，它用于证明所有形式为 $X = X$ 的定理。\n\n要证明 $37x+q=37x+q$，请使用 `rfl` 策略。",
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
- "＃ 概述\n\n我们自制的策略 `simp_add` 将解决以下形式的任意目标：\n `a + (b + c) + (d + e) = e + (d + (c + b)) + a`。",
+ "## 概述\n\n我们自制的策略 `simp_add` 将解决以下形式的任意目标：\n `a + (b + c) + (d + e) = e + (d + (c + b)) + a`。",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
  "## 概述\n\nLean 的简化器 `simp` 将它将用每个用户提供给它的引理\n以及所有标记为 `simp` 的引理重写目标。\n此外，如果提供了如`add_comm`这样的引理，它将尝试将对变量排序，以避免陷入无限循环。"}
\ No newline at end of file
diff --git a/.i18n/zh/Game.po b/.i18n/zh/Game.po
index 52db5d7..9f1e228 100644
--- a/.i18n/zh/Game.po
+++ b/.i18n/zh/Game.po
@@ -94,9 +94,9 @@ msgstr ""
 "*请注意，出于教学目的，我们的 `rfl` 比核心 Lean 和 `mathlib` 中使用的版本弱一些；数学家不区分命题等价"
 "和定义等价，因为他们以不同于类型理论家的方式思考定义（就数学家而言，`zero_add` 和 `add_zero` 都是 “事"
 "实”，谁会在乎加法的定义是什么呢）。*\n"
-"（译注：因为 `add_zero` 是加法定义的一部分，而定义等价是可以直接用 `rfl` 证明的。也就是说 `x + 0 = x` "
-"可以用 `rfl` 证明。所以作者多了一嘴，但实际上因为很少有人知道类型理论家怎么思考，所以这个注解看起来会"
-"有些奇怪。）"
+"（译注：因为 `add_zero` 是加法定义的一部分，而定义等价是可以直接用 `rfl` 证明的。也就是说 `x + 0 = "
+"x` 可以用 `rfl` 证明。所以作者多了一嘴，但实际上因为很少有人知道类型理论家怎么思考，所以这个注解看起"
+"来会有些奇怪。）"
 
 #: Game.Levels.Tutorial.L01rfl
 msgid ""
@@ -118,9 +118,9 @@ msgid ""
 msgstr ""
 "# 游戏指南\n"
 "\n"
-"在这个游戏的每个关卡中，你都将挑战证明一个数学定理，这里称之为“目标”。这些目标主要与*自然数*相关。游戏"
-"中，一些数具有明确的值，例如 $37$ 这类具体的数。然而，还有一些数是未知数，它们被称为 $x$、$q$ 等。虽然"
-"我们不知道 $x$ 的具体值，但我们知道它代表一个自然数。\n"
+"在这个游戏的每个关卡中，你都将挑战证明一个数学定理，这里称之为“目标”。这些目标主要与*自然数*相关。游"
+"戏中，一些数具有明确的值，例如 $37$ 这类具体的数。然而，还有一些数是未知数，它们被称为 $x$、$q$ 等。"
+"虽然我们不知道 $x$ 的具体值，但我们知道它代表一个自然数。\n"
 "\n"
 "在游戏的第一关，我们的任务是证明定理 $37x + q = 37x + q$。你将在下方的*对象*中看到 `x q : ℕ`，这表示 "
 "`x` 和 `q` 都是自然数。\n"
@@ -151,8 +151,8 @@ msgid ""
 msgstr ""
 "恭喜你！你已经完成了第一个证明！\n"
 "\n"
-"请记得，`rfl` 是一种*策略*。如果你对 `rfl` 策略有更多的兴趣想要深入了解，可以尝试点击右侧策略列表中的 "
-"`rfl` 查看详情。\n"
+"请记得，`rfl` 是一种*策略*。如果你对 `rfl` 策略有更多的兴趣想要深入了解，可以尝试点击右侧策略列表中"
+"的 `rfl` 查看详情。\n"
 "\n"
 "现在，请点击“下一关”，继续学习 `rw`（重写）策略。"
 
@@ -315,15 +315,15 @@ msgstr ""
 "\n"
 "`rw` 策略是一种进行“代入”的方式。有两种不同的情况你可以使用这个策略。\n"
 "\n"
-"1) 基本使用：如果 `h : A = B` 是一个假设或定理的证明，并且目标中包含一个或多个 `A`，那么 `rw [h]` 会把"
-"它们全部改为 `B`。如果目标中没有 `A`，策略会报错。\n"
+"1) 基本使用：如果 `h : A = B` 是一个假设或定理的证明，并且目标中包含一个或多个 `A`，那么 `rw [h]` 会"
+"把它们全部改为 `B`。如果目标中没有 `A`，策略会报错。\n"
 "\n"
 "2) 高级使用：来自定理证明的假设经常有缺失的部分。例如 `add_zero` 是一个证明，表示 `? + 0 = ?`，因为 "
 "`add_zero` 实际上是一个函数，而 `?` 是输入。在这种情况下，`rw` 会在目标中查找任何形式为 `x + 0` 的子"
 "项，一旦找到，它就将 `?` 定位为 `x`，然后把所有的 `x + 0` 改为 `x`。\n"
 "\n"
-"练习：思考为什么 `rw [add_zero]` 会把项 `(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为 `0 + (x + 0) + 0 "
-"+ (x + 0)`\n"
+"练习：思考为什么 `rw [add_zero]` 会把项 `(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为 `0 + (x + 0) + "
+"0 + (x + 0)`\n"
 "\n"
 "如果你不能记住等式证明的名称，请在右侧的定理列表中查找。\n"
 "\n"
@@ -334,8 +334,8 @@ msgstr ""
 "`c + a`。这是因为 `add_comm` 是一个证明，表示 `?1 + ?2 = ?2 + ?1`，`add_comm a` 是一个证明，表示 `a "
 "+ ? = ? + a`，而 `add_comm a c` 是另一个证明，表示 `a + c = c + a`。\n"
 "\n"
-"如果 `h : X = Y`，那么 `rw [h]` 将会把所有的 `X` 变为 `Y`。如果你只想改变第37次出现的 `X` 为 `Y`，那么"
-"可以使用 `nth_rewrite 37 [h]`。"
+"如果 `h : X = Y`，那么 `rw [h]` 将会把所有的 `X` 变为 `Y`。如果你只想改变第37次出现的 `X` 为 `Y`，那"
+"么可以使用 `nth_rewrite 37 [h]`。"
 
 #: Game.Levels.Tutorial.L02rw
 msgid ""
@@ -409,8 +409,8 @@ msgid ""
 "We do this in Lean by *rewriting* the proof `h`,\n"
 "using the `rw` tactic."
 msgstr ""
-"在这个关卡里，*目标*是证明 $2y=2(x+7)$。现在我们有一条*假设* `h`，它指出 $y = x + 7$。请检查假设列表中"
-"是否包含了 `h`。在 Lean 中，`h` 被视为一种假设存在的证据，这有点像 `x` 是一个未知的具体数值。\n"
+"在这个关卡里，*目标*是证明 $2y=2(x+7)$。现在我们有一条*假设* `h`，它指出 $y = x + 7$。请检查假设列表"
+"中是否包含了 `h`。在 Lean 中，`h` 被视为一种假设存在的证据，这有点像 `x` 是一个未知的具体数值。\n"
 "\n"
 "要想使用 `rfl` 完成证明，我们首先需要对 $y$ 进行替换。在 Lean 中，我们可以通过*重写*证明 `h` 来实现这"
 "一点，即使用 `rw` 策略。"
@@ -721,8 +721,8 @@ msgstr ""
 "0` 应等于 `a`。在 Lean 中，从这个定义直接衍生出的定理被命名为 `add_zero a`。比如，`add_zero 37` 证明"
 "了 `37 + 0 = 37`，`add_zero x` 证明了 `x + 0 = x`，而 `add_zero` 则证明了 `? + 0 = ?`。\n"
 "\n"
-"我们将定理记作 `add_zero x : x + 0 = x`，其中定理的名称位于前面，而定理的表述则位于后面。这和之前在*假"
-"设*中的记法很像。"
+"我们将定理记作 `add_zero x : x + 0 = x`，其中定理的名称位于前面，而定理的表述则位于后面。这和之前在*"
+"假设*中的记法很像。"
 
 #: Game.Levels.Tutorial.L05add_zero Game.Levels.Tutorial.L06add_zero2
 msgid "$a+(b+0)+(c+0)=a+b+c.$"
@@ -830,17 +830,17 @@ msgstr ""
 " `012`（数字）选项卡里\n"
 "看看你可以用哪些证明重写目标。\n"
 "\n"
-"在 Lean 中，每个数字要么是 $0$，要么是某个数字的后继数。我们已经掌握了如何加上 $0$，下一步需要明白如何"
-"加上后继数。设想我们已经知道 `37 + d = q`。那么 `37 + succ d` 应该是什么呢？由于 `succ d` 比 `d` 多 "
-"$1$，所以 `37 + succ d` 应该等于 `succ q`，也就是 `q` 加 $1$。更一般地，`x + succ d` 应等于 `succ (x "
-"+ d)`。我们把这个规则加为一个引理：\n"
+"在 Lean 中，每个数字要么是 $0$，要么是某个数字的后继数。我们已经掌握了如何加上 $0$，下一步需要明白如"
+"何加上后继数。设想我们已经知道 `37 + d = q`。那么 `37 + succ d` 应该是什么呢？由于 `succ d` 比 `d` "
+"多 $1$，所以 `37 + succ d` 应该等于 `succ q`，也就是 `q` 加 $1$。更一般地，`x + succ d` 应等于 `succ "
+"(x + d)`。我们把这个规则加为一个引理：\n"
 "\n"
 "- `add_succ x d : x + succ d = succ (x + d)`\n"
 "\n"
 "当你在证明目标中遇到 `... + succ ...` 形式时，使用 `rw [add_succ]` 来重写通常是一个好策略。\n"
 "\n"
-"现在，让我们来证明 `succ n = n + 1`。思考如何先引入 `+ succ` 形式，然后再应用 `rw [add_succ]` 策略。请"
-"在右侧“定理”部分的 `+`（代表加法）和 `012`（代表数字）标签页中查找可以用来重写目标的定理。"
+"现在，让我们来证明 `succ n = n + 1`。思考如何先引入 `+ succ` 形式，然后再应用 `rw [add_succ]` 策略。"
+"请在右侧“定理”部分的 `+`（代表加法）和 `012`（代表数字）标签页中查找可以用来重写目标的定理。"
 
 #: Game.Levels.Tutorial.L07add_succ
 msgid "For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$."
@@ -1181,8 +1181,8 @@ 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` 上，以查"
-"看它确切的含义。"
+"请注意，`succ a + «{d}»` 的意思是 `(succ a) + «{d}»`。将你的光标放在目标或假设中的任何 `succ` 上，以"
+"查看它确切的含义。"
 
 #: Game.Levels.Addition.L02succ_add
 msgid "Well done! You now have enough tools to tackle the main boss of this level."
@@ -1317,12 +1317,12 @@ msgstr ""
 "[add_comm b c]` 将不起作用！因为目标是 `(a + b) + c = (a + c) + b`，所以目标中*直接*没有 `b + c` "
 "项。\n"
 "\n"
-"使用结合律和交换律来证明 `add_right_comm`。您不需要使用归纳法。`add_assoc` 移动括号，`add_comm` 移动变"
-"量。\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` 的形式。"
+"例如，`rw [add_comm b]` 只会重写形如 `b + ? = ? + b` 的形式，而 `rw [add_comm b c]` 只会重写形如 `b "
+"+ c = c + b` 的形式。"
 
 #: Game.Levels.Addition.L05add_right_comm
 msgid ""
@@ -1379,13 +1379,14 @@ msgid ""
 "want to explore the game further (for example if you decide to 100%\n"
 "the game)."
 msgstr ""
-"欢迎来到加法世界！在这个世界中，我们将学习 `induction`（归纳）策略。这将使我们能够击败这个世界的Boss级"
-"别，即 `x + y = y + x`。\n"
+"欢迎来到加法世界！在这个世界中，我们将学习 `induction`（归纳）策略。这将使我们能够击败这个世界的Boss"
+"级别，即 `x + y = y + x`。\n"
 "\n"
-"策略 `rw`（重写）、`rfl`（反射）和 `induction`（归纳）是你在加法世界、乘法世界和幂世界中击败所有关卡所"
-"需要策略。幂世界包含了游戏的最终Boss。\n"
+"策略 `rw`（重写）、`rfl`（反射）和 `induction`（归纳）是你在加法世界、乘法世界和幂世界中击败所有关卡"
+"所需要策略。幂世界包含了游戏的最终Boss。\n"
 "\n"
-"这个游戏中还有更多的策略，但只有当你想进一步探索游戏时（例如如果你决定完成游戏的100%）才需要了解它们。"
+"这个游戏中还有更多的策略，但只有当你想进一步探索游戏时（例如如果你决定完成游戏的100%）才需要了解它"
+"们。"
 
 #: Game.Levels.Multiplication.L01mul_one
 msgid "mul_one"
@@ -1632,8 +1633,8 @@ msgid ""
 msgstr ""
 "我们的下一个目标是“左右分配律”，意思是 $a(b+c)=ab+ac$ 和 $(b+c)a=ba+ca$。与其用这样稍显浮夸的名字，不"
 "如使用 Lean 中的证明名称，它们是描述性的。\n"
-"让我们从 `mul_add a b c` 开始，这是 `a * (b + c) = a * b + a * c` 的证明。注意左边包含一个乘法然后是一"
-"个加法。"
+"让我们从 `mul_add a b c` 开始，这是 `a * (b + c) = a * b + a * c` 的证明。注意左边包含一个乘法然后是"
+"一个加法。"
 
 #: Game.Levels.Multiplication.L07mul_add
 msgid ""
@@ -1813,8 +1814,8 @@ msgid ""
 msgstr ""
 "我们应该如何定义 `37 * x`？就像加法一样，我们需要在 $x=0$ 和 $x$ 是后继数时给出定义。\n"
 "\n"
-"0的情况很简单：我们定义 `37 * 0` 为 `0`。现在假设我们知道 `37 * d`。`37 * succ d` 应该是什么呢？嗯，那"
-"是 $d+1$ 个 $37$，它应该是 `37 * d + 37`。\n"
+"0的情况很简单：我们定义 `37 * 0` 为 `0`。现在假设我们知道 `37 * d`。`37 * succ d` 应该是什么呢？嗯，"
+"那是 $d+1$ 个 $37$，它应该是 `37 * d + 37`。\n"
 "\n"
 "以下是 Lean 中的定义。\n"
 "\n"
@@ -1929,8 +1930,8 @@ msgid ""
 msgstr ""
 "`pow_one a` 表示 `a ^ 1 = a`。\n"
 "\n"
-"请注意，这并不是完全根据定义来的：`a ^ 1` 被定义为 `a ^ 0 * a`，所以它是 `1 * a`，要证明这等于 `a`，你"
-"需要在某处使用数学归纳。"
+"请注意，这并不是完全根据定义来的：`a ^ 1` 被定义为 `a ^ 0 * a`，所以它是 `1 * a`，要证明这等于 `a`，"
+"你需要在某处使用数学归纳。"
 
 #: Game.Levels.Power.L03pow_one
 msgid "For all naturals $a$, $a ^ 1 = a$."
@@ -2122,8 +2123,8 @@ msgstr ""
 "我们现在已经有足够的条件来陈述一个数学上准确但有些笨拙的费马大定理了。\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"
+"如果你还没学习过不等式世界，那么我们不能讨论 $m \\geq 3$，所以我们不得不采用使用 `n + 3` 代替 `m` 的"
+"方法，这保证了它足够大。同样，我们用 `a + 1` 代替 `x > 0`。\n"
 "\n"
 "这一关表面上看起来像我们见过的其他关卡，但人类已知的最短解法也将转化为数百万行的 Lean 代码。\n"
 "这个游戏的作者，Kevin Buzzard，正在将 Wiles 和 Taylor 的证明翻译成 Lean，尽管这项任务将花费许多年。\n"
@@ -2141,8 +2142,8 @@ msgid ""
 "modern word `sorry`. The game won't complain - or notice - if you\n"
 "prove anything with `xyzzy`."
 msgstr ""
-"`xyzzy` 是一个古老的魔法咒语，被认为是现代词汇 `sorry` 的起源。游戏不会发现——或者注意到你用 `xyzzy` 证"
-"明任何东西。"
+"`xyzzy` 是一个古老的魔法咒语，被认为是现代词汇 `sorry` 的起源。游戏不会发现——或者注意到你用 `xyzzy` "
+"证明任何东西。"
 
 #: Game.Levels.Power.L10FLT
 msgid ""
@@ -2300,8 +2301,8 @@ msgid ""
 msgstr ""
 "再做一次！\n"
 "\n"
-"`rw [zero_add] at «{h}»` 试图填充 `zero_add` 的参数（找到 `«{x}»`），然后替换它找到的所有 `0 + «{x}»` "
-"出现的地方。因此，`0 + «{y}»`还没有被重写 。"
+"`rw [zero_add] at «{h}»` 试图填充 `zero_add` 的参数（找到 `«{x}»`），然后替换它找到的所有 `0 + "
+"«{x}»` 出现的地方。因此，`0 + «{y}»`还没有被重写 。"
 
 #: Game.Levels.Implication.L02exact2
 msgid ""
@@ -2355,8 +2356,8 @@ msgid ""
 msgstr ""
 "## 概述\n"
 "\n"
-"如果 `t : P → Q` 是一个 $P\\implies Q$ 的证明，而 `h : P` 是一个 `P` 的证明，那么 `apply t at h` 会将 "
-"`h` 转换为证明 `Q`。其原理是，如果您知道 `P` 为真，那么您可以从 `t` 推断出 `Q` 为真。\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"
@@ -2366,8 +2367,8 @@ msgstr ""
 "`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"
+"为 `a + 37 = b + 42`。您可以写 `apply succ_inj (a + 37) (b + 42) at h`，但 Lean 足够聪明，可以自行推"
+"断出 `succ_inj` 的输入。\n"
 "\n"
 "### 示例：\n"
 "\n"
@@ -2411,8 +2412,8 @@ msgstr ""
 "*Peano* 标签中的这个定理以获取更多信息。\n"
 "\n"
 "皮亚诺将这个定理作为一个公理，但在算法世界中我们将展示如何在 Lean 中证明它。\n"
-"现在让我们先假设它，然后让我们使用它证明 $x+1=4 \\implies x=3$。再一次，我们将通过操纵我们的假设直到它"
-"变成目标来进行。我将引导你通过这个关卡。"
+"现在让我们先假设它，然后让我们使用它证明 $x+1=4 \\implies x=3$。再一次，我们将通过操纵我们的假设直到"
+"它变成目标来进行。我将引导你通过这个关卡。"
 
 #: Game.Levels.Implication.L04succ_inj
 msgid ""
@@ -2484,8 +2485,8 @@ 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` 输"
-"入 `←`。"
+"你可以在提供给 `rw` 的任何定理前面放一个 `←` 来进行反向重写。查看 `rw` 的文档以获得解释。使用 `\\l` "
+"输入 `←`。"
 
 #: Game.Levels.Implication.L04succ_inj
 msgid "Concretely: `rw [← succ_eq_add_one] at h`."
@@ -2496,7 +2497,8 @@ 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` 的证据。"
+"现在让我们应用（ `apply` ）我们的新定理。执行 `apply succ_inj at h` 来将 `h` 变为证明 `x = 3` 的证"
+"据。"
 
 #: Game.Levels.Implication.L04succ_inj
 msgid "Now finish in one line."
@@ -2696,16 +2698,16 @@ msgid ""
 "So if your goal is `False` then you had better hope that your hypotheses\n"
 "are contradictory, which they are in this level."
 msgstr ""
-"我们仍然不能证明 `2 + 2 ≠ 5`，因为我们还没有讨论 `≠` 的定义。在 Lean 中，`a ≠ b` 是 `a = b → False` 的"
-"*符号表示*。这里的 `False` 是一个通用的假命题，`→` 是 Lean 中表示“蕴含”的符号\n"
+"我们仍然不能证明 `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`，那么你最好希望你的假设是矛"
-"盾的，就像在本关中一样。"
+"`False` 是一个无法从一致的假设集中推导出的目标！所以如果你的目标是 `False`，那么你最好希望你的假设是"
+"矛盾的，就像在本关中一样。"
 
 #: Game.Levels.Implication.L08ne
 msgid "If $x=y$ and $x \\neq y$ then we can deduce a contradiction."
@@ -2816,8 +2818,8 @@ msgid ""
 "does the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\n"
 "the proof `zero_ne_one`; now try proving $1 \\neq 0$."
 msgstr ""
-"我们知道 `zero_ne_succ n` 是证明 `0 = succ n → False` 的证明。但是如果我们有一个假设 `succ n = 0` 呢？"
-"这恰好是反过来的！\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"
@@ -2926,10 +2928,10 @@ msgstr ""
 "```\n"
 "\n"
 "\n"
-"尽管 Lean 是一个定理证明器，但很明显我们还没有开发足够的材料使其成为一个合适的计算器。在算法世界，一个"
-"更具计算机科学色彩的世界中，我们将开发使这类问题变得更容易的机制（比如快速证明 $20 + 20 \\neq 41$ ）。"
-"或者，你也可以在高级加法世界中进行更多数学学习，我们在那里证明了建立不等式理论所需的引理。点击“离开世"
-"界”并决定你的路线。"
+"尽管 Lean 是一个定理证明器，但很明显我们还没有开发足够的材料使其成为一个合适的计算器。在算法世界，一"
+"个更具计算机科学色彩的世界中，我们将开发使这类问题变得更容易的机制（比如快速证明 $20 + 20 \\neq "
+"41$ ）。或者，你也可以在高级加法世界中进行更多数学学习，我们在那里证明了建立不等式理论所需的引理。点"
+"击“离开世界”并决定你的路线。"
 
 #: Game.Levels.Implication
 msgid "Implication World"
@@ -3104,7 +3106,7 @@ msgid ""
 "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"
 "\n"
 "我们自制的策略 `simp_add` 将解决以下形式的任意目标：\n"
 " `a + (b + c) + (d + e) = e + (d + (c + b)) + a`。"
@@ -3253,7 +3255,7 @@ msgid ""
 "\n"
 "`trivial` will solve the goal `True`."
 msgstr ""
-"＃ 小结\n"
+"## 概述\n"
 "\n"
 "`trivial` 将解决目标 `True`。"
 
@@ -3272,7 +3274,8 @@ 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)`。"
+"我们将要把那个 `False` 变成 `True`。首先通过执行 `rw [← is_zero_succ a]` 把它变成 `is_zero (succ "
+"a)`。"
 
 #: Game.Levels.Algorithm.L06is_zero
 msgid ""
@@ -3314,9 +3317,9 @@ msgstr ""
 "* 如果 `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`。"
+"`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`。"
 
 #: Game.Levels.Algorithm.L07succ_ne_succ
 msgid ""
@@ -3395,15 +3398,15 @@ msgid ""
 "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"
 "\n"
 "如果 `decide` 可以找到一种算法来解决目标，它将尝试解决该目标。\n"
 "\n"
-"## 示例\n"
+"### 示例\n"
 "\n"
 "类型为 `DecidableEq ℕ` 的项是用于判断两个自然数是否相等或不同的算法（的实现函数）。\n"
-"因此，一旦这个项被创建并成为一个 `instance`，`decide` 策略就可以使用它来解决形式为 `a = b` 或 `a ≠ b` "
-"的目标。"
+"因此，一旦这个项被创建并成为一个 `instance`，`decide` 策略就可以使用它来解决形式为 `a = b` 或 `a ≠ "
+"b` 的目标。"
 
 #: Game.Levels.Algorithm.L08decide
 msgid ""
@@ -3506,8 +3509,8 @@ msgid ""
 "\n"
 "Click on \"Start\" to proceed."
 msgstr ""
-"像 $2+2=4$ 和 $a+b+c+d+e=e+d+c+b+a$ 这样的证明如果手工完成会非常繁琐。在算法世界中，我们将学习如何让计"
-"算机帮我们完成它们。\n"
+"像 $2+2=4$ 和 $a+b+c+d+e=e+d+c+b+a$ 这样的证明如果手工完成会非常繁琐。在算法世界中，我们将学习如何让"
+"计算机帮我们完成它们。\n"
 "\n"
 "点击“开始”继续。"
 
@@ -3623,8 +3626,7 @@ msgid ""
 "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n"
 "Two ways to do it spring to mind; I'll mention them when you've solved it."
 msgstr ""
-"`add_right_eq_self x y` 是 $x + y = x\\implies y=0.$ 的定理。\n"
-"我想到了两种方法，等你解出来了我再提。"
+"`add_right_eq_self x y` 是 $x + y = x\\implies y=0$ 的定理。我想到了两种方法，等你解出来了我再提。"
 
 #: Game.Levels.AdvAddition.L04add_right_eq_self
 msgid "$x+y=x\\implies y=0$."
@@ -3723,13 +3725,13 @@ msgstr ""
 "\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"
+"例如，有时你想分别处理 `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`！所以你最终会没有目标，意味着你已经证明了一"
-"切。"
+"`cases h` 将证明目标，因为没有 *任何* 方法可以证明 `False`！所以你最终会没有目标，意味着你已经证明了"
+"一切。"
 
 #: Game.Levels.AdvAddition.L05add_right_eq_zero
 msgid ""
@@ -3768,8 +3770,8 @@ msgid ""
 msgstr ""
 "## 概述\n"
 "\n"
-"如果 `n` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n = 0`，另一个是 `n = succ "
-"d`。\n"
+"如果 `n` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n = 0`，另一个是 `n = "
+"succ d`。\n"
 "\n"
 "如果 `h` 是一个证明（例如一个假设），那么 `cases h with...` 会将证明分解成用来证明它的各个部分。\n"
 "\n"
@@ -3780,18 +3782,18 @@ msgstr ""
 "\n"
 "## 示例\n"
 "\n"
-"如果 `h : P ∨ Q` 是一个假设，那么 `cases h with hp hq` 会将一个目标变成两个目标，一个有假设 `hp : P`，"
-"另一个有假设 `hq : Q`。\n"
+"如果 `h : P ∨ Q` 是一个假设，那么 `cases h with hp hq` 会将一个目标变成两个目标，一个有假设 `hp : "
+"P`，另一个有假设 `hq : Q`。\n"
 "\n"
 "## 示例\n"
 "\n"
-"如果 `h : False` 是一个假设，那么 `cases h` 会将一个目标变成没有目标，因为没有方法可以证明 `False`！如"
-"果你没有剩余的目标，你就完成了这个关卡。\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`。"
+"如果 `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$."
@@ -3926,8 +3928,8 @@ msgid ""
 "To *prove* an \"exists\" statement, use the `use` tactic.\n"
 "Let's see an example."
 msgstr ""
-"`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。这个“倒 E”代表“存在”。所以 `a ≤ b` 意味着存在一个数字 `c` 使"
-"得 `b = a + c`。这个定义有效是因为在这个游戏中没有负数。\n"
+"`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。这个“倒 E”代表“存在”。所以 `a ≤ b` 意味着存在一个数字 `c` "
+"使得 `b = a + c`。这个定义有效是因为在这个游戏中没有负数。\n"
 "\n"
 "要*证明*一个“存在性”定理，可以使用 `use` 策略。\n"
 "让我们看一个例子。"
@@ -4122,7 +4124,8 @@ msgid ""
 "In other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.\n"
 "It's the trickiest one so far. Good luck!"
 msgstr ""
-"这一关卡要求你证明 $\\leq$ 的 *反对称性* 。换句话说，如果 $x \\leq y$ 且 $y \\leq x$，那么 $x = y$。\n"
+"这一关卡要求你证明 $\\leq$ 的 *反对称性* 。换句话说，如果 $x \\leq y$ 且 $y \\leq x$，那么 $x = y"
+"$。\n"
 "这是本游戏到目前最棘手的证明之一。祝你好运！"
 
 #: Game.Levels.LessOrEqual.L06le_antisymm
@@ -4232,16 +4235,14 @@ msgid ""
 "`cases h with h1 h2` will create two goals, one where you went left,\n"
 "and the other where you went right."
 msgstr ""
-"\"`≤`的完全性是这个世界的老大级别，接下来就是它了。它表明如果`a`和`b`是自然数，\n"
-"那么要么`a ≤ b`，要么`b ≤ a`。但我们根本没有讨论过`或`。这里有一个简要说明。\n"
-"\n"
-"1) “或”的符号是`∨`。你不需要直接打它，你可以用`\\or`来输入它。\n"
+"`≤`的完全性是这个世界的Boss关卡了，接下来就是它了。它表明如果`a`和`b`是自然数，\n"
+"那么`a ≤ b`或`b ≤ a`。但我们根本没有讨论过“或”（`or`）。这里有一个简要说明。\n"
 "\n"
-"2) 如果你的 *目标* 是一个“或”命题，那么有两个策略可以取得进展：`left`和`right`。\n"
+"1. “或”的符号是`∨`，你可以用`\\or`来输入它。\n"
+"2. 如果你的 *目标* 是一个“或”命题，那么有两个策略可以取得进展：`left`和`right`。\n"
 "但除非你的知道哪边是真的，否则不要选择一个方向。\n"
-"\n"
-"3) 如果你在 *假设* 中有一个“或”命题`h`，那么`cases h with h1 h2`会创建两个目标，一个假设左边是真的，另"
-"一个假设右边是真的。"
+"3. 如果你在 *假设* 中有一个“或”命题`h`，那么`cases h with h1 h2`会创建两个目标，一个假设左边是真的，"
+"另一个假设右边是真的。"
 
 #: Game.Levels.LessOrEqual.L07or_symm
 msgid "If $x=37$ or $y=42$, then $y=42$ or $x=37$."
@@ -4285,8 +4286,8 @@ msgid ""
 "I've left hidden hints; if you need them, retry from the beginning\n"
 "and click on \"Show more help!\""
 msgstr ""
-"我认为这是迄今为止最难的关卡。提示：如果 `a` 是一个数字，那么 `cases a with b` 会分解为 `a = 0` 和 `a "
-"= succ b` 两种情况。不要在你的假设不能保证你能证明最终目标之前选择证明左边或右边！\n"
+"我认为这是迄今为止最难的关卡。提示：如果 `a` 是一个数字，那么 `cases a with b` 会分解为 `a = 0` 和 "
+"`a = succ b` 两种情况。不要在你的假设不能保证你能证明最终目标之前选择证明左边或右边！\n"
 "\n"
 "我留下了一些隐藏的提示；如果你需要，请从头开始重试并点击“显示更多帮助”！"
 
@@ -4437,8 +4438,8 @@ msgid ""
 msgstr ""
 "我们需要这个引理来证明二是质数！\n"
 "\n"
-"你需要知道 `∨` 是右结合的。这意味着 `x = 0 ∨ x = 1 ∨ x = 2` 实际上意味着 `x = 0 ∨ (x = 1 ∨ x = 2)`。这"
-"会影响 `left` 和 `right` 的工作方式。"
+"你需要知道 `∨` 是右结合的。这意味着 `x = 0 ∨ x = 1 ∨ x = 2` 实际上意味着 `x = 0 ∨ (x = 1 ∨ x = 2)`。"
+"这会影响 `left` 和 `right` 的工作方式。"
 
 #: Game.Levels.LessOrEqual.L11le_two
 msgid "If $x \\leq 2$ then $x = 0$ or $1$ or $2$."
@@ -4534,8 +4535,7 @@ msgid ""
 "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!`（显示更多帮"
-"助！）。"
+"记住，`x ≠ 0` 是 `x = 0 → False` 的符号表示。如果你需要提示，请点击`显示更多帮助！`。"
 
 #: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
 msgid "Start with `intro hb`."
@@ -4584,7 +4584,7 @@ msgid ""
 msgstr ""
 "## 概述\n"
 "\n"
-"`tauto` 策略将解决任何可以纯粹通过逻辑解决的目标（即，通过真值表）。\n"
+"`tauto` 策略将解决任何只靠命题逻辑就可以解决的目标（即，通过真值表）。\n"
 "\n"
 "### 示例\n"
 "\n"
@@ -4606,8 +4606,8 @@ msgstr ""
 "\n"
 "### 示例\n"
 "\n"
-"如果你有一个形式为 `a = 0 → a * b = 0` 的假设，而你的目标是 `a * b ≠ 0 → a ≠ 0`，那么 `tauto` 将解决目"
-"标，因为目标在逻辑上等同于假设。\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"
@@ -4636,7 +4636,8 @@ msgid ""
 "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."
 msgstr ""
-"乘法通常会使一个数字变大，但是乘以零可以使它变小。因此，关于不等式和乘法的许多引理需要假设 `a ≠ 0`。\n"
+"乘法通常会使一个数字变大，但是乘以零可以使它变小。因此，关于不等式和乘法的许多引理需要假设 `a ≠ "
+"0`。\n"
 "这里有一个关键的引理使我们能够使用这个假设。我们可以使用 `tauto` 策略帮助我们进行证明。点击右侧的策略"
 "名称查看它的作用。"
 
@@ -4770,12 +4771,13 @@ msgstr ""
 "\n"
 "`have ha : a = 0`\n"
 "\n"
-"那么你将得到一个新的目标 `a = 0` 来证明，一旦你证明了它，你将在你原始的目标中有一个新的假设 `ha : a = "
-"0`。\n"
+"那么你将得到一个新的目标 `a = 0` 来证明，一旦你证明了它，你将在你原始的目标中有一个新的假设 `ha : a "
+"= 0`。\n"
 "\n"
 "## 示例\n"
 "\n"
-"如果你已经有了你想要 `have` 的证明，你可以立即创建它。例如，如果你有 `a` 和 `b` 这两个数字对象，那么\n"
+"如果你已经有了你想要 `have` 的证明，你可以立即创建它。例如，如果你有 `a` 和 `b` 这两个数字对象，那"
+"么\n"
 "\n"
 "`have h2 : succ a = succ b → a = b := succ_inj a b`\n"
 "\n"
@@ -4872,8 +4874,8 @@ msgid ""
 "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."
 msgstr ""
-"这个关卡要证明如果 `a * b = 0` 那么 `a = 0` 或者 `b = 0`。这在逻辑上等同上一个关卡，所以有一个非常简短"
-"的证明。"
+"这个关卡要证明如果 `a * b = 0` 那么 `a = 0` 或者 `b = 0`。这在逻辑上等同上一个关卡，所以有一个非常简"
+"短的证明。"
 
 #: Game.Levels.AdvMultiplication.L08mul_eq_zero
 msgid "Start with `have h2 := mul_ne_zero a b`."
@@ -4908,8 +4910,8 @@ msgid ""
 "\"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`.\""
 msgstr ""
-"在这个关卡中，我们证明了如果 `a * b = a * c` 且 `a ≠ 0` 那么 `b = c`。这是有些难的，因为几个原因。其中"
-"之一是我们需要引入一个新的想法：我们需要更好地理解数学归纳法的概念。\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"
@@ -4932,8 +4934,8 @@ 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`）它。"
+"归纳假设 `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`."
@@ -5005,11 +5007,11 @@ msgstr ""
 "高级 *加法* 世界证明了涉及加法的各种引理，例如 `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"
+"在高级乘法世界中，我们证明了关于乘法的类似事实，例如 `x * y = 1 → x = 1`，以及 `x * y = x → y = "
+"1`（在后一个结果中假设 `x ≠ 0`）。这将为我们进入可除性世界做准备。\n"
 "\n"
-"乘法世界比加法世界更为复杂。同样，高级乘法世界比高级加法世界更为复杂。其中一个原因是某些中间结果只在额"
-"外假设下为真，即变量之一非零。这导致了一些意想不到的额外转折。"
+"乘法世界比加法世界更为复杂。同样，高级乘法世界比高级加法世界更为复杂。其中一个原因是某些中间结果只在"
+"额外假设下为真，即变量之一非零。这导致了一些意想不到的转折。"
 
 #: Game
 msgid "Natural Number Game"
@@ -5060,8 +5062,8 @@ msgstr ""
 "\n"
 "开始游戏，请点击“教程世界”。\n"
 "\n"
-"请注意：这是基于全新 Lean 4 开发的游戏版本，新增了许多旧版 Lean 3 中未包含的世界。高级乘法世界的新版本"
-"正在开发中，其他新世界如素数世界等将于2023年10月至11月陆续推出。\n"
+"请注意：这是基于全新 Lean 4 开发的游戏版本，新增了许多旧版 Lean 3 中未包含的世界。高级乘法世界的新版"
+"本正在开发中，其他新世界如素数世界等将于2023年10月至11月陆续推出。\n"
 "\n"
 "## 更多信息\n"
 "\n"
@@ -5123,7 +5125,8 @@ msgstr ""
 "游戏会将你的进度存储在本地浏览器存储中。\n"
 "如果你删除它，你的进度将会丢失！\n"
 "\n"
-"警告：在大多数浏览器中，删除 cookie 也会清除本地存储（或“本地网站数据”）。确保首先下载你的游戏进度！\n"
+"警告：在大多数浏览器中，删除 cookie 也会清除本地存储（或“本地网站数据”）。确保首先下载你的游戏进"
+"度！\n"
 "\n"
 "## 致谢\n"
 "\n"
@@ -5131,7 +5134,8 @@ msgstr ""
 "* **原始 Lean3 版本：** Kevin Buzzard, Mohammad Pedramfar\n"
 "* **游戏引擎：** Alexander Bentkamp, Jon Eugster, Patrick Massot\n"
 "* **额外关卡：** Sian Carey, Ivan Farabella, Archie Browne.\n"
-"* **特别感谢：** 所有学生测试者，所有邀请 Kevin 发表演讲的学校，以及向他提出关于材料问题的所有学生。\n"
+"* **特别感谢：** 所有学生测试者，所有邀请 Kevin 发表演讲的学校，以及向他提出关于材料问题的所有学"
+"生。\n"
 "\n"
 "## 资源\n"
 "\n"
@@ -5140,9 +5144,9 @@ msgstr ""
 "\n"
 "## 有问题吗？\n"
 "\n"
-"请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新成"
-"员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使用您的全名，保持话题相关，且"
-"友好。如果你正在寻找一个不那么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean "
+"请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新"
+"成员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使用您的全名，保持话题相关，"
+"且友好。如果你正在寻找一个不那么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean "
 "Discord](https://discord.gg/WZ9bs9UCvx)。\n"
 "\n"
 "另外，如果你遇到问题/漏洞，你也可以在 github 上提出问题：\n"