From 4c135aa6ae2ed4c2e9be96a0510ac7aae428bbdf Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 12 Dec 2022 16:28:07 +0100
Subject: [PATCH 1/6] load level using rtk

---
 client/src/components/LeftPanel.tsx |  4 +-
 client/src/components/Level.tsx     | 69 ++++++-----------------------
 client/src/game/api.ts              | 17 +++++--
 3 files changed, 30 insertions(+), 60 deletions(-)

diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx
index b46ddb3..9457b38 100644
--- a/client/src/components/LeftPanel.tsx
+++ b/client/src/components/LeftPanel.tsx
@@ -71,12 +71,12 @@ function LemmaDocs({ lemmas }) {
 function LeftPanel({ spells, inventory }) {
   return (
     <Box>
-      {spells.length > 0 &&
+      {spells && spells.length > 0 &&
         <Paper sx={{ px: 2, py: 1 }}>
           <Typography variant="h5" sx={{ mb: 2 }}>Spell book</Typography>
           {spells.map((spell) => <TacticDoc key={spell.name} tactic={spell} />)}
         </Paper>}
-      {inventory.length > 0 && <LemmaDocs lemmas={inventory} />}
+      {inventory && inventory.length > 0 && <LemmaDocs lemmas={inventory} />}
     </Box>)
 }
 
diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index e094771..0c7e9e2 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -9,7 +9,7 @@ import { MathJax } from "better-react-mathjax";
 import { Link as RouterLink } from 'react-router-dom';
 
 
-import { Button, FormControlLabel, FormGroup, Switch } from '@mui/material';
+import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
 
 import LeftPanel from './LeftPanel';
@@ -24,6 +24,7 @@ import { ConnectionContext } from '../connection';
 import Infoview from './Infoview';
 import { useParams } from 'react-router-dom';
 import { MonacoServices } from 'monaco-languageclient';
+import { useLoadLevelQuery } from '../game/api';
 
 
 
@@ -33,43 +34,15 @@ function Level() {
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
 
-  const [tacticDocs, setTacticDocs] = useState([])
-  const [lemmaDocs, setLemmaDocs] = useState([])
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
   const [infoviewApi, setInfoviewApi] = useState(null)
   const [expertInfoview, setExpertInfoview] = useState(false)
 
-
-  const [leanData, setLeanData] = useState({goals: []})
-  const [history, setHistory] = useState([])
-  const [lastTactic, setLastTactic] = useState("")
-  const [introduction, setIntroduction] = useState("")
-  const [errors, setErrors] = useState([])
   const codeviewRef = useRef<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
   const messagePanelRef = useRef<HTMLDivElement>(null)
 
-  const [ready, setReady] = useState(false)
-
-  const [message, setMessage] = useState("")
-  const [messageOpen, setMessageOpen] = useState(false)
-
-
-  const [completed, setCompleted] = useState(false)
-
-  const processResponse = (res:any) => {
-    setLeanData(res);
-    // setErrors(res.errors);
-    // if (res.message !== "" && res.errors?.length === 0) {
-    //   setMessage(res.message)
-    //   setMessageOpen(true)
-    // }
-    // if (res.goals?.length === 0 && res.errors?.length === 0) {
-    //   setCompleted(true)
-    // }
-  }
-
   useEffect(() => {
     // Scroll to top when loading a new level
     messagePanelRef.current!.scrollTo(0,0)
@@ -106,57 +79,43 @@ function Level() {
     return () => { editor.dispose() }
   }, [])
 
-  const uri = `file:///${worldId}/${levelId}`
 
   // The next function will be called when the level changes
   useEffect(() => {
     connection.startLeanClient().then((leanClient) => {
       if (editor) {
 
-        const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri))
+        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
+        const model = monaco.editor.getModel(uri) ??
+          monaco.editor.createModel('', 'lean4', uri)
 
         editor.setModel(model)
         infoviewApi.serverRestarted(leanClient.initializeResult)
         infoProvider.openPreview(editor, infoviewApi)
-        setReady(true)
 
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
 
-        leanClient.sendRequest("loadLevel", {world: worldId, level: levelId}).then((res) => {
-          // setLevelTitle("Level " + res["index"] + ": " + res["title"])
-          // setIndex(parseInt(res["index"]))
-          setTacticDocs(res["tactics"])
-          setLemmaDocs(res["lemmas"])
-          setIntroduction(res["introduction"])
-          processResponse(res)
-        });
-
-        return () => { model.dispose(); setReady(false) }
+        return () => { model.dispose(); }
       }
     })
 
   }, [editor, levelId, connection])
 
-  function loadLevel(index) {
-    setCompleted(false)
-    setHistory([])
-    // setCurLevel(index)
-  }
 
-  return (
-    <Grid className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
+  const level = useLoadLevelQuery({world: worldId, level: levelId})
+
+  return <>
+    <Box style={level.isLoading ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
+    <Grid style={level.isLoading ? {display: "none"} : null} className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
       <Grid xs={4} className="doc-panel">
-        <LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
+        <LeftPanel spells={level?.data?.tactics} inventory={level?.data?.tactics} />
       </Grid>
       <Grid xs={4} className="main-panel">
         <div ref={messagePanelRef} className="message-panel">
-          <MathJax><ReactMarkdown>{introduction}</ReactMarkdown></MathJax>
+          <MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
         </div>
         <div ref={codeviewRef} className="codeview">
-          {/* <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
-            errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} /> */}
-          {/* <Message isOpen={messageOpen} content={message} close={closeMessage} /> */}
         </div>
       </Grid>
       <Grid xs={4} className="info-panel">
@@ -173,7 +132,7 @@ function Level() {
         </FormGroup>
       </Grid>
     </Grid>
-  )
+    </>
 }
 
 export default Level
diff --git a/client/src/game/api.ts b/client/src/game/api.ts
index c23e18e..1e52fcd 100644
--- a/client/src/game/api.ts
+++ b/client/src/game/api.ts
@@ -1,7 +1,7 @@
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
 import { Connection } from '../connection'
 
-interface GameState {
+interface GameInfo {
   title: null|string,
   introduction: null|string,
   worlds: null|{nodes: string[], edges: string[][2]},
@@ -9,6 +9,14 @@ interface GameState {
   conclusion: null|string,
 }
 
+interface LevelInfo {
+  title: null|string,
+  introduction: null|string,
+  index: number,
+  tactics: any[],
+  lemmas: any[]
+}
+
 const customBaseQuery = async (
   args : {method: string, params?: any},
   { signal, dispatch, getState, extra },
@@ -27,12 +35,15 @@ export const gameApi = createApi({
   reducerPath: 'gameApi',
   baseQuery: customBaseQuery,
   endpoints: (builder) => ({
-    getGameInfo: builder.query<GameState, void>({
+    getGameInfo: builder.query<GameInfo, void>({
       query: () => {return {method: 'info', params: {}}},
     }),
+    loadLevel: builder.query<LevelInfo, {world: string, level: number}>({
+      query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}},
+    }),
   }),
 })
 
 // Export hooks for usage in functional components, which are
 // auto-generated based on the defined endpoints
-export const { useGetGameInfoQuery } = gameApi
+export const { useGetGameInfoQuery, useLoadLevelQuery } = gameApi

From b5e1d38341472de91ce49ca4d1950bd8bf554b8c Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 12 Dec 2022 16:34:25 +0100
Subject: [PATCH 2/6] allow hot reloading in level

---
 client/src/components/Level.tsx | 94 +++++++++++++++++----------------
 1 file changed, 48 insertions(+), 46 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 0c7e9e2..8756779 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -7,11 +7,8 @@ import '@fontsource/roboto/700.css';
 import ReactMarkdown from 'react-markdown';
 import { MathJax } from "better-react-mathjax";
 import { Link as RouterLink } from 'react-router-dom';
-
-
 import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
-
 import LeftPanel from './LeftPanel';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
@@ -23,7 +20,6 @@ import './level.css'
 import { ConnectionContext } from '../connection';
 import Infoview from './Infoview';
 import { useParams } from 'react-router-dom';
-import { MonacoServices } from 'monaco-languageclient';
 import { useLoadLevelQuery } from '../game/api';
 
 
@@ -34,9 +30,6 @@ function Level() {
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
 
-  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
-  const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState(null)
   const [expertInfoview, setExpertInfoview] = useState(false)
 
   const codeviewRef = useRef<HTMLDivElement>(null)
@@ -50,6 +43,52 @@ function Level() {
 
   const connection = React.useContext(ConnectionContext)
 
+  const level = useLoadLevelQuery({world: worldId, level: levelId})
+
+  const {editor, infoProvider} = useLevelEditor(worldId, levelId, codeviewRef, infoviewRef)
+
+  return <>
+    <Box style={level.isLoading ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
+    <Grid style={level.isLoading ? {display: "none"} : null} className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
+      <Grid xs={4} className="doc-panel">
+        <LeftPanel spells={level?.data?.tactics} inventory={level?.data?.tactics} />
+      </Grid>
+      <Grid xs={4} className="main-panel">
+        <div ref={messagePanelRef} className="message-panel">
+          <MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
+        </div>
+        <div ref={codeviewRef} className="codeview">
+        </div>
+      </Grid>
+      <Grid xs={4} className="info-panel">
+
+        <Button disabled={levelId <= 1} component={RouterLink} to={`/world/${worldId}/level/${levelId - 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
+        <Button disabled={false} component={RouterLink} to={`/world/${worldId}/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
+
+        <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
+        <div style={{display: expertInfoview ? 'none' : 'block' }}>
+          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
+        </div>
+        <FormGroup>
+          <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />
+        </FormGroup>
+      </Grid>
+    </Grid>
+    </>
+}
+
+export default Level
+
+
+function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef) {
+
+  const connection = React.useContext(ConnectionContext)
+
+  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
+  const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
+  const [infoviewApi, setInfoviewApi] = useState(null)
+
+  // Create Editor
   useEffect(() => {
     const editor = monaco.editor.create(codeviewRef.current!, {
       glyphMargin: true,
@@ -76,11 +115,9 @@ function Level() {
     setInfoProvider(infoProvider)
     setInfoviewApi(infoviewApi)
 
-    return () => { editor.dispose() }
   }, [])
 
-
-  // The next function will be called when the level changes
+  // Create model when level changes
   useEffect(() => {
     connection.startLeanClient().then((leanClient) => {
       if (editor) {
@@ -94,45 +131,10 @@ function Level() {
         infoProvider.openPreview(editor, infoviewApi)
 
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
-
-        return () => { model.dispose(); }
       }
     })
 
   }, [editor, levelId, connection])
 
-
-  const level = useLoadLevelQuery({world: worldId, level: levelId})
-
-  return <>
-    <Box style={level.isLoading ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
-    <Grid style={level.isLoading ? {display: "none"} : null} className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
-      <Grid xs={4} className="doc-panel">
-        <LeftPanel spells={level?.data?.tactics} inventory={level?.data?.tactics} />
-      </Grid>
-      <Grid xs={4} className="main-panel">
-        <div ref={messagePanelRef} className="message-panel">
-          <MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
-        </div>
-        <div ref={codeviewRef} className="codeview">
-        </div>
-      </Grid>
-      <Grid xs={4} className="info-panel">
-
-        <Button disabled={levelId <= 1} component={RouterLink} to={`/world/${worldId}/level/${levelId - 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
-        <Button disabled={false} component={RouterLink} to={`/world/${worldId}/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
-
-        <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
-        <div style={{display: expertInfoview ? 'none' : 'block' }}>
-          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
-        </div>
-        <FormGroup>
-          <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />
-        </FormGroup>
-      </Grid>
-    </Grid>
-    </>
+  return {editor, infoProvider}
 }
-
-export default Level

From cd18884885756928386d2c497000b6cf2b483cd3 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 12 Dec 2022 17:07:37 +0100
Subject: [PATCH 3/6] fix

---
 client/src/components/Level.tsx | 1 +
 1 file changed, 1 insertion(+)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 8756779..534767e 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -115,6 +115,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
     setInfoProvider(infoProvider)
     setInfoviewApi(infoviewApi)
 
+    return () => { editor.setModel(null); infoProvider.dispose(); }
   }, [])
 
   // Create model when level changes

From a5d2242ef95ff98119360d6fdaa75d36fb2c1140 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 12 Dec 2022 17:12:21 +0100
Subject: [PATCH 4/6] add task gutter

---
 client/src/components/Level.tsx | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 534767e..4340ba5 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -10,6 +10,7 @@ import { Link as RouterLink } from 'react-router-dom';
 import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
 import LeftPanel from './LeftPanel';
+import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { InfoProvider } from 'lean4web/client/src/editor/infoview';
@@ -130,6 +131,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
         editor.setModel(model)
         infoviewApi.serverRestarted(leanClient.initializeResult)
         infoProvider.openPreview(editor, infoviewApi)
+        new LeanTaskGutter(infoProvider.client, editor)
 
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
       }

From b2727eef899d912094ac6ba89fe08c19c5f51a6a Mon Sep 17 00:00:00 2001
From: Jon Eugster <Jon.Eugster@hhu.de>
Date: Mon, 12 Dec 2022 14:01:57 +0100
Subject: [PATCH 5/6] toggle hints

---
 client/src/components/TacticState.tsx | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx
index fd96a47..ebebad7 100644
--- a/client/src/components/TacticState.tsx
+++ b/client/src/components/TacticState.tsx
@@ -8,15 +8,22 @@ import { MathJax } from "better-react-mathjax";
 
 import List from '@mui/material/List';
 import ListItem from '@mui/material/ListItem';
-import { Paper, Box, Typography, Alert } from '@mui/material';
-
+import { Paper, Box, Typography, Alert, FormControlLabel, FormGroup, Switch, Collapse } from '@mui/material';
 const errorRegex = /<stdin>:1:(?<col>[^:]*): (?<msg>.*)/;
 
 // TODO: Dead variables (x✝) are not displayed correctly.
 
 function Goal({ goal }) {
+
+  const [showHints, setShowHints] = React.useState(false);
+
+  const handleHintsChange = () => {
+    setShowHints((prev) => !prev);
+  };
+
   const hasObject = typeof goal.objects === "object" && goal.objects.length > 0
   const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0
+  const hasHints = typeof goal.hints === "object" && goal.hints.length > 0
   return (
     <Box sx={{ pl: 2 }}>
       {hasObject && <Box><Typography>Objects</Typography>
@@ -35,7 +42,11 @@ function Goal({ goal }) {
       <Typography>Prove:</Typography>
       <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
       {goal.messages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
-      {goal.hints.map((message) => <Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
+      <FormControlLabel
+        control={<Switch checked={showHints} onChange={handleHintsChange} />}
+        label="Help"
+      />
+      {goal.hints.map((message) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert></Collapse>)}
     </Box>)
 }
 

From 46848d8a93b08a082a1e153eeaaff561d2b50749 Mon Sep 17 00:00:00 2001
From: Jon Eugster <Jon.Eugster@hhu.de>
Date: Mon, 12 Dec 2022 20:54:31 +0100
Subject: [PATCH 6/6] merge addition of Lemma statements

---
 client/src/components/Level.tsx               |  7 ++-
 client/src/components/TacticState.tsx         | 11 +++--
 client/src/components/Welcome.tsx             |  2 +-
 client/src/game/api.ts                        |  4 +-
 server/leanserver/GameServer/Commands.lean    | 46 ++++++++++++++++---
 .../leanserver/GameServer/EnvExtensions.lean  | 12 +++++
 server/leanserver/GameServer/Game.lean        |  4 ++
 server/leanserver/GameServer/RpcHandlers.lean |  4 +-
 server/testgame/TestGame/Levels/Level1.lean   |  2 +-
 server/testgame/TestGame/Levels/Level2.lean   |  2 +-
 server/testgame/TestGame/Levels/Level3.lean   |  2 +-
 server/testgame/TestGame/Levels/Level4.lean   |  2 +-
 server/testgame/TestGame/Levels/Level5.lean   |  2 +-
 .../TestGame/Levels/Logic/L01_Rfl.lean        |  2 +-
 .../Levels/Logic/L03b_Assumption.lean         |  6 +--
 .../TestGame/Levels/Logic/L05_Apply.lean      |  6 +--
 .../TestGame/Levels/Logic/L05b_Apply.lean     |  6 +--
 .../TestGame/Levels/Logic/L05c_Apply.lean     |  1 +
 .../TestGame/Levels/Logic/L06_Iff.lean        |  4 +-
 .../TestGame/Levels/Logic/L06b_Iff.lean       |  4 +-
 .../TestGame/Levels/Logic/L06c_Iff.lean       |  1 +
 .../TestGame/Levels/Logic/L06d_Iff.lean       |  4 +-
 .../TestGame/Levels/Logic/L07_And.lean        |  1 +
 .../TestGame/Levels/Logic/L08_Or.lean         |  2 +-
 .../TestGame/Levels/Logic/L08b_Or.lean        |  1 +
 .../TestGame/Levels/Logic/L08c_Or.lean        |  2 +-
 .../TestGame/Levels/Naturals/L01_Ring.lean    |  2 +-
 .../TestGame/Levels/Naturals/L02_Ring.lean    |  2 +-
 .../TestGame/Levels/Naturals/L03_Exists.lean  |  2 +-
 .../TestGame/Levels/Naturals/L04_Forall.lean  |  2 +-
 .../TestGame/Levels/Naturals/L31_Sum.lean     |  2 +-
 .../Levels/Naturals/L32_Induction.lean        |  2 +-
 .../TestGame/Levels/Naturals/L33_Prime.lean   |  2 +-
 .../Levels/Naturals/L34_ExistsUnique.lean     |  2 +-
 .../TestGame/Levels/Negation/L01_False.lean   |  2 +-
 .../TestGame/Levels/Negation/L02_Contra.lean  |  2 +-
 .../TestGame/Levels/Negation/L03_Contra.lean  |  4 +-
 .../TestGame/Levels/Negation/L04_Contra.lean  |  2 +-
 .../TestGame/Levels/Negation/L05_Not.lean     |  1 +
 .../Levels/Negation/L06_ByContra.lean         |  2 +-
 .../Levels/Negation/L07_Contrapose.lean       |  2 +-
 .../Levels/Negation/L08_Contrapose.lean       |  2 +-
 .../TestGame/Levels/Negation/L09_PushNeg.lean |  4 +-
 43 files changed, 113 insertions(+), 64 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 4340ba5..9ecad39 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -58,8 +58,11 @@ function Level() {
         <div ref={messagePanelRef} className="message-panel">
           <MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
         </div>
-        <div ref={codeviewRef} className="codeview">
-        </div>
+        <p><b>Aufgabe:</b></p>
+        <div><MathJax><ReactMarkdown>{level?.data?.descrText}</ReactMarkdown></MathJax></div>
+        <div className="statement"><code>{level?.data?.descrFormat}</code></div>
+          {/*NOTE(TODO): currently this looks bad, so I disabled it. Maybe have a drop-down for it of Syntax highlighting... */}
+        <div ref={codeviewRef} className="codeview"></div>
       </Grid>
       <Grid xs={4} className="info-panel">
 
diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx
index ebebad7..2ec2428 100644
--- a/client/src/components/TacticState.tsx
+++ b/client/src/components/TacticState.tsx
@@ -42,11 +42,12 @@ function Goal({ goal }) {
       <Typography>Prove:</Typography>
       <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
       {goal.messages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
-      <FormControlLabel
-        control={<Switch checked={showHints} onChange={handleHintsChange} />}
-        label="Help"
-      />
-      {goal.hints.map((message) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert></Collapse>)}
+      {hasHints &&
+        <FormControlLabel
+          control={<Switch checked={showHints} onChange={handleHintsChange} />}
+          label="Help"
+        />}
+        {goal.hints.map((hint) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint}</ReactMarkdown></MathJax></Alert></Collapse>)}
     </Box>)
 }
 
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index fe9f79c..7966c56 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -92,7 +92,7 @@ function Welcome() {
         </Typography>
       </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
-        <Button component={RouterLink} to="/world/TestWorld/level/1" variant="contained">Start rescue mission</Button>
+        <Button component={RouterLink} to="/world/Logic/level/1" variant="contained">Start rescue mission</Button>
       </Box>
       <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
     </div>
diff --git a/client/src/game/api.ts b/client/src/game/api.ts
index 1e52fcd..739b11b 100644
--- a/client/src/game/api.ts
+++ b/client/src/game/api.ts
@@ -14,7 +14,9 @@ interface LevelInfo {
   introduction: null|string,
   index: number,
   tactics: any[],
-  lemmas: any[]
+  lemmas: any[],
+  descrText: null|string,
+  descrFormat: null|string,
 }
 
 const customBaseQuery = async (
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index efb4fa1..dcc398e 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -46,13 +46,47 @@ elab "Introduction" t:str : command => do
   | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
   | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
 
-/-- Define the statement of the current level. -/
-elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
+-- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
+-- us highlighting on the client side.
+partial def reprintCore : Syntax → Option Format
+  | Syntax.missing => none
+  | Syntax.atom _ val => val.trim
+  | Syntax.ident _ rawVal _ _ => rawVal.toString
+  | Syntax.node _ kind args =>
+    match args.toList.filterMap reprintCore with
+    | [] => none
+    | [arg] => arg
+    | args => Format.group <| Format.nest 2 <| Format.joinSep args " "
+
+def reprint (stx : Syntax) : Format :=
+  reprintCore stx |>.getD ""
+
+-- macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
+
+/-- Define the statement of the current level.
+
+Arguments:
+- ident: (Optional) The name of the statemtent.
+- descr: The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
+-/
+elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : command => do
+
   let lvlIdx ← getCurLevelIdx
-  let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String)
-  elabCommand (← `(theorem $(mkIdent declName) $sig $val))
-  modifyCurLevel fun level => pure {level with goal := sig}
--- TODO: Do something with the lemma name.
+  let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
+    ("level" ++ toString lvlIdx : String)
+  let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
+  -- let thmStatement' ← match statementName with
+  -- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
+  -- | some name => `(lemma $name $sig $val)
+
+  elabCommand thmStatement
+  modifyCurLevel fun level => pure {level with
+    goal := sig,
+    descrText := descr.getString,
+    descrFormat := match statementName with
+    | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
+    | some name => (Format.join ["lemma ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10  -- "lemma "  ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
+  } -- Format.pretty <| format thmStatement.raw }
 
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index a437ee6..dac2db9 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -182,6 +182,16 @@ deriving Inhabited
 def getCurLevelId [MonadError m] : m LevelId := do
   return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
 
+/--
+
+
+Fields:
+- TODO
+- introduction: Theory block shown all the time.
+- description:  The mathematical statemtent in mathematician-readable form.
+- goal:         The statement in Lean.
+- conclusion:   Displayed when level is completed.
+-/
 structure GameLevel where
   index: Nat
   title: String := default
@@ -191,6 +201,8 @@ structure GameLevel where
   lemmas: Array LemmaDocEntry := default
   messages: Array GoalMessageEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
+  descrText: String := default
+  descrFormat : String := default
   deriving Inhabited, Repr
 
 /-! ## World -/
diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean
index 0043f3e..c52348c 100644
--- a/server/leanserver/GameServer/Game.lean
+++ b/server/leanserver/GameServer/Game.lean
@@ -35,6 +35,8 @@ structure LevelInfo where
   tactics: Array TacticDocEntry
   lemmas: Array LemmaDocEntry
   introduction : String
+  descrText : String := ""
+  descrFormat : String := ""
 deriving ToJson
 
 structure LoadLevelParams where
@@ -62,6 +64,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
             title := lvl.title,
             tactics := lvl.tactics,
             lemmas := lvl.lemmas,
+            descrText := lvl.descrText,
+            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
             introduction := lvl.introduction }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
       return true
diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
index 97b7f74..3b78810 100644
--- a/server/leanserver/GameServer/RpcHandlers.lean
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -24,8 +24,8 @@ structure GameGoal where
 deriving FromJson, ToJson
 
 
-def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String)
-    (hints : Array String) : MetaM GameGoal := do
+def Lean.MVarId.toGameGoal (goal : MVarId)
+    (messages : Array String) (hints : Array String) : MetaM GameGoal := do
 match (← getMCtx).findDecl? goal with
 | none          => throwError "unknown goal"
 | some mvarDecl => do
diff --git a/server/testgame/TestGame/Levels/Level1.lean b/server/testgame/TestGame/Levels/Level1.lean
index f1cf148..6ec5eac 100644
--- a/server/testgame/TestGame/Levels/Level1.lean
+++ b/server/testgame/TestGame/Levels/Level1.lean
@@ -20,7 +20,7 @@ After closing this message, type rfl in the invocation zone and hit Enter or cli
 the \"Cast spell\" button.
 "
 
-Statement (x y z : ℕ) :  x * y + z = x * y + z := by
+Statement "" (x y z : ℕ) :  x * y + z = x * y + z := by
 rfl
 
 Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button."
diff --git a/server/testgame/TestGame/Levels/Level2.lean b/server/testgame/TestGame/Levels/Level2.lean
index 9201d72..9fd39b1 100644
--- a/server/testgame/TestGame/Levels/Level2.lean
+++ b/server/testgame/TestGame/Levels/Level2.lean
@@ -26,7 +26,7 @@ this substitution using the `rewrite` spell. This spell takes a list of equaliti
 or equivalences so you can cast `rewrite [h]`.
 "
 
-Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
+Statement "" (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
   rewrite [h]
   rfl
 
diff --git a/server/testgame/TestGame/Levels/Level3.lean b/server/testgame/TestGame/Levels/Level3.lean
index 74f3018..7318367 100644
--- a/server/testgame/TestGame/Levels/Level3.lean
+++ b/server/testgame/TestGame/Levels/Level3.lean
@@ -56,7 +56,7 @@ the *right* hand side. Try and figure out how the goal will change, and
 then try it.
 "
 
-Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by
+Statement "" (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by
   rewrite [h]
   rfl
 
diff --git a/server/testgame/TestGame/Levels/Level4.lean b/server/testgame/TestGame/Levels/Level4.lean
index ccad6c9..81ac34e 100644
--- a/server/testgame/TestGame/Levels/Level4.lean
+++ b/server/testgame/TestGame/Levels/Level4.lean
@@ -43,7 +43,7 @@ Observe that the goal mentions `... + succ ...`. So type
 and hit enter; see the goal change.
 "
 
-Statement (a : ℕ ) : a + succ 0 = succ a := by
+Statement "" (a : ℕ ) : a + succ 0 = succ a := by
   rewrite [add_succ]
   rewrite [add_zero]
   rfl
diff --git a/server/testgame/TestGame/Levels/Level5.lean b/server/testgame/TestGame/Levels/Level5.lean
index d302491..c919ea7 100644
--- a/server/testgame/TestGame/Levels/Level5.lean
+++ b/server/testgame/TestGame/Levels/Level5.lean
@@ -64,7 +64,7 @@ The names of the proofs tell you what the theorems are. Anyway, let's prove `0 +
 Start by casting `induction_on n`.
 "
 
-Statement (n : ℕ) : 0 + n = n := by
+Statement "" (n : ℕ) : 0 + n = n := by
   sorry
   -- induction_on n
   -- rewrite [add_zero]
diff --git a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
index 8593cf9..4ed4443 100644
--- a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
@@ -21,7 +21,7 @@ ersten offenen Goal zu machen.
 Wenn der Beweis komplett ist, erscheint \"goals accomplished\".
 "
 
-Statement "Zeige `42 = 42`." : 42 = 42 := by
+Statement "Zeige $ 42 = 42 $." : 42 = 42 := by
   rfl
 
 Message : 42 = 42 =>
diff --git a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
index c5a7e89..d693c49 100644
--- a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
@@ -16,10 +16,8 @@ ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man
 
 -- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
 Statement mehr_triviales
-    "
-    Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`.
-    Zeige, dass `A` wahr ist.
-    "
+    "Sei $ A $ eine logische Aussage und sei `hA` ein Beweis für $A$.
+    Zeige, dass $ A $ wahr ist."
     (A : Prop) (hA : A) : A := by
   assumption
 
diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
index a565449..8291fae 100644
--- a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
@@ -22,10 +22,8 @@ Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `
 "
 
 Statement
-    "
-    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
-    Zeige, dass `B` wahr ist.
-    "
+    "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist."
     (A B : Prop) (hA : A) (g : A → B) : B := by
   apply g
   assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean
index cd04ddf..398de77 100644
--- a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean
@@ -18,10 +18,8 @@ Beweise Aussage `F`.
 "
 
 Statement
-    "
-    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
-    Zeige, dass `B` wahr ist.
-    "
+    "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist."
     (A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E)
      (i : D → E) (k : E → F) (m : C → F) : F := by
   apply k
diff --git a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
index 8c79b34..d184925 100644
--- a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
@@ -16,6 +16,7 @@ und das Goal wird zu `B`.
 "
 
 Statement
+    ""
     (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
   intro hA
   apply g
diff --git a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
index 423f6f6..ab4e558 100644
--- a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
@@ -21,9 +21,7 @@ Gleichungen von natürlichen Zahlen.
 "
 
 Statement
-    "
-    Zeige dass `B ↔ C`.
-    "
+    "Zeige dass `B ↔ C`."
     (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
   rw [h₁]
   rw [←h₂]
diff --git a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
index f2bebfb..0c91995 100644
--- a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
@@ -17,9 +17,7 @@ Wenn das Goal `A ↔ B` ist, kann man mit der `constructor` Taktik, dieses in di
 "
 
 Statement
-    "
-    Zeige dass `B ↔ C`.
-    "
+    "Zeige dass `B ↔ C`."
     (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
   constructor
   assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean
index 12568f5..a3a0394 100644
--- a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean
@@ -20,6 +20,7 @@ man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<`
 
 "
 Statement
+    ""
     (A B : Prop) : (A ↔ B) → (A → B) := by
   intro h
   rcases h
diff --git a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean
index 76365ef..b986b1f 100644
--- a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean
@@ -17,9 +17,7 @@ Implikation `A → B` auf ein Goal `B` anwenden.
 "
 
 Statement
-    "
-    Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen.
-    "
+    "Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen."
     (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
   intro hA
   apply g
diff --git a/server/testgame/TestGame/Levels/Logic/L07_And.lean b/server/testgame/TestGame/Levels/Logic/L07_And.lean
index a5681b3..1af28d7 100644
--- a/server/testgame/TestGame/Levels/Logic/L07_And.lean
+++ b/server/testgame/TestGame/Levels/Logic/L07_And.lean
@@ -20,6 +20,7 @@ Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man
 "
 
 Statement
+    ""
     (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
   constructor
   intro h
diff --git a/server/testgame/TestGame/Levels/Logic/L08_Or.lean b/server/testgame/TestGame/Levels/Logic/L08_Or.lean
index b573a12..e4e6cb1 100644
--- a/server/testgame/TestGame/Levels/Logic/L08_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08_Or.lean
@@ -18,7 +18,7 @@ Wenn das Goal ein `∨` ist kann man mit `left` oder `right` entscheiden,
 welche Seite man beweisen möchte.
 "
 
-Statement (A B : Prop) (hA : A) : A ∨ (¬ B) := by
+Statement "" (A B : Prop) (hA : A) : A ∨ (¬ B) := by
   left
   assumption
 
diff --git a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
index 7d3c3ca..6923ff6 100644
--- a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
@@ -25,6 +25,7 @@ Diese Annahme benennt man dann mit `rcases h with hA | hB`.
 "
 
 Statement
+    ""
     (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by
   rcases h with ⟨ha, hb⟩ | (h | h)
   left
diff --git a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean
index 5fda4e2..a8fa8b0 100644
--- a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean
@@ -16,7 +16,7 @@ Introduction
 "
 
 Statement and_or_imp
-  "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
+    "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
     (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
   rcases h with h₁ | h₂
   left
diff --git a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean
index 599ae11..c0bd94b 100644
--- a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean
@@ -18,7 +18,7 @@ bereits mit `rfl` bewiesen werden können.
 Algemeinere Gleichungen mit Variablen kann man mit der Taktik `ring` lösen.
 "
 
-Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
+Statement "" (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
   ring
 
 Conclusion
diff --git a/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean b/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean
index 3993c56..421393b 100644
--- a/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean
@@ -12,7 +12,7 @@ Introduction
 Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden.
 "
 
-Statement (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
+Statement "" (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
   rw [h]
   ring
 
diff --git a/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean b/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean
index df0b272..0ec946f 100644
--- a/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean
@@ -33,7 +33,7 @@ Hierzu gibt es 3 wichtige Taktiken:
    soll. Das macht man mit `use y`
 "
 
-Statement even_square (n : ℕ) (h : even n) : even (n ^ 2) := by
+Statement even_square "" (n : ℕ) (h : even n) : even (n ^ 2) := by
   unfold even at *
   rcases h with ⟨x, hx⟩
   use 2 * x ^ 2
diff --git a/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean b/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean
index 7175f1d..9fb619e 100644
--- a/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean
@@ -19,7 +19,7 @@ Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
 Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
 "
 
-Statement : ∀ (x : ℕ), (even x) → odd (1 + x) := by
+Statement "" : ∀ (x : ℕ), (even x) → odd (1 + x) := by
   intro x h
   unfold even at h
   unfold odd
diff --git a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean
index ad47fb0..90f0417 100644
--- a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean
@@ -13,7 +13,7 @@ TODO: Summe
 
 "
 
-Statement : True := by
+Statement "" : True := by
   trivial
 
 Conclusion
diff --git a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean
index 9314c64..2e4ce58 100644
--- a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean
@@ -13,7 +13,7 @@ TODO: Induktion (& induktion vs rcases)
 
 "
 
-Statement : True := by
+Statement "" : True := by
   trivial
 
 Conclusion
diff --git a/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean b/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean
index 06592b4..acce168 100644
--- a/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean
@@ -13,7 +13,7 @@ TODO: Primzahl
 
 "
 
-Statement : True := by
+Statement "" : True := by
   trivial
 
 Conclusion
diff --git a/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean
index f669cf2..de45f47 100644
--- a/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean
+++ b/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean
@@ -13,7 +13,7 @@ TODO: Es existiert genau eine gerade Primzahl.
 
 "
 
-Statement : True := by
+Statement "" : True := by
   trivial
 
 Conclusion
diff --git a/server/testgame/TestGame/Levels/Negation/L01_False.lean b/server/testgame/TestGame/Levels/Negation/L01_False.lean
index a2ca589..814307c 100644
--- a/server/testgame/TestGame/Levels/Negation/L01_False.lean
+++ b/server/testgame/TestGame/Levels/Negation/L01_False.lean
@@ -22,7 +22,7 @@ Der einfachste Widerspruch ist wenn man einen Beweis von `false` hat:
 "
 
 Statement
-  "Ein Widerspruch impliziert alles."
+    "Ein Widerspruch impliziert alles."
     (A : Prop) (h : false) : A := by
   contradiction
 
diff --git a/server/testgame/TestGame/Levels/Negation/L02_Contra.lean b/server/testgame/TestGame/Levels/Negation/L02_Contra.lean
index 6a844ea..fa5b14e 100644
--- a/server/testgame/TestGame/Levels/Negation/L02_Contra.lean
+++ b/server/testgame/TestGame/Levels/Negation/L02_Contra.lean
@@ -17,7 +17,7 @@ also `(h : A)` und `(g : ¬ A)`. (`\\not`)
 "
 
 Statement
-  "Ein Widerspruch impliziert alles."
+    "Ein Widerspruch impliziert alles."
     (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 128 := by
   contradiction
 
diff --git a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean b/server/testgame/TestGame/Levels/Negation/L03_Contra.lean
index a7ad661..a7c7e8e 100644
--- a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean
+++ b/server/testgame/TestGame/Levels/Negation/L03_Contra.lean
@@ -22,8 +22,8 @@ Hier musst du zuerst eines der Lemmas `not_odd : ¬ odd n ↔ even n` oder
 "
 
 Statement
-  "Ein Widerspruch impliziert alles."
-  (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
+    "Ein Widerspruch impliziert alles."
+    (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
   rw [← not_even] at h₂
   contradiction
 
diff --git a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean
index 992f977..d22ba56 100644
--- a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean
+++ b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean
@@ -16,7 +16,7 @@ oder auch Annahmen der Form `A ≠ A` (`\\ne`).
 "
 
 Statement
-  "Ein Widerspruch impliziert alles."
+    "Ein Widerspruch impliziert alles."
     (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by
   rw [g₁] at h
   contradiction
diff --git a/server/testgame/TestGame/Levels/Negation/L05_Not.lean b/server/testgame/TestGame/Levels/Negation/L05_Not.lean
index bf1012d..b5abba9 100644
--- a/server/testgame/TestGame/Levels/Negation/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Negation/L05_Not.lean
@@ -15,6 +15,7 @@ wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form
 "
 
 Statement
+    ""
     (A : Prop) : ¬ (¬ A) ↔ A := by
   rw [not_not]
 
diff --git a/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean b/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean
index 4cfd4e2..b8d1962 100644
--- a/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean
@@ -19,7 +19,7 @@ dass das Gegenteil des Goals wahr sei, und dann einen Widerspruch erzeugen.
 "
 
 Statement
-  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
+    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
     (n : ℕ) (h : odd (n ^ 2)) : odd n := by
   by_contra g
   rw [not_odd] at g
diff --git a/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean b/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean
index f273736..b3db2af 100644
--- a/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean
+++ b/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean
@@ -22,7 +22,7 @@ Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
 "
 
 Statement
-  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
     (n : ℕ) : odd (n ^ 2) → odd n := by
   contrapose
   rw [not_odd]
diff --git a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean b/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean
index 50b458f..c08166e 100644
--- a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean
+++ b/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean
@@ -20,7 +20,7 @@ Implikationsannahme ins Goal schreiben.
 "
 
 Statement
-  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
     (n : ℕ) (h : odd (n ^ 2)): odd n := by
   revert h
   contrapose
diff --git a/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean
index c759ba1..3a8f8dd 100644
--- a/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean
+++ b/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean
@@ -17,8 +17,8 @@ mit `push_neg` das `¬` durch den Quantor hindurchschieben.
 "
 
 Statement
-  "Es existiert keine natürliche Zahl, die grösser als alle anderen."
-  : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
+    "Es existiert keine natürliche Zahl, die grösser als alle anderen.":
+    ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
   push_neg
   intro n
   use 3*n + 6