Prove without leaving the editor.
The same pipeline the console runs, reachable from a .lean file. Describe a problem or click above a sorry, and when the Lean 4 kernel accepts the proof it is written into your folder — no download, no copy-paste.
curl -fsSL https://raw.githubusercontent.com/Kernel-Science/agentic-theory-install/main/install.sh | shThe script fetches the latest .vsix and installs it into whichever supported editor it finds on your machine. Read it first if you would rather not pipe a script into a shell — it is on GitHub.
Install from a VSIX.
If your editor lives behind a proxy, or you would rather see what you are installing, take the file yourself.
- 01Download
agentic-theory.vsixfrom the latest release. - 02In the editor, open Extensions, then the … menu, then Install from VSIX… and pick the file.
- 03Reload the window when prompted.
Sign in once, then bring a theorem.
Open the command palette
⌘⇧P on a Mac, Ctrl+Shift+P elsewhere. Run “Agentic Theory: Sign In”.
Confirm in the browser
The same account you use here. The editor keeps the session in its own secret storage.
Open the panel
Describe the physics, or open a .lean file and click ▶ Prove with Agentic Theory above a sorry.
No Python, no Lean toolchain, no 4 GB Mathlib index and no provider key on your machine. The proving runs on our servers; the extension is a client for it. You need VS Code 1.90 or newer, an Agentic Theory account, and a connection.
Six surfaces, one pipeline.
Chat panel
Describe the physics in words. The panel proposes a Lean 4 statement, then runs the pipeline in front of you — blueprint, search hits, tactics, kernel responses.
Prove above any sorry
A CodeLens sits over every unproved theorem and lemma in a .lean file. There is also a right-click action and a command, if you would rather not click the line.
Formalize a selection
Select prose in a markdown problem sheet and turn it into a candidate theorem, ready to be proved.
Physlib and Mathlib search
A quick pick over both libraries. Picking a hit inserts its name at the cursor — the same index the console searches.
Runs view
Every run the pipeline knows about, including ones started from the console. Pull any accepted proof into the workspace you are in.
Typeset maths
LaTeX in the chat is rendered with KaTeX, so a derivation reads as a derivation and not as backslashes.
In your tree, or nowhere.
Only what the kernel accepted is ever written. The assistant is not allowed to author Lean itself, and anything that looks like it is stripped before it reaches the screen.
- A run started from a sorry in your file replaces that sorry in place.
- Otherwise the proof is written to <LakePackage>/Proofs/<TheoremName>.lean, so lake build picks it up without anything being moved.
- Existing files are never overwritten: a differing proof of the same name is written alongside, and an identical one is not rewritten at all.
Not at your editor?
The console does the same work in a browser tab, and the runs view in the extension will find whatever you started here.