Isabelle Automation

Python tooling for automated theorem proving in Isabelle

Isabelle is an interactive prover: a person writes a theory, and the prover checks it and shows the proof state as they go. Automating that loop — reading proof states, trying proof methods, replacing a sledgehammer call with the proof it found — needs programmatic access to what the editor sees. These Python packages provide it, both from a running Isabelle and statically from the theory files alone. All four are MIT-licensed and work in progress.

Packages

• python-lsp-client (lsp_client) — an asynchronous client for the Language Server Protocol, with the protocol’s messages as pydantic models. It knows nothing about Isabelle and aims to be correct with respect to the official specification; until version 1 it is incomplete.
• python-isabelle-lsp-client (isabelle_lsp_client) — starts isabelle vscode_server and talks to it over LSP. Callbacks subscribe to Isabelle’s PIDE notifications, and moving the caret elaborates the theory up to that point, so the proof state after any single tactic can be read back — finer-grained than a client that talks to the Isabelle server process. The auto_sledge example replaces every sledgehammer call in a theory with the proof Isabelle finds. It supports Isabelle 2023 and 2024, and needs the isabelle-emacs fork, whose plain-text output mode it depends on.
• python-isabelle-parser (isabelle_parser) — an Earley grammar for the outer syntax of Isabelle/Isar on top of Lark. It turns a .thy file — theory header, document markup, specifications, Isar proofs and ML commands — into a parse tree to walk, without an Isabelle installation.
• isabelle-check (isabelle_check) — incremental checking for agents that edit theories. Instead of re-running isabelle build after every edit, it keeps a session warm in a resident isabelle server and re-checks only the theories whose files changed and the theories that import them, reporting errors as file:line with the failed goal. It ships as a command-line tool and a Claude Code skill, and has no Python dependencies.

Which one to use

Both the LSP client and isabelle-check drive a running Isabelle, but for different jobs. Use isabelle-check for the edit–check loop of an agent or script that edits theory files and needs to know what broke. Use the LSP client to look inside a proof: read proof states, try steps in memory, run sledgehammer, ask for hover information (tbl1).

Package dependencies

#direction: down #spacing: 50 #padding: 10 #.external: dashed fill=#ffffff [<package> python-isabelle-lsp-client|isabelle_lsp_client] [<package> python-lsp-client|lsp_client] [<package> python-isabelle-parser|isabelle_parser] [<external> Isabelle|isabelle vscode_server (isabelle-emacs fork)] [<external> lark] [<package> isabelle-check|isabelle_check] [<external> Isabelle server|isabelle server] [python-isabelle-lsp-client] -> [python-lsp-client] [python-isabelle-lsp-client] --> JSON-RPC over stdio [Isabelle] [python-isabelle-parser] -> [lark] [isabelle-check] --> JSON over TCP [Isabelle server]

Solid arrows are Python package dependencies; dashed boxes are not part of this project. The Isabelle client imports the generic LSP client and runs Isabelle as a subprocess, speaking JSON-RPC over its standard input and output (the dashed arrow). The parser stands apart: it needs neither the clients nor Isabelle, which makes it the cheap way to look at a theory — and the only way when there is no prover to ask. The checker stands apart too: it speaks Isabelle’s own server protocol rather than LSP, so it needs neither client.

Incremental checking for agents

An agent working on a proof edits a theory, checks it, reads the errors and edits again, many times over. Checking with isabelle build re-proves every theory of the session each time. isabelle-check keeps the checked theories in a running Isabelle session, so a check costs only the theories an edit affects (tbl2).

The first check is slower than a build, but it happens once per session. After that, the saving depends on where the edit falls. Reuse works per theory: Isabelle’s headless session re-checks a changed theory in full, together with every theory importing it. An edit at the end of an import chain is cheap, and one at its root costs about a full build. The interactive session also accepts sorry without complaint, so the checker scans the files for sorry and oops and reports a result as clean only if there are none, as a strict build would.

What a check costs an agent in tokens is its output, which lands in the agent’s context. isabelle-check reports errors as relative file:line with the failed goal, and a clean result in one line; isabelle build adds absolute paths, goals broken across lines, timing and a pointer to the build log. Per check, that makes isabelle-check 2–4.5 times cheaper than isabelle build, and 8–33 times cheaper than isabelle build -v (tbl3).

In absolute terms these are small numbers: a check costs tens to a few hundred tokens either way, while each turn of an agent re-reads tens of thousands. A hundred edit–check cycles save some 10,000–30,000 tokens. The larger gain is time: checking just the edited theory took 0.3 s against 25 s for the build.

Parser coverage on the AFP

The parser’s coverage of the Archive of Formal Proofs is still low-ish. Of a seeded random sample of 500 theory files from the afp-2026-09-11 release, measured on 14 September 2026, only 29% parse (tbl4).

The measure is strict: one unsupported statement fails the whole file. The rejections come from inner-syntax terms with exotic notation, some proof methods and a few rarely used commands the grammar does not cover yet. The timeouts come from the Earley chart, which grows super-linearly on large or highly ambiguous files; even a file that parses takes a median of 2.1 s. A successful parse is authoritative, and a failure means “not yet supported” rather than “invalid Isabelle”. The numbers are refreshed weekly in the parser’s README.

Installation

None of the packages is on PyPI yet. Install from GitHub, the LSP client first, since the Isabelle client depends on it:

1
2
3
4

pip install git+https://github.com/christiankissig/python-lsp-client.git
pip install git+https://github.com/christiankissig/python-isabelle-lsp-client.git
pip install git+https://github.com/christiankissig/python-isabelle-parser.git
pip install git+https://github.com/christiankissig/isabelle-check.git

The checker needs no other package. On a git checkout of Isabelle, such as the isabelle-emacs fork, create the distribution id that isabelle server expects once (the checker’s README shows how).