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 three 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.

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] [python-isabelle-lsp-client] -> [python-lsp-client] [python-isabelle-lsp-client] --> JSON-RPC over stdio [Isabelle] [python-isabelle-parser] -> [lark]

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.

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 (tbl1).

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

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