diff --git a/README.md b/README.md
index 65e3ab3..ec4a1a8 100644
--- a/README.md
+++ b/README.md
@@ -113,10 +113,7 @@ Inside the interactive TUI, type `/` followed by a command.
 | Command | Description |
 |---------|-------------|
 | `/new <title>` | Start a new session |
-| `/clear [title]` | Create a new session (alias) |
-| `/resume <session-id>` | Switch to a different session |
-| `/sessions` | List all sessions |
-| `/status` | Current session status |
+| `/resume <session-id>` | Switch to a different session (no args opens picker) |
 
 ### Proving
 
@@ -126,8 +123,9 @@ Inside the interactive TUI, type `/` followed by a command.
 | `/lemma <label> :: <statement>` | Create a lemma node |
 | `/verify` | Trigger Lean verification manually |
 | `/proof` | Show proof state and node tree |
+| `/lean` | Inspect Lean state (scratch file, verification, history) |
 | `/focus <id\|clear>` | Focus on a specific branch or node |
-| `/autonomous start\|stop\|step\|status` | Control autonomous proving loop |
+| `/autonomous start\|full\|stop\|step\|status` | Control autonomous proving loop |
 | `/agent spawn <role> <task>` | Spawn a specific agent (planner, prover, repairer, retriever, critic) |
 
 ### Corpus and sync
@@ -146,12 +144,7 @@ Inside the interactive TUI, type `/` followed by a command.
 | Command | Description |
 |---------|-------------|
 | `/nodes` | List all proof nodes |
-| `/branches` | Show branch status |
-| `/agents` | Show agent status |
-| `/tasks` | Show task queue |
-| `/questions` | Show pending clarification questions |
 | `/answer <option\|text>` | Answer a pending question |
-| `/instructions` | Display AGENTS.md instructions |
 | `/memory` | Show workspace memory |
 | `/remember <text>` | Save to workspace memory |
 | `/remember global <text>` | Save to global memory |
@@ -163,7 +156,6 @@ Inside the interactive TUI, type `/` followed by a command.
 | `/paper` | Display compiled paper |
 | `/export paper\|tex\|lean\|all` | Export proof in various formats |
 | `/dashboard` | Open web dashboard |
-| `/login` | Sync auth credentials |
 
 ## Search strategies
 
diff --git a/crates/openproof-cli/src/slash_commands.rs b/crates/openproof-cli/src/slash_commands.rs
index a43c605..487172d 100644
--- a/crates/openproof-cli/src/slash_commands.rs
+++ b/crates/openproof-cli/src/slash_commands.rs
@@ -1,4 +1,4 @@
-//! Slash-command dispatch (`/help`, `/status`, `/autonomous`, etc.).
+//! Slash-command dispatch (`/help`, `/new`, `/autonomous`, etc.).
 //!
 //! All `/command` strings entered by the user flow through
 //! `apply_local_command`.  Each command arm is self-contained: it reads from
@@ -43,21 +43,15 @@ pub fn apply_local_command(
                 "Help",
                 [
                     "/help",
-                    "/status",
                     "/new <title>",
-                    "/clear [title]",
                     "/resume <session-id>",
                     "/nodes",
-                    "/branches",
-                    "/agents",
-                    "/tasks",
                     "/focus <branch-id|node-id|clear>",
                     "/agent spawn <role> <task>",
                     "/proof",
+                    "/lean",
                     "/paper",
-                    "/questions",
                     "/answer <option-id|text>",
-                    "/instructions",
                     "/memory",
                     "/remember <text>",
                     "/remember global <text>",
@@ -66,30 +60,16 @@ pub fn apply_local_command(
                     "/corpus status|search <query>|ingest|recluster",
                     "/sync status|enable|disable|drain",
                     "/export paper|tex|lean|all",
-                    "/autonomous status|start|stop|step",
+                    "/autonomous status|start|full|stop|step",
                     "/theorem <label> :: <statement>",
                     "/lemma <label> :: <statement>",
                     "/verify",
-                    "/login",
                     "/dashboard",
-                    "/sessions",
-                    "Tab focuses panes. Enter sends. q quits.",
+                    "Tab focuses panes. Enter sends. Ctrl+C quits.",
                 ]
                 .join("\n"),
             );
         }
