diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx
index 2df97d6..b98dbc2 100644
--- a/client/src/components/hints.tsx
+++ b/client/src/components/hints.tsx
@@ -91,12 +91,14 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
   const {proof, setProof} = React.useContext(ProofContext)
   const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
 
-  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected
+  let k = proof?.steps.length ?
+    ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
+    : 0
 
   const activateHiddenHints = (ev) => {
     // If the last step (`k`) has errors, we want the hidden hints from the
     // second-to-last step to be affected
-    if (!(proof.steps.length)) {return}
+    if (!(proof?.steps.length)) {return}
 
     // state must not be mutated, therefore we need to clone the set
     let tmp = new Set(showHelp)
@@ -109,7 +111,7 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
     console.debug(`help: ${Array.from(tmp.values())}`)
   }
 
-  if (hasHiddenHints(proof.steps[k]) && !showHelp.has(k)) {
+  if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
     return <Button to="" onClick={activateHiddenHints}>
       Show more help!
     </Button>
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index d5b5648..decf9ec 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -67,7 +67,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
   const dispatch = useAppDispatch()
 
   React.useEffect(() => {
-    if (proof.completed) {
+    if (proof?.completed) {
       dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
 
       // On completion, add the names of all new items to the local storage
@@ -232,16 +232,16 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
     ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
   } else {
     ret = <div className="infoview vscode-light">
-      {proof.completedWithWarnings &&
+      {proof?.completedWithWarnings &&
         <div className="level-completed">
-          {proof.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
+          {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
         </div>
       }
       <Infos />
-      <Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints}
+      <Hints hints={proof?.steps[curPos?.line]?.goals[0]?.hints}
         showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
         selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
-        lastLevel={curPos?.line == proof.steps.length - 1}/>
+        lastLevel={curPos?.line == proof?.steps.length - 1}/>
       <MoreHelpButton selected={curPos?.line}/>
     </div>
   }
@@ -266,11 +266,11 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
     // If the last step has errors, we display the command in a different style
     // indicating that it will be removed on the next try.
     return <div className="failed-command">
-      <i>Failed command</i>: {proof.steps[i].command}
+      <i>Failed command</i>: {proof?.steps[i].command}
     </div>
   } else {
     return <div className="command">
-      <div className="command-text">{proof.steps[i].command}</div>
+      <div className="command-text">{proof?.steps[i].command}</div>
       <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
         <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
       </Button>
@@ -414,7 +414,7 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      proof.steps.slice(line).map((step, i) => {
+      proof?.steps.slice(line).map((step, i) => {
         let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
 
         // Only add these hidden hints to the deletion stack which were visible
@@ -431,7 +431,7 @@ export function TypewriterInterface({props}) {
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
-      setTypewriterInput(proof.steps[line].command)
+      setTypewriterInput(proof?.steps[line].command)
       // Reload proof on deleting
       loadGoals(rpcSess, uri, setProof)
       ev.stopPropagation()
@@ -453,7 +453,7 @@ export function TypewriterInterface({props}) {
 
    // Scroll to the end of the proof if it is updated.
    React.useEffect(() => {
-    if (proof.steps.length > 1) {
+    if (proof?.steps.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {
       proofPanelRef.current?.scrollTo(0,0)
@@ -475,7 +475,7 @@ export function TypewriterInterface({props}) {
   }, [selectedStep])
 
   // TODO: superfluous, can be replaced with `withErr` from above
-  let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false
+  let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -495,12 +495,12 @@ export function TypewriterInterface({props}) {
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
-        {proof.steps.length ?
+        {proof?.steps.length ?
           <>
-            {proof.steps.map((step, i) => {
+            {proof?.steps.map((step, i) => {
               let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
 
-              // if (i == proof.steps.length - 1 && hasInteractiveErrors(step.diags)) {
+              // if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) {
               //   // if the last command contains an error, we only display the errors but not the
               //   // entered command as it is still present in the command line.
               //   // TODO: Should not use index as key.
@@ -521,18 +521,18 @@ export function TypewriterInterface({props}) {
                       hints={filteredHints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                   }
-                  {/* <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
+                  {/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
                   {!(isLastStepWithErrors(proof, i)) &&
-                    <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+                    <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
                   }
-                  {mobile && i == proof.steps.length - 1 &&
+                  {mobile && i == proof?.steps.length - 1 &&
                     <MoreHelpButton />
                   }
 
                   {/* Show a message that there are no goals left */}
                   {/* {!step.goals.length && (
                     <div className="message information">
-                      {proof.completed ?
+                      {proof?.completed ?
                         <p>Level completed! 🎉</p> :
                         <p>
                           <b>no goals left</b><br />
@@ -545,12 +545,12 @@ export function TypewriterInterface({props}) {
               }
             //}
             )}
-            {proof.diagnostics.length > 0 &&
+            {proof?.diagnostics.length > 0 &&
               <div key={`proof-step-remaining`} className="step step-remaining">
-                <Errors errors={proof.diagnostics} typewriterMode={true} />
+                <Errors errors={proof?.diagnostics} typewriterMode={true} />
               </div>
             }
-            {mobile && proof.completed &&
+            {mobile && proof?.completed &&
               <div className="button-row mobile">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
@@ -567,7 +567,7 @@ export function TypewriterInterface({props}) {
         }
       </div>
     </div>
-    <Typewriter disabled={disableInput || !proof.steps.length}/>
+    <Typewriter disabled={disableInput || !proof?.steps.length}/>
     </RpcContext.Provider>
   </div>
 }
diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
index e457af0..2b50a69 100644
--- a/client/src/components/infoview/typewriter.tsx
+++ b/client/src/components/infoview/typewriter.tsx
@@ -230,7 +230,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   /** If the last step has an error, add the command to the typewriter. */
   useEffect(() => {
     if (lastStepHasErrors(proof)) {
-      setTypewriterInput(proof.steps[proof.steps.length - 1].command)
+      setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
     }
   }, [proof])
 
@@ -344,7 +344,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   }
 
   // do not display if the proof is completed (with potential warnings still present)
-  return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
+  return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
       <form onSubmit={handleSubmit}>
         <div className="typewriter-input-wrapper">
           <div ref={inputRef} className="typewriter-input" />
@@ -376,10 +376,10 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
 export function getInteractiveDiagsAt (proof: ProofState, k : number) {
   if (k == 0) {
     return []
-  } else if (k >= proof.steps.length-1) {
+  } else if (k >= proof?.steps.length-1) {
     // TODO: Do we need that?
-    return proof.diagnostics.filter(msg => msg.range.start.line >= proof.steps.length-1)
+    return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1)
   } else {
-    return proof.diagnostics.filter(msg => msg.range.start.line == k-1)
+    return proof?.diagnostics.filter(msg => msg.range.start.line == k-1)
   }
 }
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 5b28376..ae3c9bd 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -84,7 +84,7 @@ function ChatPanel({lastLevel, visible = true}) {
   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
+  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -129,27 +129,27 @@ function ChatPanel({lastLevel, visible = true}) {
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {proof.steps.map((step, i) => {
+      {proof?.steps.map((step, i) => {
         let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
         if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
           return <Hints key={`hints-${i}`}
           hints={filteredHints} showHidden={showHelp.has(i)} step={i}
-          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
+          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
         }
       })}
 
       {/* {modifiedHints.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
-        if (!(i == proof.steps.length - 1 && withErr)) {
+        if (!(i == proof?.steps.length - 1 && withErr)) {
           // TODO: Should not use index as key.
           return <Hints key={`hints-${i}`}
             hints={step} showHidden={showHelp.has(i)} step={i}
-            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
         }
       })} */}
       <DeletedHints hints={deletedChat}/>
-      {proof.completed &&
+      {proof?.completed &&
         <>
           <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
             Level completed! 🎉
@@ -163,7 +163,7 @@ function ChatPanel({lastLevel, visible = true}) {
       }
     </div>
     <div className="button-row">
-      {proof.completed && (lastLevel ?
+      {proof?.completed && (lastLevel ?
         <Button to={`/${gameId}`}>
           <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
         </Button> :
@@ -334,15 +334,15 @@ function PlayableLevel({impressum, setImpressum}) {
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
-    if (proof.steps.length) {
+    if (proof?.steps.length) {
       console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof?.steps.length))))
     }
   }, [proof])
 
   // save showed help in store
   useEffect(() => {
-    if (proof.steps.length) {
+    if (proof?.steps.length) {
       console.debug(`showHelp:\n ${showHelp}`)
       dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
     }