OpenGauss Lean 4 Workflow Commands: prove, draft, review

Each workflow command spawns a managed backend child session — either Claude Code or Codex — that runs the corresponding lean4-skills command inside the active Gauss project. Gauss stages all of the Lean tooling, MCP/LSP wiring, backend credentials, and runtime assets before handing off to the child session, so the backend agent starts with full context and never needs to be configured manually. The full synopsis of all nine commands is:

Usage: /prove [scope or flags] | /draft [topic or flags] |
       /review [target or flags] | /checkpoint [target or flags] |
       /refactor [target or flags] | /golf [target or flags] |
       /autoprove [scope or flags] | /formalize [topic or flags] |
       /autoformalize [topic or flags]

Command-to-lean4-skills Mapping

Every workflow command is a thin launcher. Any text you pass after the command name is forwarded verbatim as arguments to the corresponding lean4-skills backend command:

Gauss command	Backend command
`/prove`	`/lean4:prove`
`/draft`	`/lean4:draft`
`/review`	`/lean4:review`
`/checkpoint`	`/lean4:checkpoint`
`/refactor`	`/lean4:refactor`
`/golf`	`/lean4:golf`
`/autoprove`	`/lean4:autoprove`
`/formalize`	`/lean4:formalize`
`/autoformalize`	`/lean4:autoformalize`

Prerequisites

Workflow commands require all of the following to be present and authenticated before launch. Gauss performs a preflight check and prints the exact missing item if something is wrong — run gauss doctor for a full report.

claude or codex CLI installed and authenticated (see Backend Auth Modes below).
- Claude Code: npm install -g @anthropic-ai/claude-code
- Codex CLI: install the OpenAI Codex CLI and run codex login
uv or uvx available on $PATH (used to run the managed Lean MCP server).
ripgrep (rg) available on $PATH (used for Lean local search in managed workflows).
git available on $PATH (used to stage managed Lean workflow assets).
An active Gauss project — run /project init, /project convert, or /project use first.

Every workflow command requires an active Gauss project. Gauss walks upward from the current working directory looking for .gauss/project.yaml. If none is found, the command fails with a message directing you to /project init, /project convert, or /project use <path>.

Backend Auth Modes

The managed backend defaults to claude-code. You can switch to codex with /autoformalize-backend codex or by setting gauss.autoformalize.backend: codex in ~/.gauss/config.yaml. Auth is resolved automatically from whichever credentials are available:

Mode	Behaviour
`auto` (default)	Prefer local backend credentials (`claude auth login` / `codex login`). Fall back to a saved `ANTHROPIC_API_KEY` or `OPENAI_API_KEY` in `~/.gauss/.env` if no local credentials are found.
`login`	Ignore staged API-key auth; let the backend use its normal interactive login flow.
`api-key`	Force the managed session onto saved environment/API-key auth only.

Override the auth mode with gauss.autoformalize.auth_mode in ~/.gauss/config.yaml, or with the GAUSS_AUTOFORMALIZE_AUTH_MODE environment variable.

/prove

Usage: /prove [scope or flags]
Backend: /lean4:prove Spawns a guided proving agent in the active Lean project. The agent reads the startup context Gauss generates (project root, Lean root, MCP config), then runs /lean4:prove with any arguments you supply. It works interactively, asking for guidance when it gets stuck and explaining its approach before modifying files.

/prove                           # prove with no scope restriction
/prove MyModule.lean             # target a specific file
/prove Nat.add_comm              # target a specific lemma name
/prove --todo                    # pick up all sorry'd theorems

/draft

Usage: /draft [topic or flags]
Backend: /lean4:draft Drafts Lean declaration skeletons for the specified topic or scope. Useful for scaffolding a new file or adding type signatures before filling in proofs. The agent creates syntactically valid Lean declarations with sorry placeholders that you can then hand to /prove.

/draft                           # draft skeletons based on project context
/draft "group homomorphism"      # draft declarations for a topic
/draft MyModule.lean             # draft additions for an existing file

/review

Usage: /review [scope or flags]
Backend: /lean4:review Spawns a read-only Lean review agent. The agent does not write any files — it reads the project, runs Lean diagnostics, and reports findings (errors, warnings, style issues, proof quality) back to you inside the Gauss session.

/review                          # review the whole project
/review MyModule.lean            # review a single file
/review --errors-only            # only report errors

/checkpoint

Usage: /checkpoint [scope or flags]
Backend: /lean4:checkpoint Saves the current proof state as a named checkpoint inside the active project. Checkpoints are Lean-level markers, distinct from the filesystem checkpoints created by gauss chat --checkpoints. Use this when you have a partially completed proof and want a named recovery point before attempting a risky tactic.

/checkpoint                      # checkpoint the current state
/checkpoint before-ring-lemma    # named checkpoint

/refactor

Usage: /refactor [scope or flags]
Backend: /lean4:refactor Spawns a Lean refactor workflow agent. It reorganises, renames, or restructures declarations while keeping all proofs valid. The agent uses the Lean LSP MCP server to verify that every change compiles before writing it.

