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 a project-scoped orchestrator that wraps the lean4-skills proving and formalization workflows behind a single interactive CLI. Launch gauss, select a Lean project, and spawn managed backend agents for proving, drafting, reviewing, refactoring, and formalizing — all tracked through a swarm manager so you never lose a running session.

Quickstart

Go from zero to a running /prove session in under five minutes.

Installation

Install on macOS, Linux, or Windows (via WSL2) with the one-line installer.

Workflow Commands

/prove, /draft, /review, /autoprove, /formalize, and more.

Project Model

Understand how OpenGauss registers and discovers Lean 4 projects.

​
What OpenGauss does

OpenGauss sits between you and the lean4-skills toolchain. Every slash command you run inside the gauss REPL spawns a managed backend child session — a Claude Code or Codex agent that runs the corresponding lean4-skills workflow command inside your active Lean project. OpenGauss handles project detection, backend setup, workflow spawning, swarm tracking, and recovery, so you stay focused on the math.
1

Install OpenGauss

Clone the repo and run the one-line installer. It sets up uv, installs dependencies, and drops you into a gauss tmux session.
git clone https://github.com/math-inc/OpenGauss.git
cd OpenGauss
./scripts/install.sh
2

Select or create a Lean project

Register an existing Lean repo or scaffold a new one from a template.
/project init ~/my-lean-project
3

Spawn a workflow agent

Launch a managed proving agent. OpenGauss starts Claude Code in the project root and forwards your arguments into the lean4:prove workflow.
/prove
4

Track running agents

Check on all active workflow sessions and reattach to any of them.
/swarm
/swarm attach <task-id>

​
Core workflow commands

/prove

Guided Lean proof agent

/draft

Draft declaration skeletons

/review

Read-only Lean review agent

/autoprove

Autonomous proving agent

/formalize

Interactive formalization

/autoformalize

Autonomous formalization

​
Explore the docs

Configuration

Tune models, providers, terminal backends, memory, and display settings.

Guides

Step-by-step guides for formalization, local models, messaging, and MCP.

CLI Reference

Every gauss subcommand and flag documented with defaults and examples.

API & Embedding

Use AIAgent programmatically or run batch jobs with the batch runner.

Build docs developers (and LLMs) love

Get started for freeTalk to us