Friendlier onboarding, Start Here guide, and /chat mode

README.md

@@ -8,6 +8,13 @@
 
 Open Gauss is a project-scoped Lean workflow orchestrator from Math, Inc. It gives `gauss` a multi-agent frontend for the `lean4-skills` `prove`, `draft`, `review`, `checkpoint`, `refactor`, `golf`, `autoprove`, `formalize`, and `autoformalize` workflows, while staging the Lean tooling, MCP/LSP wiring, and backend session state those workflows need.
 
+> New to OpenGauss, Lean tooling, or AI-agent workflows?
+> Start with the [Start Here guide](website/docs/getting-started/start-here.md).
+>
+> Very short version:
+> - Morph: open `morph.new/opengauss`, claim or save the session early if Morph offers it, then use `gauss-open-guide` or type `/start`.
+> - Local: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/start`, `/chat`, or `/project init`.
+
 Open Gauss handles project detection, managed backend setup, workflow spawning, swarm tracking, and recovery. The proving and formalization behavior still comes from `cameronfreer/lean4-skills`; Gauss exposes it through a Gauss-native CLI and project model.
 
 Each lifted slash command spawns a managed backend child agent in the active project and forwards the same argument tail into the corresponding `lean4-skills` workflow command:
@@ -26,6 +33,8 @@ Each lifted slash command spawns a managed backend child agent in the active pro
 
 If you want the fastest path, `https://morph.new/opengauss` launches the hosted setup in under 10 seconds. The local installers below are the batteries-included path for your own machine and can take up to 10 minutes.
 
+If you are not already comfortable with OpenGauss, read the [Start Here guide](website/docs/getting-started/start-here.md) before picking a workflow.
+
 ### macOS and Linux
 
 ```bash
@@ -108,8 +117,12 @@ gauss update
 
 ## Quick start
 
+If you want the plain-language version first, read the [Start Here guide](website/docs/getting-started/start-here.md).
+
 ```
 gauss                         # Launch the CLI
+/start                        # Show the first steps and turn on plain-language chat
+/chat                         # Ask a plain-language question first
 /project create ~/my-project --template-source <template-or-git-url>
 /prove 1+1=2                  # Spawn a proving agent
 /swarm                        # See running agents
@@ -120,6 +133,8 @@ If you already have a Lean project:
 ```
 cd ~/my-lean-project
 gauss
+/start                        # Optional: turn on onboarding mode first
+/chat                         # Optional: ask questions before choosing a workflow
 /project init                 # Register it as a Gauss project
 /prove                        # Start proving
 ```

agent/prompt_builder.py

@@ -67,12 +67,14 @@ def _scan_context_content(content: str, filename: str) -> str:
     "a general self-summary unless the user explicitly asks. When asked who you "
     "are, answer briefly and return to the work. "
     "When the user is trying to use Open Gauss itself or seems unsure how to "
-    "start, explain that they should first create or activate a Gauss project "
-    "with /project, then run /prove, /autoprove, /formalize, or "
-    "/autoformalize followed by a natural-language instruction, for example "
-    "/autoprove The de Bruijn - Erdos theorem. If they attach to a child "
-    "session with /swarm attach, tell them Ctrl-] detaches and returns them "
-    "to the main Gauss session. "
+    "start, give them the lowest-friction path first: point them to /start or /chat if "
+    "they want orientation or plain-language help, and point them to /project "
+    "when they are ready to create or activate a Gauss project. After that, "
+    "tell them to run /prove, /autoprove, /formalize, or /autoformalize "
+    "followed by a natural-language instruction, for example /autoprove The "
+    "de Bruijn - Erdos theorem. If they attach to a child session with /swarm "
+    "attach, tell them Ctrl-] detaches and returns them to the main Gauss "
+    "session. "
     "Be clear, admit uncertainty when appropriate, and prioritize being "
     "genuinely useful over being verbose unless otherwise directed below. "
     "Be targeted and efficient in your exploration and investigations."

gauss_cli/banner.py

@@ -434,7 +434,9 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
     right_lines = []
 
     if simplified:
