Stream: New Members & Projects

Topic: The proof agent AoA's update channel

Qiyuan Xu (Jul 27 2026 at 03:19):

This thread is dedicated to AoA news. Discussion is also welcome.

Introducing AoA (Agent over Abstract Syntax Trees), our proof agent built on Isabelle/HOL.

:direct_hit: AoA achieves 99.6% on miniF2F, 89.2% on NTP4VC-Pearl, and 97.7% on NTP4VC-realC, while delivering a 2.3–4.7x reduction in API cost, a 2.9–6.9x reduction in token consumption, and 1.4–2.0x faster total execution time compared to Amazon's Isabelle Agent — which is likewise built on Isabelle and equipped with Sledgehammer.

These results are powered by two key innovations:

:sparkles: AoA abstracts away from the concrete syntax of proof languages, representing proofs as abstract syntax trees via a JSON schema. This enables the first effective proof agent on a freshly redesigned language (Isabelle/Minilang) that commercial LLMs have had little exposure to — suggesting that the LLM era, far from stifling new languages, can actually accelerate their development.

:sparkles: AoA also abandons the traditional agent interaction paradigm of source-code editing with line-number indexing, adopting a novel tree-editing model that eliminates the line-number drift issues that conventional agents often struggle with.

:document: Paper: https://arxiv.org/abs/2607.16372
:mechanical_arm: Source code: https://github.com/xqyww123/Isa-Mini

Qiyuan Xu (Jul 27 2026 at 03:19):

One-line install:

conda create -n isabelle -c https://conda.qiyuan.me -c conda-forge isabelle-ai

One-line launch:

conda activate isabelle
isabelle jedit

One-line usage:

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

Important: AoA is nothing more than an ordinary tactic — you can use it as a drop-in replacement anywhere you'd normally write by auto or a much longer proof ... qed. In this way, AoA respects your project. Unlike existing agents that may extensively rewrite your project, AoA never touches your Isabelle text and produces no side effects beyond the target proof.

Qiyuan Xu (Jul 27 2026 at 03:24):

Update: isabelle-ai v0.2.0 is out. If you already have an older version installed, run conda update -c http://conda.qiyuan.me -c conda-forge isabelle-ai.

This release changes how the Isabelle semantics data is installed. Previously, the ~700MB download ran silently after conda create/install, making the install look like it had hung. It's now shipped and managed as a separate conda package, so conda create/install no longer stalls.

Kevin Kappelmann (Jul 27 2026 at 07:15):

Hi Qiyuan, do you believe the increased efficiency is largely due to the line-numbeded edits in Isabelle/Q? In PIDE MCP, we use string matching-based edits (which are standard in coding agents like open code). Maybe it is worth running it as an alternative competitor since a core claim of your approach is the increased efficiency of Isabelle source text editing.

Qiyuan Xu (Jul 27 2026 at 10:13):

Hi @Kevin Kappelmann, it's a good point! I will look into adding that experiment. We should indeed be careful not to attribute the cost reduction entirely to the tree-edit model. The gains of AoA come from two sources: the adoption of Minilang and the tree-edit model. These two are strongly coupled and difficult to ablate independently. My impression is that Minilang itself accounts for a non-trivial part of the simplification, though I don't yet know how much.

Qiyuan Xu (Jul 27 2026 at 10:18):

One more thing to note: AoA/Minilang is purely a proof language, which does not support theory-level declarations, unlike a full-stack MCP over Isar; AoA is merely a proof tactic.

Kevin Kappelmann (Jul 27 2026 at 11:49):

Ok thanks! I think an ablation study separating the effects of using minilang and the tree edits model would indeed be insightful.

Do I understand correctly that the agent emits tree edits using Minilang commands, the minilang commands are translated symbolically to standard isabelle commands, and the tree is translated symbolically to an Isar proof?

And the minilang language itself is limited to a fixed grammar, or is it user customisable to include new commands, say coinduction (if not already included) or user defined proof methods?

Qiyuan Xu (Jul 27 2026 at 14:22):

Good question! The first half is mostly right, but with one correction: Minilang commands are not symbolically elaborated into Isar text. Minilang is designed as a drastic simplification of Isar, but its implementation is largely independent — it has its own proof-script interpreter built directly on Isabelle/ML, driving the proof state itself rather than going through Isar as an intermediate representation.

The reason for this design is that it gives us more freedom to add harnesses around the interaction model and the feedback the agent receives. A few examples of what we do:

• Detection of free / schematic variables in subgoals — their presence usually signals a mistake, e.g. a forgotten universal quantification, so we surface this to the agent explicitly.
• Elaborated syntax errors — instead of the red squiggly underline in PIDE, we unparse the position markup into plain text so the agent can actually "see" where parsing broke, e.g. the parsing fails at `...λ 【here】λx. x` .
• Detection of so-called "consuming" premises of a rule in Induction / Case_Split (c.f. isar-ref.pdf, p. 157 of the 2025-2 edition). When the agent invokes induction or case-splitting without supplying the required consuming premises, Minilang emits a special message that switches the interaction into a question mode, explicitly prompting the agent to provide them, instead of letting the proof silently go wrong.
• Non-termination detection in rewriting — when rewriting falls into a non-terminating loop, Minilang detects this and notifies the agent, then falls back to a single-step rewriting mode: when multiple redexes are available, the LLM is asked to explicitly choose which one to rewrite.

In short, we deeply customize/hack the underlying interaction model and feedback channel, so that the agent either gets enough guidance to avoid the common pitfalls, or the pitfalls are mechanically simplified away altogether.

As for extensibility: the grammar of Minilang itself is fixed by design — we deliberately keep the command set small and closed, since the whole point is to give the agent a minimalistic surface. However, Minilang allows arbitrary Isabelle tactics / proof methods, including user-defined ones. Though not implemented yet, AoA's semantic retrieval module will allow users to write usage documentation for tactics, so that AoA can retrieve a custom tactic together with instructions on how to use it, and then apply it.

Kevin Kappelmann (Jul 27 2026 at 14:26):

OK thanks!

Qiyuan Xu (Jul 27 2026 at 14:27):

*by the "Detection of free/schematic variables" I actually meant undeclared/schematic variables

Last updated: Aug 05 2026 at 21:11 UTC