diff --git a/.i18n/Game.pot b/.i18n/Game.pot
new file mode 100644
index 0000000..ded3bff
--- /dev/null
+++ b/.i18n/Game.pot
@@ -0,0 +1,75 @@
+msgid ""
+msgstr "Project-Id-Version: Game v4.6.0\n"
+"Report-Msgid-Bugs-To: \n"
+"POT-Creation-Date: Thu Feb 29 12:11:54 2024\n"
+"Last-Translator: \n"
+"Language-Team: none\n"
+"Language: en\n"
+"Content-Type: text/plain; charset=UTF-8\n"
+"Content-Transfer-Encoding: 8bit"
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "Hello World"
+msgstr ""
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "This text is shown as first message when the level is played.\n"
+"You can insert hints in the proof below. They will appear in this side panel\n"
+"depending on the proof a user provides."
+msgstr ""
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "You can either start using `h` or `g`."
+msgstr ""
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "You should use `«{h}»` now."
+msgstr ""
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "You should use `«{g}»` now."
+msgstr ""
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "This last message appears if the level is solved."
+msgstr ""
+
+#: Game.Levels.DemoWorld
+msgid "Demo World"
+msgstr ""
+
+#: Game.Levels.DemoWorld
+msgid "\n"
+"This introduction is shown before one enters level 1 of the demo world. Use markdown.\n"
+""
+msgstr ""
+
+#: Game
+msgid "Hello World Game"
+msgstr ""
+
+#: Game
+msgid "\n"
+"This text appears on the starting page where one selects the world/level to play.\n"
+"You can use markdown.\n"
+""
+msgstr ""
+
+#: Game
+msgid "\n"
+"Here you can put additional information about the game. It is accessible\n"
+"from the starting through the drop-down menu.\n"
+"\n"
+"For example: Game version, Credits, Link to Github and Zulip, etc.\n"
+"\n"
+"Use markdown.\n"
+""
+msgstr ""
+
+#: Game
+msgid "Game Template"
+msgstr ""
+
+#: Game
+msgid "You should use this game as a template for your own game and add your own levels."
+msgstr ""
diff --git a/.i18n/config.json b/.i18n/config.json
new file mode 100644
index 0000000..22776e9
--- /dev/null
+++ b/.i18n/config.json
@@ -0,0 +1,4 @@
+{
+  "sourceLang": "en",
+  "translationContactEmail": ""
+}
diff --git a/Game/Metadata.lean b/Game/Metadata.lean
index 10095d0..9b4545f 100644
--- a/Game/Metadata.lean
+++ b/Game/Metadata.lean
@@ -1,6 +1,6 @@
 import GameServer.Commands
 
-import Mathlib.Tactic.Common
+-- import Mathlib.Tactic.Common
 
 /-! Use this file to add things that should be available in all levels.
 
diff --git a/lake-manifest.json b/lake-manifest.json
index d40cda4..2faf3e0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,73 +4,28 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/lean4game.git",
-   "type": "git",
-   "subDir": "server",
-   "rev": "d689c7ec865dfcd804b478ee526e9cd06cff0c22",
-   "name": "GameServer",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
-   "name": "aesop",
+   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
+   "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/lean4game.git",
    "type": "git",
-   "subDir": null,
-   "rev": "feec58a7ee9185f92abddcf7631643b53181a7d3",
-   "name": "mathlib",
+   "subDir": "server",
+   "rev": "dd60093dfc508e6cf593b46a6c92b7cbb0f3392f",
+   "name": "GameServer",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Game",
diff --git a/lakefile.lean b/lakefile.lean
index 6857589..8fe3b62 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -32,7 +32,7 @@ you can use `require mathlib from git "[URL]" @ leanVersion`
 
 
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ leanVersion
+-- require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ leanVersion
 
 
 
diff --git a/lean-toolchain b/lean-toolchain
index bd59abf..5026204 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0