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.

Formalization is the process of converting informal mathematical statements — theorems, definitions, proofs written in natural language or symbolic notation — into machine-checked Lean 4 code. OpenGauss provides two formalization commands that spawn managed backend agents to do this work inside your active Lean project: /formalize for an interactive, user-guided session and /autoformalize for an autonomous run that proceeds without step-by-step guidance.

​
The two modes

​
/formalize — interactive

/formalize launches a managed backend session where you and the agent work together. The agent opens Claude Code (or Codex) in your project root and begins the lean4:formalize workflow, but it pauses to ask for clarification, suggest alternatives, and incorporate your feedback at each stage. Use this mode when the mathematical content is nuanced or when you want direct control over naming, style, and theorem boundaries. 
/formalize "the Cauchy–Schwarz inequality for inner product spaces"
/formalize --scope Analysis/InnerProduct.lean

​
/autoformalize — autonomous

/autoformalize hands the entire task to the agent. It spawns the same managed backend but runs the lean4:autoformalize workflow end-to-end without stopping for confirmation. Use this mode for well-scoped statements where you trust the agent to make reasonable decisions, or when running in a batch context. 
/autoformalize "the fundamental theorem of calculus, part 1"
/autoformalize --scope FTC.lean
Both commands delegate their proving and formalization behavior to the cameronfreer/lean4-skills project. OpenGauss handles project detection, backend staging, MCP wiring, and swarm tracking — the mathematical workflow logic lives in lean4-skills.

​
How the managed backend works

When you run /formalize or /autoformalize, OpenGauss:
  1. Discovers the active Gauss project by walking upward from your current directory to find .gauss/project.yaml.
  2. Stages the lean4-skills assets (cloned into ~/.gauss/autoformalize/assets/) and the lean-lsp-mcp MCP server.
  3. Prepares a managed backend home directory with credentials, MCP config, and a startup context file.
  4. Spawns a child session — Claude Code or Codex — in the Lean project root, injecting the startup context as the initial prompt.
  5. The child session runs /lean4:formalize or /lean4:autoformalize inside the active Lean project.
  6. The task appears in /swarm where you can monitor it, reattach to it, or cancel it.
The same mechanism powers all other Gauss workflow commands: /prove forwards to /lean4:prove, /draft to /lean4:draft, /review to /lean4:review, and so on.

​
Typical formalization workflow

1

Select or create a Lean project

Register your project if you haven’t already:
/project init ~/my-lean-project
# or scaffold a new one:
/project create ~/new-project --template-source <url>
2

Start Gauss

From your project directory:
cd ~/my-lean-project
gauss
3

Run the formalization command

Pass the mathematical statement directly as a string argument:
/formalize "Every Cauchy sequence in a complete metric space converges"
Or target a specific file in your project:
/formalize --scope MetricSpaces/Completeness.lean
4

The agent opens Claude Code in your project root

Gauss stages the lean4-skills plugin and MCP server, then launches Claude Code with the startup context injected. Claude Code immediately runs /lean4:formalize (or /lean4:autoformalize) as its first action.For the interactive /formalize mode you’ll see the agent’s progress in the spawned session and can provide guidance. For /autoformalize the agent runs fully autonomously.
5

Monitor and reattach via /swarm

The running task is listed in the swarm:
/swarm                        # list running workflow agents
/swarm attach <task-id>       # reattach to a running agent
/swarm cancel <task-id>       # cancel a running agent
6

Save progress with /checkpoint

At any point you can snapshot the working state of the Lean project:
/checkpoint
This is forwarded to /lean4:checkpoint in the backend session.

​
The prove / autoprove distinction

The same interactive vs. autonomous pattern applies to the proving commands:
CommandModeBackend
/prove [scope or flags]Interactive — you guide the agent/lean4:prove
/autoprove [scope or flags]Autonomous — agent works independently/lean4:autoprove
/formalize [topic or flags]Interactive formalization/lean4:formalize
/autoformalize [topic or flags]Autonomous formalization/lean4:autoformalize
In addition, /draft, /review, /refactor, /golf, and /checkpoint are available for the full Lean workflow lifecycle. All commands follow the same pattern: Gauss spawns a managed backend child session and forwards the argument tail to the corresponding lean4-skills workflow command.

​
Backend requirements

OpenGauss supports two managed workflow backends:
The default backend. Requires the Claude Code CLI installed and authenticated:
npm install -g @anthropic-ai/claude-code
claude auth login
Or save an ANTHROPIC_API_KEY in ~/.gauss/.env. When both local Claude credentials and a saved API key are present, Gauss prefers the local credentials.You can control auth behavior with gauss.autoformalize.auth_mode in ~/.gauss/config.yaml:
gauss:
  autoformalize:
    backend: claude-code
    auth_mode: auto     # auto | login | api-key
Other prerequisites checked before launch:
  • git — for staging lean4-skills assets
  • uv or uvx — for running the lean-lsp-mcp MCP server
  • rg (ripgrep) — for Lean local search in the workflow
  • An active Gauss project (gauss doctor reports all of these)

​
Passing flags through

Any text after the command name is forwarded verbatim as the argument tail to the backend lean4-skills command. This lets you pass lean4-skills-specific flags without any special Gauss syntax: 
/autoformalize --scope MyTheorem.lean
/formalize --draft-only "Fermat's Last Theorem"
/autoprove --timeout 300 NatPrimes

​
Example session

Here is what a typical interactive /formalize session looks like: 
gauss> /formalize "every finite group has an order dividing the product of its elements"

[Gauss] Staging lean4-skills assets... done
[Gauss] Spawning claude-code backend in ~/my-lean-project
[Gauss] Task ID: formalize-20250601-142031
[Gauss] Attaching to managed session...

claude> Reading startup context...
claude> Running /lean4:formalize "every finite group has an order dividing..."
claude> Searching for relevant Mathlib declarations...
claude> Found: Group.card_dvd_of_orderOf_dvd, Finset.prod_mem
claude> Drafting Lean 4 statement...

  theorem group_order_dvd (G : Type*) [Group G] [Fintype G] :
      ∀ g : G, orderOf g ∣ Fintype.card G := orderOf_dvd_card

claude> This is Lagrange's theorem in a specific form.
        Shall I also formalize the general statement?

gauss> Yes, please include the general Lagrange statement.
Use /checkpoint inside a long formalization session to snapshot the current Lean project state. If the agent takes a wrong turn, you can /rollback to the last checkpoint.

​
Forgiving command aliases

Inside the interactive Gauss CLI, you can omit the leading slash for workflow commands and Gauss will rewrite them automatically: 
formalize "Zorn's lemma"       →   /formalize "Zorn's lemma"
autoformalize FTC.lean         →   /autoformalize FTC.lean
auto-formalize                 →   /autoformalize
prove NatPrimes                →   /prove NatPrimes

Build docs developers (and LLMs) love

Get started for freeTalk to us