diff --git a/client/src/app.tsx b/client/src/app.tsx
index b194b5a1..3cb91662 100644
--- a/client/src/app.tsx
+++ b/client/src/app.tsx
@@ -8,7 +8,8 @@ import '@fontsource/roboto/700.css';
 
 import './css/reset.css';
 import './css/app.css';
-import { PreferencesContext, WorldLevelIdContext} from './components/infoview/context';
+import { HistoryContext, PreferencesContext, WorldLevelIdContext} from './components/infoview/context';
+import { NO_HISTORY_INDEX } from './components/infoview/typewriter';
 import UsePreferences from "./state/hooks/use_preferences"
 import i18n from './i18n';
 import { Popup } from './components/popup/popup';
@@ -24,6 +25,9 @@ function App() {
 
   const {mobile, layout, isSavePreferences, language, isSuggestionsMobileMode, setLayout, setIsSavePreferences, setLanguage, setIsSuggestionsMobileMode} = UsePreferences()
 
+  // Typewriter history state (persists across game levels)
+  const [history, setHistory] = React.useState<string[]>([])
+
   React.useEffect(() => {
     i18n.changeLanguage(language)
   }, [language])
@@ -33,10 +37,12 @@ function App() {
       <GameIdContext.Provider value={gameId}>
           <WorldLevelIdContext.Provider value={{worldId, levelId}}>
           <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, language, isSuggestionsMobileMode, setLayout, setIsSavePreferences, setLanguage, setIsSuggestionsMobileMode}}>
-            <React.Suspense>
-              <Outlet />
-            </React.Suspense>
-            <Popup />
+            <HistoryContext.Provider value={{history, setHistory}}>
+              <React.Suspense>
+                <Outlet />
+              </React.Suspense>
+              <Popup />
+            </HistoryContext.Provider>
           </PreferencesContext.Provider>
           </WorldLevelIdContext.Provider>
       </GameIdContext.Provider>
diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts
index 598e13a8..5d55bea2 100644
--- a/client/src/components/infoview/context.ts
+++ b/client/src/components/infoview/context.ts
@@ -7,6 +7,7 @@ import { InteractiveDiagnostic } from '@leanprover/infoview-api';
 import { Diagnostic } from 'vscode-languageserver-types'
 import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';
+import { NO_HISTORY_INDEX } from './typewriter';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
   null as any)
@@ -126,6 +127,14 @@ export const DeletedChatContext = React.createContext<{
   setShowHelp: () => {}
 })
 
+export const HistoryContext = React.createContext<{
+  history: string[],
+  setHistory: React.Dispatch<React.SetStateAction<string[]>>,
+}>({
+  history: [],
+  setHistory: () => {},
+});
+
 export const InputModeContext = React.createContext<{
   typewriterMode: boolean,
   setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
@@ -133,6 +142,10 @@ export const InputModeContext = React.createContext<{
   setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
   lockEditorMode: boolean,
   setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
+  historyIndex: number,
+  setHistoryIndex: React.Dispatch<React.SetStateAction<number>>,
+  tempInput: string,
+  setTempInput: React.Dispatch<React.SetStateAction<string>>,
 }>({
   typewriterMode: true,
   setTypewriterMode: () => {},
@@ -140,6 +153,10 @@ export const InputModeContext = React.createContext<{
   setTypewriterInput: () => {},
   lockEditorMode: false,
   setLockEditorMode: () => {},
+  historyIndex: NO_HISTORY_INDEX,
+  setHistoryIndex: () => {},
+  tempInput: "",
+  setTempInput: () => {},
 });
 
 
diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
index 7425ffd9..572c88e8 100644
--- a/client/src/components/infoview/typewriter.tsx
+++ b/client/src/components/infoview/typewriter.tsx
@@ -17,11 +17,14 @@ import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } fro
 import { Diagnostic } from 'vscode-languageserver-types';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { DeletedChatContext, InputModeContext, MonacoEditorContext, PreferencesContext, ProofContext, WorldLevelIdContext } from './context'
+import { DeletedChatContext, HistoryContext, InputModeContext, MonacoEditorContext, PreferencesContext, ProofContext, WorldLevelIdContext } from './context'
 import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
 import { GameHint, ProofState } from './rpc_api'
 import { useTranslation } from 'react-i18next'
 
+/* Constant for historyIndex, indicating navigation is not active */
+export const NO_HISTORY_INDEX = -1;
+
 export interface GameDiagnosticsParams {
   uri: DocumentUri;
   diagnostics: Diagnostic[];
@@ -89,7 +92,9 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
-  const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
+  // Typewriter state from consolidated context
+  const {history, setHistory} = React.useContext(HistoryContext);
+  const {typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode, historyIndex, setHistoryIndex, tempInput, setTempInput} = React.useContext(InputModeContext)
 
   const inputRef = useRef<HTMLDivElement>()
 
@@ -110,6 +115,15 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
 
     const pos = editor.getPosition()
     if (typewriterInput) {
+      // Add to history if not empty and not duplicate of last entry
+      const trimmed = typewriterInput.trim();
+      if (trimmed) {
+        setHistory(prev => {
+          const filtered = prev.filter(item => item !== trimmed)
+          return [...filtered, trimmed].slice(-100) // Keep last 100 commands
+        })
+      }
+
       setProcessing(true)
       editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
@@ -120,6 +134,8 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
         forceMoveMarkers: false
       }])
       setTypewriterInput('')
