◆ Brigade

A kitchen-style hierarchy of AI agents brainstorms, plans, formalizes and repairs mathematical proofs — and a Lean 4 proof assistant alone decides what counts as proved. Agents propose; the verifier disposes.

▶ Try the in-browser demo GitHub Get the real version

01Two very different things — don't confuse them

⚠ This website: a simulation

  • One small free model runs inside your browser (WebLLM / WebGPU — no server, no account, no API key) and role-plays every agent: skeptic, brainstormers, strategist, formalizer, prover, critic, chef.
  • No Lean is involved. The "verifier" tickets are theater.
  • One part is real: a numeric skeptic written in JavaScript. Constant arithmetic is computed exactly, and "for every n …" claims are probed on a grid — in your own browser.
Verdicts here: REFUTED (counterexample — certain) · TRUE by computation (constant arithmetic — certain) · SIMULATED proved (plausible, not machine-checked).

✓ The repository: the real prover

  • The full multi-agent pipeline calling Claude with your own API key.
  • A local Lean 4 + Mathlib install actually compiles every proof: zero errors, zero sorrys, whole-file re-check, axiom audit.
  • Four invariants enforced in code and pinned by a 31-test CI suite.
Only here does PROVED mean a machine-checked guarantee. Requires: clone the repo, install Lean locally, add your key.

02Simulated demo — one free model, in your browser

Type any mathematical claim. The model reads it (unlike a canned demo), the JS skeptic checks what it honestly can, and the whole kitchen run is played out below. First use downloads the model once (it's cached afterwards). Needs a WebGPU-capable browser — recent Chrome or Edge on a desktop.

not loaded
try:
SIMULATION — no Lean here chef sous-chef workers simulated verifier idle

03How the real system works

The design answers one question: how do you get honest mathematics out of models that are rewarded for sounding right? By never letting them grade themselves.

PROPOSE — language models (fallible, creative) Chef Skeptic Brainstormers ×3 Sous-chef plan Formalizer Prover Critic triage stuck? chef decomposes into sub-lemmas round failed? retrospective seeds the next round DISPOSE — Lean 4 + Mathlib (ground truth) • statement gate: compiles with := by sorry • proof check: 0 errors, 0 sorries • lint: sorry/admit/axiom banned first • assembled file re-checked whole • axiom audit: nothing beyond the 3 the ONLY thing allowed to say VERIFIED / PROVED attempts errors back
I1 · Lean-only acceptance

A lemma is VERIFIED only after Lean compiles its proof with zero errors and zero sorries.

I2 · Assembly + axiom audit

PROVED requires the assembled file to re-verify as a whole, with no axioms beyond propext, Classical.choice, Quot.sound.

I3 · Pinned statements

Provers submit tactic bodies only. Echoing a different, easier theorem gets stripped — the pinned statement is what Lean sees.

I4 · Lint before Lean

sorry, admit, axiom, native_decide, unsafe: rejected before the verifier is even consulted.

Before any proving, a Skeptic hunts for numeric counterexamples with sympy — against the main claim and every planned lemma. Falsification is cheap; verification is expensive; Brigade spends each where it belongs. In strategic mode, sibling lemmas' first proofs share one Lean compilation and a warm REPL keeps Mathlib loaded — speed without ever weakening acceptance.

04Recording of a genuine run (the real pipeline)

This is the recorded event stream of an actual job through the real orchestrator in its deterministic test harness — the same acceptance path as production. Watch the statement gate catch a broken formalization, a failed proof get repaired, a stuck lemma get decomposed, and the axiom audit gate the final verdict.

RUNNING…

05Run the real thing

Three ingredients: this repo, your own Anthropic API key (Settings panel in the app), and a local Lean 4 + Mathlib install (one script, ~5–10 GB). Only then does "proved" mean what it should.

git clone https://github.com/ysmouhib/brigade
cd brigade
pip install -e server/
bash scripts/setup_lean.sh        # the Lean 4 + Mathlib verifier (skippable to look around)
cd server && python -m uvicorn app.main:app --port 8811
# open http://localhost:8811 — add your key in Settings, pick "Claude + Lean"

Windows: powershell -ExecutionPolicy Bypass -File scripts\windows_demo.ps1, then WINDOWS_GUIDE.md in the repo walks every remaining step, WSL included. Inside the app, the third engine is a scripted replay of the recording above — it's labeled as such and refuses custom input, on purpose.