OpenGauss is a project-scoped Lean workflow orchestrator from Math, Inc. It givesDocumentation 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.
gauss a multi-agent frontend for the lean4-skills suite of workflows — proving, formalization, drafting, review, and more — while handling Lean tooling setup, MCP/LSP wiring, and backend session state so you can focus on the mathematics. A single interactive CLI drives managed backend child agents (Claude Code or OpenAI Codex) that execute the corresponding lean4-skills commands inside your registered project.
Want to try OpenGauss without installing anything locally? Open the hosted environment at https://morph.new/opengauss-0-2-2. The session launches in under 10 seconds. Claim or save the session early if Morph offers it, then start with
gauss-open-guide, gauss, /chat, or /project init.What OpenGauss does
OpenGauss sits between you and thelean4-skills toolchain. When you type a slash command in the gauss CLI, OpenGauss spawns a managed backend child agent in the active Lean project and forwards your arguments directly into the matching lean4-skills workflow command:
| Gauss command | Forwards to |
|---|---|
/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 ... |
cameronfreer/lean4-skills. OpenGauss exposes it through a Gauss-native CLI and project model, adding project detection, swarm tracking, and session recovery on top.
Key capabilities
Workflow commands — each command spawns a focused agent for a distinct Lean task:/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]— snapshot and checkpoint the current proof state/refactor [scope or flags]— spawn a Lean refactor workflow agent/golf [scope or flags]— minimize and golf existing Lean proofs/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 lists every running workflow agent, lets you reattach to any agent with /swarm attach <task-id>, and cancel one with /swarm cancel <task-id>. This makes it practical to run several agents in parallel across a large proof development.
gauss doctor — a built-in diagnostic command that reports the managed-workflow backend, auth mode, uv / lake availability, and whether the current working directory resolves to an active Gauss project. Run it first when something is not working.
The project model
Gauss treats all Lean work as project-scoped. Before launching managed workflows you register a project once; every subsequent workflow agent then spawns inside that project root. Project state is stored in a.gauss/project.yaml file that Gauss discovers by walking upward from the current working directory.
The core project commands are:
/project init [path]— register an existing Lean repo/project convert [path]— register an existing Lean blueprint repo/project create <path> [--template-source <source>]— bootstrap from a template and register/project use [path]— pin the current session to a registered project/project clear— remove the session override and return to ambient discovery
Architecture overview
The runtime path for a workflow is:lean4-skills layer handles the actual Lean proof interaction. The two are deliberately separated so you can upgrade either independently.
Quickstart
Install OpenGauss and run your first
/prove workflow in five minutes.Installation
Detailed install instructions for macOS, Linux, and Windows WSL2.
Project model
Learn how
.gauss/project.yaml scopes every workflow agent to the right Lean project.Workflow commands
Full reference for
/prove, /formalize, /swarm, and every other slash command.