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.

OpenGauss is designed to go from zero to a running proof agent in a single terminal session. This guide walks you through cloning the repo, running the one-line installer, registering a Lean 4 project, and spawning your first /prove workflow — all in under five minutes.
If you want zero local setup, skip this guide entirely and open https://morph.new/opengauss-0-2-2. The hosted environment is pre-configured and ready in under 10 seconds. Claim or save the session early if Morph offers it, then start directly with /project init or /prove.

​
Prerequisites

Before you begin, make sure you have the following available:
  • git — to clone the repository
  • uv — the Python package manager used by the installer (auto-installed by install.sh if missing)
  • ripgrep (rg) — used by lean4-skills for local Lean search
  • Claude or Codex auth — either run claude auth login / codex auth login beforehand, or have your ANTHROPIC_API_KEY or OPENAI_API_KEY ready to paste during gauss setup
  • A Lean 4 project — an existing repo with a lakefile.lean or lakefile.toml, or willingness to create one during setup
After installation, run gauss doctor at any time to check which prerequisites are satisfied, confirm your auth mode, and see whether the current directory resolves to an active Gauss project. It will tell you exactly what is missing before you try to launch a workflow.

​
Steps

1

Clone and install OpenGauss

Clone the repository and run the one-line installer. The script installs uv if needed, creates a repo-local installer environment, installs the local runner, executes the shared opengauss installer flow, and auto-attaches you to a gauss tmux session.
git clone https://github.com/math-inc/OpenGauss.git
cd OpenGauss
./scripts/install.sh
The installer prints progress as it works. When it finishes you will either be attached to the gauss tmux session automatically, or you will see the exact tmux attach -t gauss command to run.
2

Configure your provider (optional)

If you did not pre-authenticate Claude or Codex, run the interactive setup wizard now. It walks you through choosing a backend, entering API keys, and saving them to ~/.gauss/.env.
gauss setup
You can also export your key directly in the shell before launching:
export ANTHROPIC_API_KEY=sk-ant-...
# or
export OPENAI_API_KEY=sk-...
Skip this step entirely if you already ran claude auth login or codex auth login — Gauss will detect those credentials automatically.
3

Launch the Gauss CLI

Start the interactive CLI. If you were auto-attached by the installer you are already inside it; otherwise run:
gauss
You will see the Gauss banner and an interactive prompt. Type /chat to enable inline onboarding and plain-language chat if you want a guided tour before diving in.
4

Register a Lean 4 project

Tell Gauss which Lean project to use for all subsequent workflow agents. If you already have a Lean project on disk:
/project init ~/my-lean-project
If you want to start fresh from a template:
/project create ~/my-lean-project --template-source <template-or-git-url>
Gauss writes a .gauss/project.yaml into the project root and sets it as the active project for the current session. Every workflow agent you spawn from now on runs inside that project root.
5

Spawn a prove agent

Launch a guided proving agent against the active project. You can pass a specific theorem name, a file scope, or flags — or start with no arguments to let the agent discover work to do:
/prove
To target a specific goal:
/prove 1 + 1 = 2
Gauss spawns a managed backend child agent (Claude Code by default) and forwards your arguments to the lean4-skills /lean4:prove workflow command inside the project root. You will see the agent session open in a new tmux pane.
6

Track running agents with /swarm

When you have more than one workflow agent running you can list, reattach, or cancel them from the main Gauss prompt:
/swarm
Example output:
TASK ID          COMMAND     STATUS     STARTED
prove-a1b2c3     /prove      running    3m ago
draft-d4e5f6     /draft      running    1m ago
Reattach to a specific agent:
/swarm attach prove-a1b2c3
Cancel a running agent:
/swarm cancel prove-a1b2c3

​
What to do next

With OpenGauss running and your first agent spawned, a natural next step is to explore the full range of workflow commands — /draft, /review, /formalize, /autoprove — or read the project model documentation to understand how .gauss/project.yaml scopes each agent. The core loop is always the same: 
gauss  →  /project init  →  /prove (or /draft, /review, …)  →  /swarm

Build docs developers (and LLMs) love

Get started for freeTalk to us