/refactor                        # refactor the whole project
/refactor MyModule.lean          # refactor a single file
/refactor --rename OldName NewName  # rename a declaration everywhere

/golf

Usage: /golf [scope or flags]
Backend: /lean4:golf Runs the proof-golf workflow, which attempts to minimize proof terms in the target scope. Golf mode replaces verbose tactic proofs with shorter equivalents (omega, simp, decide, norm_num, etc.) while keeping all goals closed.

/golf                            # golf the whole project
/golf MyModule.lean              # golf a single file
/golf Nat.add_comm               # golf a single theorem

/autoprove

Usage: /autoprove [scope or flags]
Backend: /lean4:autoprove

/prove vs /autoprove

	`/prove`	`/autoprove`
Mode	Guided, interactive	Autonomous, non-interactive
Pauses for guidance	Yes — asks when stuck	No — keeps trying strategies
Best for	Complex proofs needing human insight	Batch-closing `sorry`s, routine lemmas
Backend command	`/lean4:prove`	`/lean4:autoprove`
Suitable for unattended runs	No	Yes

Spawns an autonomous proving agent that attempts to close all outstanding sorry placeholders in the target scope without asking for interactive guidance. It tries multiple tactic strategies in sequence and reports which theorems it could and could not close.

/autoprove                       # attempt all sorry'd theorems in the project
/autoprove MyModule.lean         # target a single file
/autoprove Nat.add_comm          # target a single theorem

/formalize

Usage: /formalize [topic or flags]
Backend: /lean4:formalize Runs an interactive formalization workflow for informal mathematics. You describe a mathematical statement in natural language and the agent produces a Lean 4 statement and proof sketch. Unlike /autoformalize, this is interactive: the agent asks clarifying questions and presents intermediate steps for your review.

/formalize "the sum of the first n natural numbers is n*(n+1)/2"
/formalize "every finite group has an identity element"
/formalize arxiv:2402.03300      # formalize a result from an arXiv paper

The backend agent has access to arXiv paper search, so you can reference papers by ID or keyword and it will look them up before formalizing.

/autoformalize

Usage: /autoformalize [topic or flags]
Backend: /lean4:autoformalize Runs an autonomous formalization workflow. Like /formalize, it takes informal mathematics as input, but it operates without stopping to ask questions — it researches, drafts, and attempts to verify the full Lean proof in one unattended run.

/autoformalize "Cauchy-Schwarz inequality"
/autoformalize "https://arxiv.org/abs/2402.03300"
/autoformalize MyInformalSketch.md

Forgiving aliases: /auto-formalize and /auto_formalize are both rewritten to /autoformalize before dispatch.

Swarm Tracking

When a workflow command starts, it registers a task in the swarm tracker. Use /swarm to see all running agents and their status from any Gauss session:

/swarm                          # list all running workflow agents
/swarm attach <task-id>         # reattach your terminal to a running agent
/swarm cancel <task-id>         # terminate a running agent

Agents continue executing in the background after you detach. You can start multiple parallel agents (each in its own Gauss session with --worktree) and monitor them all from a single parent session with /swarm.

Forgiving Aliases

All nine workflow commands accept common alternative spellings that the REPL silently rewrites before dispatch:

You type	Gauss dispatches
`prove ...`	`/prove ...`
`draft ...`	`/draft ...`
`review ...`	`/review ...`
`checkpoint ...`	`/checkpoint ...`
`refactor ...`	`/refactor ...`
`golf ...`	`/golf ...`
`autoprove ...`	`/autoprove ...`
`auto-proof ...`	`/autoprove ...`
`formalize ...`	`/formalize ...`
`autoformalize ...`	`/autoformalize ...`
`auto-formalize ...`	`/autoformalize ...`
`/auto-proof ...`	`/autoprove ...`
`/auto_proof ...`	`/autoprove ...`
`/auto-formalize ...`	`/autoformalize ...`
`/auto_formalize ...`	`/autoformalize ...`

CLI Reference

Toolsets & Skills

API & Embedding

OpenGauss Lean 4 Workflow Commands: prove, draft, review

Command-to-lean4-skills Mapping

Prerequisites

Backend Auth Modes

/prove

/draft

/review

/checkpoint

/refactor

/golf

/autoprove

/formalize

/autoformalize

Swarm Tracking

Forgiving Aliases

Build docs developers (and LLMs) love

CLI Reference

Toolsets & Skills

API & Embedding

Documentation Index

​Command-to-lean4-skills Mapping

​Prerequisites

​Backend Auth Modes

​/prove

​/draft

​/review

​/checkpoint

​/refactor

​/golf

​/autoprove

​/formalize

​/autoformalize

​Swarm Tracking

​Forgiving Aliases

Build docs developers (and LLMs) love

Command-to-lean4-skills Mapping

Prerequisites

Backend Auth Modes

/prove

/draft

/review

/checkpoint

/refactor

/golf

/autoprove

/formalize

/autoformalize

Swarm Tracking

Forgiving Aliases