# The Lea Ecosystem

> An agent backbone for mathematician-led formalization.

Lea is an open-source Lean 4 agent backbone built so the mathematician stays at the center of formalization — steering the decomposition, intervening mid-proof, and reviewing every claim as it is established.

Lea is a Lean 4 agent backbone. The prover runs in-process behind one application-neutral
API exposing runs, sessions and a stream of typed events. Two applications ship on it:
LeaChat (standalone web client) and LeaOverleaf (Chrome extension + local companion that
formalizes theorems marked in an Overleaf document).

Design commitments:
- The mathematician steers decomposition, intervenes mid-proof, and reviews each claim.
- "Proved" (the file elaborates) is never collapsed into "verified" (SafeVerify kernel
  replay, per-declaration type/body match, axiom whitelist).
- Status is derived from the latest Lean verdict, never stored.
- Extension points are plain files: skills (markdown), sub-agent roles (YAML), tools and
  MCP servers (one registry).

## Pages
- Home: https://vida-nyu.github.io/Lea/
- Install guide: https://vida-nyu.github.io/Lea/install/
- Blog: https://vida-nyu.github.io/Lea/blog/
- Source: https://github.com/VIDA-NYU/Lea
- Community: https://discord.gg/CtEJvUTjm

## Posts
- [2026-08-11] Introducing Lea: formalization that keeps the mathematician in the loop — https://vida-nyu.github.io/Lea/blog/introducing-lea/
  Lea is an open-source Lean 4 agent backbone built on one premise — the mathematician steers the decomposition, intervenes mid-proof, and reviews each claim as it is established.