lean-prover

A native desktop IDE for Lean 4 on macOS, Windows and Linux. Every proof re-checked by Tenet, an independent Lean 4 kernel. An MCP server for AI assistants, with Git and GitHub built in.

Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.

emdash — algebraic goal assistant (proof assistant for ω-categories)

Levee autoformalizes your rulebook (business logic, domain constraints, policy docs) into Lean 4 specs, then enforces them against AI agents at runtime. Formal verification for agentic AI: rules an LLM agent can’t talk its way around.

A Formal Proof of the Irrationality of the Euler-Mascheroni Constant.

Is a Lean based framework to prove solve sudokus and maybe other logic puzzles. The goal is not to solve puzzles but prove the solution.