The console, with a folder behind it.
Everything the browser does — describe the physics, watch the pipeline run, take the file the Lean 4 kernel accepted — in a native app that can write to your project instead of your downloads folder.
The desktop app runs on macOS and Windows. On a phone or tablet, the console in your browser is the whole product.
The parts a browser tab cannot have.
A folder of its own
A browser tab has no workspace. The app does: accepted proofs and each run's record are written to disk, in your project, rather than downloaded one file at a time.
One account, three places
Sign in once and the app trades a single-use code for its own session. The same account carries the console, the editor extension and this — one history of runs between them.
Nothing else to install
No Python, no Lean toolchain, no 4 GB Mathlib index, no provider key on your machine. The proving runs on our servers; the app is a client for the same gateway the console is.
Open it, sign in, bring a theorem.
The app cannot hold the console’s cookie, so signing in goes through your browser once and comes back with a single-use code. Nothing else is asked of you.
- 01Open the installer and drag the app across, or run the Windows setup.
- 02Choose Sign in. Your browser opens, you confirm the account you already use here, and it hands the app back a code.
- 03Point the app at a folder and describe the physics. Runs you started in the console are already there.
A Mac on Apple Silicon or Intel, or 64-bit Windows. An Agentic Theory account, and a connection — the prover lives on our servers, not in the app.
Prefer your editor?
The same pipeline is a VS Code extension too, with a CodeLens over every sorry in your Lean files.