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 delegates the actual Lean proving and formalization work to a managed backend child session — a separately spawned CLI process that runs the lean4-skills workflows on your behalf. Two backends are supported: claude-code (the default) and codex. Both backends receive the same startup context, project wiring, and Lean LSP MCP configuration; the difference lies in which CLI binary is invoked and how authentication is resolved. This page covers configuration, auth modes, and the Lean LSP MCP integration that both backends share.

​
Supported Backends

The claude-code backend spawns a managed claude CLI child session running claude-opus-4-6 by default.Install and authenticate:
# Install the Claude CLI (see https://claude.ai/code for the current installer)
# Then authenticate interactively:
claude auth login
Or use an API key directly:
# Add to ~/.gauss/.env
ANTHROPIC_API_KEY=sk-ant-...
The default model for managed Claude Code sessions is claude-opus-4-6. This is set by the CLAUDE_MODEL constant in the Gauss source and is not currently user-configurable per-session.
Auth resolution — auto mode (default):Gauss first checks for local Claude credentials (OAuth token in ~/.claude/.credentials.json, a primaryApiKey in ~/.claude.json, or the macOS Keychain). If local credentials are found, they take priority. When no local credentials are present, Gauss falls back to checking the CLAUDE_CODE_OAUTH_TOKEN, ANTHROPIC_TOKEN, and ANTHROPIC_API_KEY environment variables (in that order). You can override this with the auth_mode config key (see Auth Modes below).Configure in ~/.gauss/config.yaml:
gauss:
  autoformalize:
    backend: claude-code
    auth_mode: auto   # auto | login | api-key

​
Changing the Backend

You can switch backends at any time without restarting gauss. Inside the gauss REPL: 
/autoformalize-backend claude-code
/autoformalize-backend codex
In ~/.gauss/config.yaml (persists across sessions): 
gauss:
  autoformalize:
    backend: claude-code   # or: codex
Via environment variable (overrides config for the current shell): 
export GAUSS_AUTOFORMALIZE_BACKEND=codex
gauss
Gauss normalizes backend names, so claude, claude-code, codex, codex-cli, and openai-codex are all accepted and resolved to the canonical identifier.

​
Auth Modes (Claude Code)

The gauss.autoformalize.auth_mode config key controls how Gauss resolves Claude credentials for each managed session. You can also set GAUSS_AUTOFORMALIZE_AUTH_MODE as an environment variable to override the config value for the current shell.

auto

Default. Prefer local Claude CLI credentials (OAuth login or macOS Keychain). Fall back to environment variables (CLAUDE_CODE_OAUTH_TOKEN, ANTHROPIC_TOKEN, ANTHROPIC_API_KEY) only when no local credentials are found.

login

Always use the interactive Claude login flow. Environment-variable API keys are ignored even if they are present.

api-key

Force the managed session to use environment-variable auth (CLAUDE_CODE_OAUTH_TOKEN, ANTHROPIC_TOKEN, or ANTHROPIC_API_KEY). Interactive login credentials are bypassed.
# ~/.gauss/config.yaml
gauss:
  autoformalize:
    auth_mode: auto   # auto | login | api-key
When auth_mode is auto, Gauss checks for credentials in this order:
  1. Local OAuth credentials (~/.claude/.credentials.json or macOS Keychain entry Claude Code-credentials)
  2. Local API key stored in ~/.claude.json (primaryApiKey)
  3. CLAUDE_CODE_OAUTH_TOKEN environment variable or ~/.gauss/.env
  4. ANTHROPIC_TOKEN environment variable or ~/.gauss/.env
  5. ANTHROPIC_API_KEY environment variable or ~/.gauss/.env

​
Lean LSP MCP Integration

Both backends connect to a Lean LSP MCP server (lean-lsp-mcp) that provides real-time type-checking, goal state inspection, and symbol navigation to the child agent. Gauss starts this server automatically as part of the managed session setup — you do not need to configure it manually. The MCP server is launched via uvx (or uv x if uvx is not on PATH): 
uvx --from lean-lsp-mcp lean-lsp-mcp
The LEAN_PROJECT_PATH environment variable is passed to the server so it knows which Lean project to attach to. Gauss writes the full MCP configuration (server command, args, and env) into a per-session config file before the child CLI is launched. To pin a specific version or use a local build, set the GAUSS_AUTOFORMALIZE_LEAN_LSP_MCP_SPEC environment variable: 
export GAUSS_AUTOFORMALIZE_LEAN_LSP_MCP_SPEC="lean-lsp-mcp==0.3.1"

​
lean4-skills Plugin

The actual workflow logic — proving strategies, draft templates, review checklists, and so on — lives in the lean4-skills plugin, maintained at cameronfreer/lean4-skills. Gauss checks out this repository into a managed asset cache on first use and keeps it updated. The plugin exposes a lean4 namespace that provides the /lean4:prove, /lean4:draft, /lean4:autoformalize, and other workflow commands that the managed child agent executes. For the claude-code backend, the plugin is installed as a Claude marketplace plugin inside the managed Claude home directory. For the codex backend, the plugin source directory is passed as a skill reference in the session instructions.
If you need to pin the lean4-skills checkout to a specific Git ref (branch, tag, or commit SHA), set GAUSS_AUTOFORMALIZE_LEAN4_SKILLS_REF in your environment before running a workflow command. Gauss will force a fresh checkout to that ref.

Build docs developers (and LLMs) love

Get started for freeTalk to us