Skip to main content

Documentation 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.

Every workflow command you type in the gauss REPL becomes a managed backend child session — a short-lived, project-scoped agent that runs a lean4-skills workflow command inside your active Lean 4 project and then returns control to you. This page explains the full lifecycle: from the moment you type /prove to when the swarm manager records the running agent and you can reattach to it.

​
The Core Loop

OpenGauss follows a five-step cycle for every workflow invocation:
1

You type a slash command in the gauss REPL

For example: /prove Nat.add_comm or /autoformalize my theorem statement. The REPL accepts both slash-prefixed commands and forgiving bare-word aliases such as prove ... (see the Forgiving Aliases section below).
2

Gauss resolves the active project

Before spawning anything, Gauss discovers the active Gauss project by walking upward from cwd for a .gauss/project.yaml manifest, or by using any session-level override set with /project use. If no project is found, the command fails immediately with a clear error.
3

Gauss stages managed assets and builds a launch plan

The command is resolved against the workflow alias map, the configured backend (claude-code or codex) is identified, auth is staged, the lean4-skills plugin and Lean LSP MCP server are checked out and wired up, and a HandoffRequest is assembled with the full argv, working directory, and environment.
4

A managed backend child session is spawned

Gauss launches a claude or codex CLI subprocess rooted at the active project. The subprocess receives a startup context document that includes the project root, lean root, the resolved backend command (e.g. /lean4:prove Nat.add_comm), and session contract instructions. Gauss hands off to this child session and tracks it in the swarm.
5

The lean4-skills workflow runs inside the child session

The child agent reads its startup context, loads the lean4 plugin, and executes the corresponding lean4-skills workflow command — using the Lean LSP MCP server for real-time type-checking feedback as it works. When it finishes (or you detach), the session is recorded in the swarm.

​
Command Mapping

Each Gauss slash command is a thin alias over the corresponding lean4-skills workflow command. The mapping is fixed:
Gauss commandlean4-skills commandPurpose
/prove/lean4:proveGuided interactive proving agent
/draft/lean4:draftDraft Lean declaration skeletons
/review/lean4:reviewRead-only Lean code review agent
/checkpoint/lean4:checkpointSnapshot and checkpoint workflow
/refactor/lean4:refactorLean code refactor agent
/golf/lean4:golfProof golfing (minimize proof terms)
/autoprove/lean4:autoproveAutonomous proving agent
/formalize/lean4:formalizeInteractive formalization from informal maths
/autoformalize/lean4:autoformalizeAutonomous formalization agent
Any arguments you append to the Gauss command are forwarded verbatim to the backend command. For example: 
/prove --sorry-free Nat.add_comm
# becomes → /lean4:prove --sorry-free Nat.add_comm
The lean4-skills plugin is sourced from the cameronfreer/lean4-skills GitHub repository and is checked out into a managed asset directory under your Gauss home on first use.

​
Forgiving Command Aliases

Gauss accepts bare-word variants without a leading slash, automatically rewriting them into the canonical managed workflow command before dispatch:
What you typeRewritten to
prove .../prove ...
draft .../draft ...
review .../review ...
checkpoint .../checkpoint ...
refactor .../refactor ...
golf .../golf ...
autoprove .../autoprove ...
auto-proof .../autoprove ...
formalize .../formalize ...
autoformalize .../autoformalize ...
auto-formalize .../autoformalize ...
This rewriting happens before any project resolution, so the rest of the launch pipeline sees a canonical command regardless of what you typed.

​
Swarm Manager

Every managed workflow session is registered with the swarm manager so you can track long-running agents, reattach to suspended sessions, or cancel work that is no longer needed. 
/swarm                        # List all running and recently completed agents
/swarm attach <task-id>       # Reattach your terminal to a running agent
/swarm cancel <task-id>       # Send a cancellation signal to a running agent
The task ID shown by /swarm is the same ID embedded in each session’s startup context and log files, making it straightforward to correlate a running child process with the workflow that spawned it.

​
Managed Workflow Prerequisites

Gauss performs a preflight check before every workflow spawn. The following must all be satisfied:

Backend CLI

The claude CLI (for claude-code) or the codex CLI must be installed and authenticated. Gauss checks for the executable on PATH before trying to spawn anything.

uv / uvx

Either uvx or uv must be available so Gauss can run the managed Lean LSP MCP server (lean-lsp-mcp) without a global install.

ripgrep

The rg binary is required for local Lean symbol search inside workflow sessions. Install it via your system package manager.

Active Gauss project

A .gauss/project.yaml manifest must be reachable from the current working directory, or a session-level override must be set with /project use.
If any prerequisite is missing, Gauss surfaces a clear AutoformalizePreflightError that names the missing component and tells you how to fix it.

​
gauss doctor

Running gauss doctor at any time reports the full preflight state without actually launching a session: 
Backend:        claude-code
Auth mode:      auto  (local credentials found)
uv:             ✓  /usr/local/bin/uvx
lake:           ✓  /home/user/.elan/bin/lake
ripgrep:        ✓  /usr/bin/rg
Active project: my-lean-project  (~/proofs/my-lean-project)
It checks the managed-workflow backend, auth mode, uv/lake availability, and whether the current working directory resolves to an active Gauss project.

​
The AIAgent Loop

Inside each managed backend session, the underlying agent follows a synchronous while-loop that drives the conversation until either the workflow completes or the iteration budget is exhausted: 
while api_call_count < max_iterations and iteration_budget.remaining > 0:
    response = client.chat.completions.create(
        model=model,
        messages=messages,
        tools=tool_schemas,
    )
    if response.tool_calls:
        for tool_call in response.tool_calls:
            result = handle_function_call(tool_call.name, tool_call.args, task_id)
            messages.append(tool_result_message(result))
        api_call_count += 1
    else:
        return response.content
Messages follow the OpenAI format (system / user / assistant / tool roles). The agent reads its startup context on the first turn, invokes the lean4 plugin to load workflow guidance, and then uses the lean-lsp MCP server for incremental type-checking feedback on every Lean edit it makes.
The max_iterations limit defaults to 90 turns (set via agent.max_turns in ~/.gauss/config.yaml). Long proofs rarely need adjustment, but for very large formalization tasks you can raise this limit.

Build docs developers (and LLMs) love

Get started for freeTalk to us