lean-collab

Run `npx skills add mutable-state-inc/lean-collab --all -g -y` in your terminal to install all skills in this suite globally.

It orchestrates multiple parallel workers to prove Lean 4 theorems by splitting goals into subgoals, verifying tactics, and composing the final verified proof automatically.

You need Lean 4 with Mathlib installed, a Rust toolchain to build the CLI, and an Ensue API key for shared memory coordination between workers.

Workers reason about the math first, validate proof skeletons with a --skeleton flag before decomposing, and search a shared memory of previously successful tactics and failed strategies.

Yes. It runs as a plugin in Claude Code, where the /lean-collab skill spawns parallel prover and decomposer agents that coordinate until the proof is complete.