Agentic Theory for VS Code

Prove physics theorems in Lean 4 from your editor. Describe a problem in words, or click above any sorry, and the Agentic Theory pipeline formalises it, decomposes it with structured physics, searches Physlib and Mathlib, writes tactics, and checks every step with the Lean 4 kernel.

When the kernel accepts a proof, it is written into your folder. If the run started from a sorry in one of your files, the proof replaces that sorry in place. Nothing the kernel rejected is ever written.

Install

macOS and Linux:

curl -fsSL https://raw.githubusercontent.com/Kernel-Science/agentic-theory-install/main/install.sh | sh

Windows (PowerShell):

irm https://raw.githubusercontent.com/Kernel-Science/agentic-theory-install/main/install.ps1 | iex

Prefer to do it by hand? Download agentic-theory.vsix from the latest release, then in your editor: Extensions → … → Install from VSIX…

Works with VS Code, Cursor, Windsurf, VSCodium, Positron and Trae.

First run

1. Cmd/Ctrl+Shift+P → Agentic Theory: Sign In
2. Confirm the account in your browser
3. Open the Agentic Theory panel and describe a physics problem

What runs where

The proving does not happen on your machine. Your editor sends a statement and receives a proof, so there is no Python to install, no Lean toolchain, and no Mathlib to build — and a proof takes about the same time on an old laptop as on a new one.

The one thing that is local is the part that has to be: writing the accepted proof into the folder you have open.

Requirements

• VS Code 1.90 or newer (or a compatible editor)
• An Agentic Theory account
• A network connection

Notes

This repository exists to distribute the extension and to collect issues. The extension's source is not public.

Found a bug? Open an issue.