Formal & prose, side by side
A CodeMirror editor holds the Lean source while a textbook-style prose proof of the same argument renders alongside it — the formalism and its meaning in one view.
Turnstile
A Lean proof assistant pairing formal proofs with prose. Develop Lean 4 proofs alongside a textbook-style rendering of the same argument, with a Claude-backed assistant keeping the prose in step with the formalism.
Overview
Turnstile is a desktop app for developing
Lean 4 proofs alongside a
textbook-style prose rendering of the same argument. The left pane is
a CodeMirror editor backed by a live lean --server.
The right pane is human-readble prose proof of the proof along with the Proof Assistant — a Claude-backed collaborator that reads your source, goal state, and diagnostics through tools, and keeps the prose in step with the formalism. The Lean code is the mathematics; the prose relates the meaning.
Features
Live Lean server
The editor is backed by a live lean --server, so
goal state and diagnostics are always current. Turnstile installs
elan, the pinned Lean toolchain, and the
Mathlib
cache on first launch.
Proof Assistant
A Claude-backed collaborator reads your source, goal state, and diagnostics through tools, and keeps the prose in step as the proof evolves.
Releases
Download the latest stable build of Turnstile for your platform. The links always resolve to the most recent published release.
macOS
Universal build for Apple silicon and Intel Macs.
Linux
x86_64 packages — pick the format your distribution uses.