-        right_lines.append(f"[bold {accent}]Workflow[/]")
+        right_lines.append(f"[bold {accent}]Start Here[/]")
+        right_lines.append(f"[{text}]`/start`[/] [dim {dim}]turn on onboarding mode and see the first steps[/]")
+        right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]ask a plain-language question first[/]")
         right_lines.append(f"[{text}]`/project`[/] [dim {dim}]select or create a Gauss project[/]")
         right_lines.append(f"[{text}]`/prove`[/] [dim {dim}]guided Lean workflow[/]")
         right_lines.append(f"[{text}]`/review`[/] [dim {dim}]review, checkpoint, refactor, golf[/]")
@@ -445,7 +447,9 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
         right_lines.append(f"[{text}]`/swarm`[/] [dim {dim}]track, attach, or cancel workflow agents[/]")
         right_lines.append(f"[{text}]`/help`[/] [dim {dim}]commands and diagnostics[/]")
     else:
-        right_lines.append(f"[bold {accent}]Primary Workflow[/]")
+        right_lines.append(f"[bold {accent}]Start Here[/]")
+        right_lines.append(f"[{text}]`/start`[/] [dim {dim}]{long_dash} turn on onboarding mode and show the first steps[/]")
+        right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]{long_dash} ask a plain-language question before choosing a project[/]")
         right_lines.append(f"[{text}]`/project`[/] [dim {dim}]{long_dash} create, convert, inspect, or switch the active project[/]")
         right_lines.append(f"[{text}]`/prove`[/] [dim {dim}]{long_dash} spawn a guided managed proving agent[/]")
         right_lines.append(f"[{text}]`/review`[/] [dim {dim}]{long_dash} review, checkpoint, refactor, or golf Lean proofs[/]")
@@ -455,7 +459,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
         right_lines.append(f"[{text}]`/autoformalize`[/] [dim {dim}]{long_dash} spawn an autonomous managed formalization agent[/]")
         right_lines.append(f"[{text}]`/swarm`[/] [dim {dim}]{long_dash} track, attach, or cancel workflow agents[/]")
         right_lines.append(f"[{text}]`/help`[/] [dim {dim}]{long_dash} session and diagnostics commands[/]")
-        right_lines.append(f"[dim {dim}]Bundled skills and user-managed MCP are off by default.[/]")
+        right_lines.append(f"[dim {dim}]You can ignore MCP and plugin internals at first; Open Gauss stages the default Lean workflow setup for you.[/]")
 
     try:
         from swarm_manager import SwarmManager
