Ergo

Ergo is an AI-powered IDE for Lean 4 theorem proving that deeply integrates Claude with the Lean 4 language server to give mathematicians a productive, modern environment for writing formal proofs.

Editor — Lean 4 syntax highlighting, Unicode input (type \forall → ∀), inline diagnostics, auto-save, and undo/redo.

Lean Integration — Live proof goals and tactic state in the Infoview as you move your cursor, diagnostics from the Lean server, hover info, file progress indicators, and one-click toolchain install.

AI Agent — Claude-powered assistant with full tool use that reads files, edits code, creates files, lists directories, gets diagnostics, and reads proof state. Edits are auto-applied with an undo button to revert any change.

Build System — Build Project, Get Mathlib Cache, Update Dependencies, and Clean Build with a terminal-like output panel featuring auto-scroll, error highlighting, and cancel support.

IDE — File explorer with collapsible tree view, tabbed editor, resizable panels, project creation with lake init, and a Catppuccin Mocha dark theme throughout.