-        "/status" => {
-            emit_local_notice(tx, state, store, "Status", state.status_report());
-        }
-        "/branches" => {
-            emit_local_notice(tx, state, store, "Branches", state.branches_report());
-        }
-        "/agents" => {
-            emit_local_notice(tx, state, store, "Agents", state.agents_report());
-        }
-        "/tasks" => {
-            emit_local_notice(tx, state, store, "Tasks", state.tasks_report());
-        }
         "/new" => {
             let write = state.create_session(if arg_text.is_empty() {
                 None
@@ -111,27 +91,6 @@ pub fn apply_local_command(
                 ),
             );
         }
-        "/clear" => {
-            let write = state.create_session(if arg_text.is_empty() {
-                None
-            } else {
-                Some(arg_text)
-            });
-            persist_write(tx.clone(), store.clone(), write);
-            emit_local_notice(
-                tx,
-                state,
-                store,
-                "Session",
-                format!(
-                    "Cleared into new session: {}.",
-                    state
-                        .current_session()
-                        .map(|session| session.title.clone())
-                        .unwrap_or_else(|| "OpenProof Rust Session".to_string())
-                ),
-            );
-        }
         "/resume" => {
             if arg_text.is_empty() {
                 state.overlay = Some(openproof_core::Overlay::SessionPicker {
@@ -322,24 +281,6 @@ pub fn apply_local_command(
                 emit_local_notice(tx, state, store, "Paper", "No active session.".to_string());
             }
         }
-        "/questions" => {
-            emit_local_notice(
-                tx,
-                state,
-                store,
-                "Questions",
-                state.pending_question_report(),
-            );
-        }
-        "/instructions" => {
-            let context = crate::system_prompt::load_prompt_context();
-            let content = if context.instructions.trim().is_empty() {
-                "No AGENTS.md instructions loaded.".to_string()
-            } else {
-                context.instructions
-            };
-            emit_local_notice(tx, state, store, "Instructions", content);
-        }
         "/memory" => {
             let context = crate::system_prompt::load_prompt_context();
             let content = if context.memory.trim().is_empty() {
@@ -420,15 +361,6 @@ pub fn apply_local_command(
         "/theorem" => apply_statement_command(tx, state, store, ProofNodeKind::Theorem, arg_text),
         "/lemma" => apply_statement_command(tx, state, store, ProofNodeKind::Lemma, arg_text),
         "/verify" => start_verify_active_node(tx, state, store),
-        "/login" => {
-            emit_local_notice(
-                tx,
-                state,
-                store,
-                "Login",
-                "Use `openproof login` from another shell to import the current Codex ChatGPT login.".to_string(),
-            );
-        }
         "/dashboard" => {
             let store_dash = store.clone();
             let tx_dash = tx.clone();
@@ -455,11 +387,6 @@ pub fn apply_local_command(
                 }
             });
         }
-        "/sessions" => {
-            state.overlay = Some(openproof_core::Overlay::SessionPicker {
-                selected: state.selected_session,
-            });
-        }
         _ => {
             emit_local_notice(
                 tx,
diff --git a/crates/openproof-core/src/commands.rs b/crates/openproof-core/src/commands.rs
index b6ecc6a..33f8fb7 100644
--- a/crates/openproof-core/src/commands.rs
+++ b/crates/openproof-core/src/commands.rs
@@ -3,21 +3,15 @@ use crate::state::AppState;
 /// All known slash commands for tab completion.
 pub const SLASH_COMMANDS: &[&str] = &[
     "help",
-    "status",
     "new",
-    "clear",
     "resume",
     "nodes",
-    "branches",
-    "agents",
-    "tasks",
     "focus",
     "agent spawn",
     "proof",
+    "lean",
     "paper",
-    "questions",
     "answer",
-    "instructions",
     "memory",
     "remember",
     "share",
@@ -35,14 +29,13 @@ pub const SLASH_COMMANDS: &[&str] = &[
     "export all",
     "autonomous status",
     "autonomous start",
+    "autonomous full",
     "autonomous stop",
     "autonomous step",
     "theorem",
     "lemma",
     "verify",
-    "login",
     "dashboard",
-    "sessions",
 ];
 
 /// Compute tab completions for the current command buffer.