Slash commands are special directives typed directly inside a runningDocumentation Index
Fetch the complete documentation index at: https://mintlify.com/math-inc/OpenGauss/llms.txt
Use this file to discover all available pages before exploring further.
gauss interactive session. They are processed by the REPL before the input ever reaches the language model, giving you precise control over sessions, project management, configuration, and Lean workflow orchestration without leaving the terminal.
Forgiving alias rewriting: Common workflow words without the leading slash are automatically rewritten. For example, typing
prove my_lemma is treated the same as /prove my_lemma. The full list of recognized aliases includes prove, draft, review, checkpoint, refactor, golf, autoprove, auto-proof, formalize, autoformalize, and auto-formalize.Start Here
/chat — first-step guide and plain-language chat mode
/chat — first-step guide and plain-language chat mode
Usage:
/chatShows an inline onboarding guide and enables plain-language chat mode for the current session. If you are new to OpenGauss, start here — it walks you through creating a project and picking the right workflow command.Friendly aliases (without slash): chat, start, begin, get started/project — create, convert, inspect, or switch the active Gauss project
/project — create, convert, inspect, or switch the active Gauss project
Usage:
Gauss discovers
/project <subcommand> [args]Manages the active Gauss project that all managed Lean workflow commands target.| Subcommand | Description |
|---|---|
/project init [path] [--name <name>] | Register an existing Lean repo as a Gauss project |
/project convert [path] [--name <name>] | Register an existing Lean blueprint repo |
/project create <path> [--template-source <src>] [--name <name>] | Bootstrap and register a new project from a template |
/project use [path] | Pin the current session to an existing Gauss project |
/project clear | Remove the session override and fall back to ambient discovery |
.gauss/project.yaml by walking upward from the current working directory. Once a project is active all managed backend child agents launch from that project root, ensuring workflow commands always run in the right context.Set a default template once with gauss.project.template_source in ~/.gauss/config.yaml or the GAUSS_BLUEPRINT_TEMPLATE_SOURCE environment variable so you can skip --template-source on every /project create.Workflow
Workflow commands spawn managed backend child sessions. Each one is covered in detail on the Lean 4 Workflow Commands page./prove, /draft, /review, /checkpoint, /refactor, /golf, /autoprove, /formalize, /autoformalize
/prove, /draft, /review, /checkpoint, /refactor, /golf, /autoprove, /formalize, /autoformalize
Each of these commands launches a managed backend agent (Claude Code or Codex) inside the active Gauss project and forwards any arguments to the corresponding
See the Workflow Commands reference for prerequisite details, backend auth modes, and full usage examples.
lean4-skills workflow command.| Command | lean4-skills target | Summary |
|---|---|---|
/prove [scope or flags] | /lean4:prove | Guided interactive Lean proof workflow |
/draft [topic or flags] | /lean4:draft | Draft Lean declaration skeletons |
/review [scope or flags] | /lean4:review | Read-only Lean review (no writes) |
/checkpoint [scope or flags] | /lean4:checkpoint | Save current proof state checkpoint |
/refactor [scope or flags] | /lean4:refactor | Lean refactor workflow |
/golf [scope or flags] | /lean4:golf | Proof golf / minimize proof terms |
/autoprove [scope or flags] | /lean4:autoprove | Autonomous proving, runs without interactive guidance |
/formalize [topic or flags] | /lean4:formalize | Interactive formalization of informal mathematics |
/autoformalize [topic or flags] | /lean4:autoformalize | Autonomous formalization |
/autoformalize-backend — show or change the managed workflow backend
/autoformalize-backend — show or change the managed workflow backend
Usage: You can also change the backend permanently in
/autoformalize-backend [backend]With no argument, shows the currently configured managed workflow backend (claude-code or codex). With an argument, changes the backend for future workflow invocations.~/.gauss/config.yaml under gauss.autoformalize.backend, or set the GAUSS_AUTOFORMALIZE_BACKEND environment variable./swarm — list, attach to, or cancel workflow agents
/swarm — list, attach to, or cancel workflow agents
Usage: Workflow agents continue running in the background even after you detach, so you can start multiple agents in parallel and check on them with
/swarm · /swarm attach <id> · /swarm cancel <id>/swarm lists all currently running managed workflow agents with their task IDs, workflow kind, and status. Use attach to reattach your terminal to a running agent’s session, and cancel to terminate one./swarm.Session
Session management commands
Session management commands
| Command | Description |
|---|---|
/managed-chat | Open the configured managed backend child session (Claude Code or Codex) and return to Gauss when it exits |
/new | Start a new session (fresh session ID and history) |
/reset | Alias for /new |
/clear | Clear the screen and start a new session |
/history | Show the full conversation history for the current session |
/save | Save the current conversation to the session store |
/retry | Resend the last user message to the agent |
/undo | Remove the last user/assistant exchange from the session history |
/title <name> | Set a human-readable title for the current session (e.g. /title My Lean Project) |
/compress | Manually flush memories and compress the conversation context |
/rollback [number] | List available filesystem checkpoints, or restore checkpoint N (requires --checkpoints flag at startup) |
/stop | Kill all running background processes |
Configuration
Configuration commands
Configuration commands
| Command | Description |
|---|---|
/config | Show the current effective configuration (model, provider, tools, skills, and key settings) |
/model [name] | Show the current model, or interactively pick a new one. Optionally pass a model name directly. |
/provider | Show all available providers and indicate which is currently active |
/verbose | Cycle the tool progress display through four modes: off → new → all → verbose |
/reasoning [level|show|hide] | Manage reasoning effort and token display. Pass a level (low, medium, high), show to display reasoning tokens, or hide to suppress them. |
Info
Info commands
Info commands
| Command | Description |
|---|---|
/help | Show the full slash command help with all categories and descriptions |
/usage | Show token usage statistics for the current session (input, output, cache, and total) |
/paste | Check the clipboard for an image and attach it to the next message |
Exit
Exit commands
Exit commands
| Command | Description |
|---|---|
/quit | Exit the CLI and end the current session |
/exit | Alias for /quit |
/q | Short alias for /quit |