+      setHistoryIndex(NO_HISTORY_INDEX)
+      setTempInput('')
       // Load proof after executing edits
       loadGoals(rpcSess, uri, worldId, levelId, setProof, setCrashed)
     }
@@ -253,14 +269,41 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
 
   useEffect(() => {
     if (!oneLineEditor) return
-    // Run command when pressing enter
+    // Run command when pressing enter and handle history navigation
     const l = oneLineEditor.onKeyUp((ev) => {
       if (ev.code === "Enter" || ev.code === "NumpadEnter") {
         runCommand()
+      } else if (ev.code === "ArrowUp") {
+        // Navigate up in history
+        if (history.length > 0) {
+          if (historyIndex === NO_HISTORY_INDEX) {
+            // Save current input and go to last history item
+            setTempInput(typewriterInput)
+            setHistoryIndex(history.length - 1)
+            setTypewriterInput(history[history.length - 1])
+          } else if (historyIndex > 0) {
+            // Go to previous history item
+            setHistoryIndex(historyIndex - 1)
+            setTypewriterInput(history[historyIndex - 1])
+          }
+        }
+      } else if (ev.code === "ArrowDown") {
+        // Navigate down in history
+        if (historyIndex !== NO_HISTORY_INDEX) {
+          if (historyIndex < history.length - 1) {
+            // Go to next history item
+            setHistoryIndex(historyIndex + 1)
+            setTypewriterInput(history[historyIndex + 1])
+          } else {
+            // Return to current input
+            setHistoryIndex(NO_HISTORY_INDEX)
+            setTypewriterInput(tempInput)
+          }
+        }
       }
     })
     return () => { l.dispose() }
-  }, [oneLineEditor, runCommand])
+  }, [oneLineEditor, runCommand, history, historyIndex, typewriterInput, tempInput])
 
   // BUG: Causes `file closed` error
   //TODO: Intention is to run once when loading, does that work?
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 662d0f3c..4685099a 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -26,7 +26,7 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl
 import { store } from '../state/store'
 import { Button } from './button'
 import { Markdown } from './markdown'
-import { hasInteractiveErrors } from './infoview/typewriter'
+import { NO_HISTORY_INDEX, hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
   ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
@@ -233,9 +233,10 @@ function PlayableLevel() {
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
 
-  // set to true to prevent switching between typewriter and editor
   const [lockEditorMode, setLockEditorMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
+  const [tempInput, setTempInput] = useState("")
+  const [historyIndex, setHistoryIndex] = useState(NO_HISTORY_INDEX)
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
 
   // When clicking on an inventory item, the inventory is overlayed by the item's doc.
@@ -396,7 +397,7 @@ function PlayableLevel() {
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode, historyIndex, setHistoryIndex, tempInput, setTempInput}}>
           <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>