Open Gauss

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.

Very short version:

• Morph: open https://morph.new/opengauss-0-2-2, claim or save the session early if Morph offers it, then use gauss-open-guide, gauss, /chat, or /project init.
• Local: run ./scripts/install.sh, then gauss-open-guide or gauss, then start with /chat, /project init, or /project create.

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:

• /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 ...

Install

If you want the fastest pinned release path, https://morph.new/opengauss-0-2-2 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 before picking a workflow.

macOS and Linux

git clone https://github.com/math-inc/OpenGauss.git
cd OpenGauss
./scripts/install.sh

This is the canonical local install path. It bootstraps the local installer runtime, runs the shared opengauss installer flow on your machine, and then auto-attaches to the final gauss tmux session when possible.

It will:

1. Install uv if needed
2. Create a repo-local installer environment
3. Install or upgrade the local runner
4. Run the shared opengauss installer flow on your machine
5. Auto-attach you to the local gauss tmux session when possible, or print the exact tmux attach -t gauss command if not

You can pass normal template-runner flags through to the alternate script, for example:

./scripts/install.sh --plain
./scripts/install.sh --secret OPENAI_API_KEY=...
./scripts/install.sh --secret ANTHROPIC_API_KEY=...

Windows (via WSL2)

Open Gauss on Windows runs through WSL2 using the same shared installer flow.

From PowerShell:

.\scripts\install.ps1 -WithWorkspace

This bootstrap:

1. Starts your WSL distro
2. Clones or updates OpenGauss inside your WSL home directory
3. Runs ./scripts/install.sh there, which executes the shared opengauss installer flow inside WSL

If no WSL distro is initialized yet, the bootstrap will install Ubuntu for you with wsl --install -d Ubuntu. If that process drops you into the new Linux shell, type exit to return to PowerShell and rerun .\scripts\install.ps1 -WithWorkspace. Windows may also ask to enable WSL features or restart before you rerun the installer.

If WSL is not installed yet:

wsl --install -d Ubuntu

You can also install manually inside WSL:

wsl
git clone https://github.com/math-inc/OpenGauss.git ~/OpenGauss
cd ~/OpenGauss
./scripts/install.sh

Use a Linux path such as ~/OpenGauss, not /mnt/c/..., for the best performance and terminal behavior.

Configuration

🖥️ Using Local Models (vLLM)

If you prefer to run models locally (e.g., using a local GPU) to save on API costs:

1. Start your vLLM server (OpenAI-compatible):

   python -m vllm.entrypoints.openai.api_server --model 
   

2. Point Gauss at that server with gauss setup, or update OPENAI_BASE_URL in ~/.gauss/.env.

Updating

cd OpenGauss
git pull
gauss update

Quick start

If you want the plain-language version first, read the Start Here guide.

gauss                         # Launch top-level Gauss
/chat                         # Turn on inline onboarding and plain-language chat
/project create ~/my-project --template-source 
/prove 1+1=2                  # Spawn a proving agent after selecting a project
/swarm                        # See running agents

If you already have a Lean project:

cd ~/my-lean-project
gauss
/chat                         # Optional: inline onboarding in the current Gauss session
/project init                 # Register it as a Gauss project
/prove                        # Start proving

The core loop

1. Start the CLI with gauss
2. Create or select the active project with /project
3. Launch /prove, /draft, /review, /checkpoint, /refactor, /golf, /autoprove, /formalize, or /autoformalize
4. Gauss spawns a managed backend child session that runs the corresponding lean4-skills workflow command in the active project
5. Use /swarm to track or reattach to running workflow agents

Project model

Gauss treats Lean work as project-scoped by default. Before launching managed workflows, select the active project once and then let Gauss keep spawning backend child agents inside that project root.

• /project init [path] [--name ] registers an existing Lean repo as a Gauss project
• /project convert [path] [--name ] registers an existing Lean blueprint repo
• /project create [--template-source ] [--name ] bootstraps a project from a template and registers it
• /project use [path] pins the current session to an existing Gauss project
• /project clear removes the session override and falls back to ambient project discovery

If you use /project create often, set a default template once with gauss.project.template_source in ~/.gauss/config.yaml or the GAUSS_BLUEPRINT_TEMPLATE_SOURCE environment variable.

Gauss discovers .gauss/project.yaml upward from the current working directory, but managed workflow child agents launch from the active project root so the forwarded Lean workflow command always runs in the right project context.

Workflow commands

• /prove [scope or flags] — spawn a guided proving agent
• /draft [topic or flags] — draft Lean declaration skeletons
• /review [scope or flags] — spawn a read-only Lean review agent
• /checkpoint [scope or flags] — spawn the Lean checkpoint workflow
• /refactor [scope or flags] — spawn a Lean refactor workflow agent
• /golf [scope or flags] — spawn a Lean proof golfing workflow agent
• /autoprove [scope or flags] — spawn an autonomous proving agent
• /formalize [topic or flags] — spawn an interactive formalization agent
• /autoformalize [topic or flags] — spawn an autonomous formalization agent
• /swarm — list running workflow agents
• /swarm attach — reattach to a running agent
• /swarm cancel — cancel a running agent

Inside the interactive CLI, Gauss also rewrites common missing-slash forms like prove ..., review ..., checkpoint ..., and auto-proof ... into the corresponding managed workflow commands.

Managed workflow prerequisites

• gauss.autoformalize.backend defaults to claude-code
• Built-in backends: claude-code, codex
• claude or codex installed and authenticated for the backend you select
• Claude auth can come from either:
  • the normal claude auth login flow / Claude credential files
  • a saved ANTHROPIC_API_KEY in ~/.gauss/.env
• If both are present, Gauss defaults to Claude's own local auth and only falls back to ANTHROPIC_API_KEY when no Claude credentials are available
• Override with gauss.autoformalize.auth_mode in ~/.gauss/config.yaml:
  • auto (default): prefer local backend auth, then fall back to saved env/API-key auth
  • login: ignore staged API-key auth and let the backend use the normal interactive login flow
  • api-key: force the managed session onto saved env/API-key auth
• uv or uvx available
• ripgrep (rg) available for Lean local search
• An active Gauss project selected via .gauss/project.yaml

Gauss checks these before launch and tells you exactly what is missing. gauss doctor also reports the managed-workflow backend, auth mode, uv / lake availability, and whether the current working directory resolves to an active Gauss project.

This repository was forked from nousresearch/hermes-agent.