From 49f1a334061c8d1518bfccedea97d0e1f44b0553 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 1 Feb 2025 23:24:33 +0000 Subject: [PATCH] more realistic claims about prime number world --- .i18n/en/Game.pot | 66 ++++++++++--------- Game.lean | 12 ++-- .../AdvMultiplication/L05le_mul_right.lean | 3 +- 3 files changed, 43 insertions(+), 38 deletions(-) diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot index 7c7a434..3f14094 100644 --- a/.i18n/en/Game.pot +++ b/.i18n/en/Game.pot @@ -1,7 +1,7 @@ msgid "" msgstr "Project-Id-Version: Game v4.7.0\n" "Report-Msgid-Bugs-To: \n" -"POT-Creation-Date: Mon Apr 29 13:18:35 2024\n" +"POT-Creation-Date: Sat Feb 1 23:22:17 2025\n" "Last-Translator: \n" "Language-Team: none\n" "Language: en\n" @@ -166,7 +166,7 @@ msgid "## Summary\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" +"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" @@ -1343,7 +1343,7 @@ msgstr "" msgid "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" +"If you're having trouble exchanging the right `a * b`\n" "because `rw [mul_comm]` swaps the wrong multiplication,\n" "then read the documentation of `rw` for tips on how to fix this." msgstr "" @@ -1378,7 +1378,7 @@ msgstr "" msgid "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" +"clearly see that there are two levels 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" @@ -1855,7 +1855,7 @@ msgid "`a ≠ b` is *notation* for `(a = b) → 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 upshot of this is that you 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" @@ -2301,7 +2301,7 @@ msgstr "" #: 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`." +"contrapositive, namely a hypothesis of `succ m = succ n` and a goal of `m = n`." msgstr "" #: Game.Levels.Algorithm.L07succ_ne_succ @@ -2518,20 +2518,18 @@ msgid "Here's a proof using `add_left_eq_self`:\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" +"Alternatively you can just prove it by induction on `x`:\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" +"induction x with d hd\n" +"intro h\n" +"rw [zero_add] at h\n" +"exact h\n" +"intro h\n" +"rw [succ_add] at h\n" +"apply succ_inj at h\n" +"apply hd at h\n" +"exact h\n" "```" msgstr "" @@ -2666,7 +2664,13 @@ msgid "## Summary\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`." +"number which is morally `b - a` (i.e. `use b - a`)\n" +"\n" +"Any of the following examples is possible assuming the type of the argument passed to the `use` function is accurate:\n" +"\n" +"- `use 37`\n" +"- `use a`\n" +"- `use a * a + 1`" msgstr "" #: Game.Levels.LessOrEqual.L01le_refl @@ -3180,7 +3184,7 @@ msgstr "" #: 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" +"hypothesis `a ≠ 0`. Here is a key lemma that 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." msgstr "" @@ -3227,7 +3231,7 @@ msgstr "" #: Game.Levels.AdvMultiplication.L05le_mul_right msgid "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" +"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." @@ -3278,7 +3282,7 @@ msgid "# Summary\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" +"are proving. For example\n" "\n" "`have h2 := succ_inj a b`\n" "\n" @@ -3310,7 +3314,7 @@ msgid "Now you can `apply le_mul_right at h2`." msgstr "" #: Game.Levels.AdvMultiplication.L06mul_right_eq_one -msgid "Now `rw [h] at h2` so you can `apply le_one at hx`." +msgid "Now `rw [«{h}»] at «{h2}»` so you can `apply le_one at «{h2}»`." msgstr "" #: Game.Levels.AdvMultiplication.L06mul_right_eq_one @@ -3381,8 +3385,8 @@ msgid "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c` "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`.\"" +"\"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 "" #: Game.Levels.AdvMultiplication.L09mul_left_cancel @@ -3479,10 +3483,10 @@ msgid "# Welcome to the Natural Number Game\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" +"worlds which were not present in the old Lean 3 version. More new worlds\n" +"such as Strong Induction World, Even/Odd World and Prime Number World\n" +"are in development; if you want to see their state or even help out, checkout\n" +"out the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues).\n" "\n" "## More\n" "\n" @@ -3491,9 +3495,9 @@ msgid "# Welcome to the Natural Number Game\n" msgstr "" #: Game -msgid "*Game version: 4.2*\n" +msgid "*Game version: 4.3*\n" "\n" -"*Recent additions: Inequality world, algorithm world*\n" +"*Recent additions: bug fixes*\n" "\n" "## Progress saving\n" "\n" diff --git a/Game.lean b/Game.lean index 6c67bfb..c7d4964 100644 --- a/Game.lean +++ b/Game.lean @@ -41,10 +41,10 @@ those who read the help texts like this one. To start, click on \"Tutorial World\". Note: this is a new Lean 4 version of the game containing several -worlds which were not present in the old Lean 3 version. A new version -of Advanced Multiplication World is in preparation, and worlds -such as Prime Number World and more will be appearing during October and -November 2023. +worlds which were not present in the old Lean 3 version. More new worlds +such as Strong Induction World, Even/Odd World and Prime Number World +are in development; if you want to see their state or even help out, checkout +out the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues). ## More @@ -53,9 +53,9 @@ links, and ways to interact with the Lean community. " Info " -*Game version: 4.2* +*Game version: 4.3* -*Recent additions: Inequality world, algorithm world* +*Recent additions: bug fixes* ## Progress saving diff --git a/Game/Levels/AdvMultiplication/L05le_mul_right.lean b/Game/Levels/AdvMultiplication/L05le_mul_right.lean index d22d88b..0b77212 100644 --- a/Game/Levels/AdvMultiplication/L05le_mul_right.lean +++ b/Game/Levels/AdvMultiplication/L05le_mul_right.lean @@ -18,7 +18,8 @@ TheoremDoc MyNat.le_mul_right as "le_mul_right" in "≤" Introduction " -In Prime Number World we will be proving that $2$ is prime. +One day this game will have a Prime Number World, with a final boss +of proving that $2$ is prime. To do this, we will have to rule out things like $2 = 37 × 42.$ We will do this by proving that any factor of $2$ is at most $2$, which we will do using this lemma. The proof I have in mind manipulates the hypothesis