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 every piece of Lean work as project-scoped. Before you can spawn a proving, drafting, or formalization agent, you register a Lean 4 repository as a Gauss project. That registration writes a small manifest file called .gauss/project.yaml into the repo root, and from that point forward every managed workflow child agent automatically launches inside that project. This section explains the project model in detail — what the manifest contains, how Gauss discovers it, and which commands let you create or switch projects.

​
What Is a Gauss Project?

A Gauss project is a Lean 4 repository that contains a .gauss/project.yaml manifest. The manifest records the project name, its kind (always lean4), the relative path to the Lean root, the creation timestamp, the source mode used to create it, and a set of derived runtime paths. Gauss validates the manifest on every load: it checks the schema version, confirms that a non-empty name is present, verifies that kind is lean4, and asserts that the declared lean_root directory actually contains a lakefile.lean or lakefile.toml. A minimal .gauss/project.yaml looks like this: 
schema_version: 1
name: my-lean-project
kind: lean4
lean_root: .
created_at: "2025-01-15T10:30:00+00:00"
source:
  mode: init
  template_source: ""
blueprint:
  markers: []
paths:
  runtime: .gauss/runtime
  cache: .gauss/cache
  workflows: .gauss/workflows

​
Project Discovery

When you run a workflow command, Gauss needs to know which project is active. It performs upward discovery: starting from the current working directory, it walks toward the filesystem root looking for a .gauss/ subdirectory. The first directory that contains .gauss/project.yaml becomes the active project. 
/home/user/proofs/MyTheorem/       ← Gauss stops here (contains .gauss/)
  .gauss/
    project.yaml
  MyProject/
    lakefile.lean
    MyTheorem.lean          ← you are here (cwd)
If no manifest is found anywhere in the ancestor chain, Gauss raises a ProjectNotFoundError and tells you exactly which command to run next.
You can bypass discovery entirely by running gauss-open-guide to get onboarding guidance, or by running gauss and then /project use <path> to pin your session to a specific project root.
Managed workflow child agents always launch from the active project root, not from your current working directory, so the forwarded lean4-skills workflow command always executes in the right Lean context.

​
The GaussProject Dataclass

When a project is loaded from disk, Gauss populates a frozen GaussProject dataclass with the following fields:
​
root
Path
Absolute path to the project root directory (the directory that contains .gauss/).
​
gauss_dir
Path
Absolute path to the .gauss/ directory inside the project root.
​
manifest_path
Path
Absolute path to the .gauss/project.yaml manifest file.
​
name
str
Human-readable project name. Defaults to the directory name if not specified during init.
​
kind
str
Project kind. Always lean4 in the current release.
​
schema_version
int
Integer schema version of the manifest. Currently always 1.
​
lean_root
Path
Absolute path to the Lean 4 project root — the directory that contains lakefile.lean or lakefile.toml. Must be at or below root.
​
runtime_dir
Path
.gauss/runtime — scratch directory used by managed workflow sessions at runtime.
​
cache_dir
Path
.gauss/cache — persistent cache for staged assets between runs.
​
workflows_dir
Path
.gauss/workflows — workflow state and session artifacts.
​
created_at
str
ISO 8601 UTC timestamp recording when the manifest was first written.
​
source_mode
str
How the project was created: init, convert, or create.
​
template_source
str
The Git URL or local path used to scaffold the project, if it was created with /project create. Empty for init and convert projects.
​
blueprint_markers
tuple[str, ...]
Files detected at registration time that indicate this is a Lean blueprint project. See the Blueprint Projects section below.
​
manifest
dict[str, Any]
The raw parsed manifest payload as a dictionary, for access to any fields not covered by the typed attributes above.

​
Project Commands

All project management happens through /project subcommands inside the gauss REPL.
1

Register an existing Lean repo

/project init [path] [--name <name>]
Writes .gauss/project.yaml into an existing Lean 4 repository. Run this inside your repo root (omit path) or pass the path explicitly. The --name flag overrides the default name (the directory’s basename).
2

Register a blueprint repo

/project convert [path] [--name <name>]
Like init, but signals that this is a Lean blueprint repository. Gauss scans for blueprint markers and records them in the manifest.
3

Scaffold a new project from a template

/project create <path> [--template-source <source>] [--name <name>]
Clones a blueprint template into <path> (the directory must not already exist), then registers it as a Gauss project. The --template-source flag accepts a Git URL or a local directory path.
4

Pin your session to a project

/project use [path]
Sets a session-level override so that all subsequent workflow commands target this project, regardless of your current working directory.
5

Clear the session override

/project clear
Removes the session override and returns Gauss to ambient upward discovery from cwd.

​
Blueprint Projects

A blueprint project is a Lean repository structured around a formal mathematics blueprint — typically using the leanblueprint toolchain, GitHub Actions for continuous checking, and a templates/ directory for task scaffolding. Gauss detects blueprint projects by checking for the presence of any of the following markers at the project root:
MarkerMeaning
lean-toolchainPinned Lean toolchain version file
lakefile.leanLean 4 Lake build manifest
lakefile.tomlLean 4 Lake TOML build manifest
templates/blueprint.ymlBlueprint task template
.github/workflows/gauss.ymlGauss-managed CI workflow
If at least one marker is present, GaussProject.is_blueprint returns True and the project label shown in the CLI includes a · blueprint tag.

​
Default Template Source

If you run /project create frequently, you can avoid typing --template-source every time by configuring a default. Gauss resolves the template source in this priority order:
  1. The GAUSS_BLUEPRINT_TEMPLATE_SOURCE environment variable
  2. The gauss.project.template_source key in ~/.gauss/config.yaml
# ~/.gauss/config.yaml
gauss:
  project:
    template_source: "https://github.com/your-org/lean4-blueprint-template.git"
The --template-source flag passed directly to /project create always takes precedence over both. If none of these are set and you run /project create without --template-source, Gauss raises a ProjectTemplateUnavailableError and explains what to configure.

Build docs developers (and LLMs) love

Get started for freeTalk to us