Isabelle/Minilang

A minimalist proof language for Isabelle/HOL, designed for machine learning and LLM agents.

News 🎉🎉🎉

We release the AoA agent, now the primary interface for proving with Minilang. AoA is a proof agent built on Minilang, exposed as an ordinary Isabelle proof method: on any goal in any existing Isabelle context, simply write by aoa and the agent takes over.

theory Scratch
  imports Complex_Main Minilang_AoA.Minilang_AoA
begin
  theorem sqrt2_not_rational: "sqrt 2 ∉ ℚ"
    by aoa
end

AoA integrates seamlessly into existing proof developments — no fine-tuned model, no local LLM infrastructure to set up, no changes to your theory files. The agent never edits/touches your Isabelle script: all of its work happens in the background, and its effects are confined to the target proof context (here, the one opened by sqrt2_not_rational); outside that context, anything is untouched.

The proof found by aoa is saved to a separate file (scratch.proof-cache in the example above). Replaying by aoa reuses the stored proof directly — the agent is not re-run and no API cost is incurred — unless the cached proof no longer holds, in which case the agent is automatically invoked again.

Read AoA User Manual for how to install and other details.

Key Features

Minilang eliminates the human-oriented complexities of Isabelle/Isar, letting language models focus on high-level proof planning while delegating fine-grained reasoning to classical automation (Sledgehammer & friends). What started as a minimal proof shell has grown into a full stack:

• Minilang — a minimalist proof language with only ~10 core operations, each with clear semantic distinctions (OOPSLA'26 paper)
• Translator — a rule-based Isar → Minilang translator that has converted ~85% of ~340K existing Isabelle/AFP proofs into a large-scale training corpus (code)
• AoA Agent — Agent over AST: a token-efficient LLM proof agent that edits Minilang proofs directly as JSON abstract syntax trees, usable from inside Isabelle via a single by aoa method (paper, code, README)

Visit our Example Gallery to see more.

AoA: Agent over AST

The AoA agent answers a practical question: how do we cut the prohibitive API cost of LLM proof agents, and how do we let general-purpose LLMs write proofs in a language for which they lack corpus-scale exposure?

• AST-native interaction: instead of emitting source text and re-locating states by line numbers after every edit, the model supplies proofs as JSON representations of Minilang's AST — a format native to tool-calling LLMs — and drives the prover through a tree-edit model.
• Proof tree = operations + states: proof operations and proof states are fused into one tree, so each operation carries its own subgoal's state, readable directly off the tree without separate queries.
• Token- and cost-efficient: against Amazon's Isabelle Agent on the miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3–4.7×, uses 2.9–6.9× fewer tokens and 3.9–8.9× fewer tool calls, and finishes 1.4–2.0× faster — while solving more problems on the harder verification benchmark.
• No fine-tuning required: works with general-purpose LLMs out of the box, with drivers for Claude Code, Codex, and OpenAI-compatible / Anthropic APIs.
• One-line usage inside Isabelle: invoke the agent on any goal simply with the proof method by aoa.

See the paper: Theorem-Proving Agent over Abstract Syntax Tree of Redesigned Language.

Proven effectiveness of Minilang for Neural Theorem Proving

Fine-tuning LLMs on the Minilang corpus (instead of raw Isar) improves the pass@1 success rate on the PISA benchmark by up to 20/29 percentage points compared to Isar-based models with/without Sledgehammer:

• pass@1 reaches 69.1%, exceeding Baldur's pass@64 (65.7%)
• pass@8 reaches 79.2%, exceeding the previous SOTA on PISA (71.0%, Magnushammer)

See the paper: A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL.

The corpus & translator

• Rule-based translation from Isar to Minilang via three strategies: elaboration (make implicit information explicit), normalization (consolidate diverse idioms into uniform representations), and elimination of tactics (replace tactics with Sledgehammer*, except those matching informal reasoning).
• ~290K proofs (85.25% of ~340K Isar proofs from Isabelle/AFP) successfully translated, forming one of the largest structured proof corpora for machine learning. Available on Hugging Face.

Citation

If you use Minilang or this repository, please cite:

@misc{xu2026aoatheoremprovingagent,
    title={AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language}, 
    author={Qiyuan Xu and Joshua Ong Jun Leang and Renxi Wang and Wenda Li and Haonan Li and Luke Ong and Conrad Watt},
    year={2026},
    eprint={2607.16372},
    archivePrefix={arXiv},
    primaryClass={cs.SE},
    url={https://arxiv.org/abs/2607.16372}, 
}

@article{10.1145/3798275,
    author = {Xu, Qiyuan and Wang, Renxi and Wang, Peixin and Li, Haonan and Watt, Conrad},
    title = {A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL},
    year = {2026},
    issue_date = {April 2026},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {10},
    number = {OOPSLA1},
    url = {https://doi.org/10.1145/3798275},
    doi = {10.1145/3798275},
    month = apr,
    articleno = {167},
    numpages = {26},
    keywords = {Interactive Theorem Proving, Isabelle/HOL, Large Language Models, Neural Theorem Proving, Proof Language Design}
}