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 treats all Lean work as project-scoped. Before launching any managed workflow — /prove, /formalize, /autoprove, and so on — you register a Gauss project once and then let Gauss keep spawning backend child agents inside that project root. The project model is stored in a small .gauss/project.yaml manifest that lives alongside your Lean source tree.

​
How Gauss discovers the active project

When you launch gauss, it walks upward from your current working directory looking for a .gauss/ folder. The first directory it finds that contains a valid project.yaml becomes the active project for that session. You can override this automatic discovery by pinning a project with /project use or by clearing the override with /project clear. 
~/my-lean-project/           ← project root
  .gauss/
    project.yaml             ← Gauss manifest (auto-discovered)
    runtime/
    cache/
    workflows/
  lakefile.lean              ← Lean project root marker
  MyProject/
    Basic.lean
The Lean project root is found by a separate upward walk that looks for lakefile.lean or lakefile.toml. These two roots can differ when your Gauss manifest sits above the Lean root (for example in a monorepo), but the Lean root must always be inside the Gauss project root.

​
Three ways to start a project

​
1. Register an existing Lean repo

If you already have a working Lean 4 repository, navigate into it and register it as a Gauss project: 
/project init ~/my-lean-project
# or, if you're already inside the repo:
/project init
Gauss will detect lakefile.lean or lakefile.toml automatically and write .gauss/project.yaml.

​
2. Scaffold from a template

To start a brand-new project from a blueprint template, use /project create. Gauss clones the template source, then registers the result as a Gauss project in one step: 
/project create ~/new-project --template-source https://github.com/example/lean-blueprint-template.git
If you run /project create often, save a default template source so you don’t have to pass --template-source every time — see Setting a default template source below.

​
3. Register an existing blueprint repo

If you have a Lean blueprint repository (one that already contains blueprint infrastructure files), use /project convert instead of /project init. The convert path records the detected blueprint markers in the manifest. 
/project convert ~/blueprint-repo

​
Switching between projects

Once projects are registered you can switch the active project at any time from inside a running gauss session.
CommandEffect
/project use <path>Pin the current session to the project at <path>
/project clearRemove the session override and fall back to auto-discovery
/project use accepts either the project root directory or the path to its .gauss/ directory or manifest file.

​
Setting a default template source

When you use /project create regularly, avoid typing --template-source every time by setting a default once:
Edit ~/.gauss/config.yaml and add:
gauss:
  project:
    template_source: "https://github.com/example/lean-blueprint-template.git"

​
Blueprint projects

A blueprint project is a Lean project that ships extra infrastructure for rendering a mathematical blueprint — typically an HTML proof-outline website alongside the formal Lean development. OpenGauss detects blueprint projects by checking for known marker files under the project root:
Marker fileMeaning
lean-toolchainLean toolchain pin
lakefile.lean / lakefile.tomlLean project root
templates/blueprint.ymlBlueprint template config
.github/workflows/gauss.ymlGauss CI workflow
When /project convert finds any of these markers, it records them in the blueprint.markers list inside project.yaml. You can check project.is_blueprint (or inspect the manifest) to confirm the project was recognized as a blueprint.

​
The project manifest

Every registered Gauss project has a .gauss/project.yaml file. Here is an annotated example: 
schema_version: 1
name: my-lean-project
kind: lean4
lean_root: .                    # path to Lean root, relative to project root
created_at: "2025-06-01T12:00:00+00:00"

source:
  mode: init                    # init | create | convert
  template_source: ""           # template URL used by /project create

blueprint:
  markers:                      # blueprint marker files detected at registration
    - lean-toolchain
    - lakefile.lean

paths:
  runtime: .gauss/runtime
  cache: .gauss/cache
  workflows: .gauss/workflows
Field reference:
FieldDescription
schema_versionAlways 1 for the current manifest format
nameHuman-readable project label (defaults to directory name)
kindAlways lean4 — the only supported project kind
lean_rootPath to the Lean project root, relative to the Gauss project root
created_atISO-8601 UTC timestamp of registration
source.modeHow the project was registered: init, create, or convert
source.template_sourceTemplate URL when mode is create
blueprint.markersBlueprint marker files found at registration time

​
Start from scratch: full walkthrough

Follow these steps to go from nothing to a running Gauss workflow on a new project.
1

Install OpenGauss

If you haven’t already, run the installer:
git clone https://github.com/math-inc/OpenGauss.git
cd OpenGauss
./scripts/install.sh
2

(Optional) Set a default template source

Add gauss.project.template_source to ~/.gauss/config.yaml or export GAUSS_BLUEPRINT_TEMPLATE_SOURCE so you don’t need to repeat it.
3

Create the project

Launch gauss and scaffold a new project from your template:
gauss
/project create ~/my-lean-project --template-source <url>
Gauss clones the template, detects lakefile.lean or lakefile.toml, and writes .gauss/project.yaml.
4

Confirm the active project

Gauss will confirm the newly created project is now active. You can verify by running /project with no arguments to see the current project summary.
5

Start a workflow

With a project active, any workflow command will launch in the right root:
/prove
/formalize "There are infinitely many primes"
/autoprove --scope Primes.lean

​
Full /project command synopsis

/project init [path] [--name <name>]
    Register an existing Lean repo as a Gauss project.

/project convert [path] [--name <name>]
    Register an existing Lean blueprint repo as a Gauss project.

/project create <path> [--template-source <url>] [--name <name>]
    Clone a blueprint template and register the result as a Gauss project.

/project use [path]
    Pin the current session to an existing Gauss project.

/project clear
    Remove the session override and fall back to ambient project discovery.
gauss doctor reports whether the current working directory resolves to an active Gauss project, alongside backend, auth, and toolchain health checks.

Build docs developers (and LLMs) love

Get started for freeTalk to us