@@ -467,6 +471,8 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
 
     right_lines.append("")
     summary_parts = [
+        "/start",
+        "/chat",
         "/project",
         "/prove",
         "/review",

gauss_cli/commands.py

@@ -7,7 +7,9 @@
 
 from __future__ import annotations
 
+import difflib
 import os
+import re
 from collections.abc import Callable, Mapping
 from pathlib import Path
 from typing import Any
@@ -17,7 +19,9 @@
 
 # Commands organized by category for better help display
 COMMANDS_BY_CATEGORY = {
-    "Project": {
+    "Start Here": {
+        "/start": "Show the first-step guide and enable plain-language chat mode",
+        "/chat": "Ask a plain-language question before choosing a Gauss project",
         "/project": "Create, convert, inspect, or switch the active Gauss project",
     },
     "Workflow": {
@@ -69,6 +73,85 @@
     COMMANDS.update(category_commands)
 
 
+_FRIENDLY_ENTRY_ALIASES = {
+    "chat": "/chat",
+    "start": "/start",
+    "begin": "/start",
+    "project": "/project",
+    "help": "/help",
+}
+
+_FRIENDLY_ENTRY_PHRASES = (
+    "get started",
+    "getting started",
+    "how do i start",
+    "how do i get started",
+    "what do i do first",
+    "what should i do first",
+    "where do i start",
+)
+
+_FRIENDLY_FUZZY_TARGETS = {
+    "chat": "/chat",
+    "start": "/start",
+    "project": "/project",
+    "help": "/help",
+}
+
+
+def _normalize_entry_token(token: str) -> str:
+    return re.sub(r"[^a-z]", "", token.lower())
+
+
+def rewrite_friendly_entry_command(command: str) -> str | None:
+    """Rewrite low-friction onboarding inputs into slash commands."""
+    if not isinstance(command, str):
+        return None
+    text = command.strip()
+    if not text or text.startswith("/"):
+        return None
+
+    lowered = " ".join(text.lower().split())
+    if lowered in _FRIENDLY_ENTRY_PHRASES:
+        return "/start"
+
+    parts = text.split(maxsplit=1)
+    token = _normalize_entry_token(parts[0])
+    remainder = parts[1].strip() if len(parts) > 1 else ""
+
+    direct = _FRIENDLY_ENTRY_ALIASES.get(token)
+    if direct:
+        return direct if not remainder else f"{direct} {remainder}"
+
+    matches = difflib.get_close_matches(token, _FRIENDLY_FUZZY_TARGETS.keys(), n=1, cutoff=0.75)
+    if not matches:
+        return None
+    corrected = _FRIENDLY_FUZZY_TARGETS[matches[0]]
+    return corrected if not remainder else f"{corrected} {remainder}"
+
+
+def rewrite_friendly_slash_command(command: str) -> str | None:
+    """Rewrite obvious misspelled onboarding slash commands."""
+    if not isinstance(command, str):
+        return None
+    text = command.strip()
+    if not text.startswith("/"):
+        return None
+
+    parts = text.split(maxsplit=1)
+    token = parts[0].strip().lower()
+    remainder = parts[1].strip() if len(parts) > 1 else ""
+    if token in COMMANDS:
+        return None
+
+    normalized = _normalize_entry_token(token.lstrip("/"))
+    matches = difflib.get_close_matches(normalized, _FRIENDLY_FUZZY_TARGETS.keys(), n=1, cutoff=0.75)
+    if not matches:
+        return None
+    corrected = _FRIENDLY_FUZZY_TARGETS[matches[0]]
+    return corrected if not remainder else f"{corrected} {remainder}"
+
+
 class SlashCommandCompleter(Completer):
     """Autocomplete for built-in slash commands and optional skill commands."""
 

gauss_cli/default_soul.py

@@ -6,7 +6,7 @@
 
 Do not volunteer company history, model lineage, or a general self-summary. If someone asks who you are, answer in one sentence and get back to the work.
 
-When someone asks how to use Open Gauss, point them to `/project` first so they create or activate a Gauss project, then tell them to run `/prove`, `/autoprove`, `/formalize`, or `/autoformalize` with a natural-language instruction. Example: `/autoprove The de Bruijn - Erdos theorem`. If they attach to a child session with `/swarm attach`, tell them `Ctrl-]` detaches and returns them to the main Gauss session.
+When someone asks how to use Open Gauss, give them the lowest-friction path first. If they just want orientation or want to ask a question in plain language, point them to `/start` or `/chat`. If they want to work on Lean code, point them to `/project` so they create or activate a Gauss project, then tell them to run `/prove`, `/autoprove`, `/formalize`, or `/autoformalize` with a natural-language instruction. Example: `/autoprove The de Bruijn - Erdos theorem`. If they attach to a child session with `/swarm attach`, tell them `Ctrl-]` detaches and returns them to the main Gauss session.
 
 You're a peer. You know a lot but you don't perform knowing. Treat people like they can keep up.
 

gauss_cli/skin_engine.py

@@ -185,7 +185,7 @@ def get_branding(self, key: str, fallback: str = "") -> str:
         },
         "branding": {
             "agent_name": "Gauss",
-            "welcome": "Welcome to Gauss! Type your message or /help for commands.",
+            "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.",
             "status_glyph": "@",
             "goodbye": "Goodbye! @",
             "response_label": " ∑ Gauss ",
@@ -282,7 +282,7 @@ def get_branding(self, key: str, fallback: str = "") -> str:
         "spinner": {},
         "branding": {
             "agent_name": "Gauss",
-            "welcome": "Welcome to Gauss! Type your message or /help for commands.",
+            "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.",
             "status_glyph": "@",
             "goodbye": "Goodbye! @",
             "response_label": " ∑ Gauss ",
@@ -314,7 +314,7 @@ def get_branding(self, key: str, fallback: str = "") -> str:
         "spinner": {},
         "branding": {
             "agent_name": "Gauss",
-            "welcome": "Welcome to Gauss! Type your message or /help for commands.",
+            "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.",
             "status_glyph": "@",
             "goodbye": "Goodbye! @",
             "response_label": " ∑ Gauss ",