Stream: Announcements

Topic: Introducing AoA

Qiyuan Xu (Jul 22 2026 at 16:02):

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

:sparkles: AoA abstracts away from the concrete syntax of proof languages, representing proofs as abstract syntax trees via JSON schema.

This enables the first effective proof agent on a freshly redesigned language (Isabelle/Minilang) that commercial LLMs have had little exposure to, achieving 99.6% on miniF2F, 89.2% on NTP4VC-Pearl, and 97.7% on NTP4VC-realC. This success suggests 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.

:direct_hit: Combining Minilang with the tree-editing model, AoA achieves a 2.3–4.7x reduction in API cost, a 2.9–6.9x reduction in token consumption, and 1.4–2.0x faster in total execution time, compared to Amazon's Isabelle Agent — which is likewise built on Isabelle and equipped with Sledgehammer.

:document: Paper: https://arxiv.org/abs/2607.16372

:mechanical_arm: Source code: https://github.com/xqyww123/Isa-Mini

AoA is fully productized, supporting Windows, Linux, and macOS.

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

:mechanical_arm: AoA ships with proof caching: once a proposition is proved, it is never proved again unless the proof becomes invalid — zero redundant overhead.

AoA respects your projects! It quietly completes your proofs, never disturbs your Isabelle text, and produces no side effects beyond the target proof.

Qiyuan Xu (Jul 22 2026 at 16:57):

• 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

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

Future releases will be announced in #New Members & Projects > The proof agent AoA's update channel @ 💬

Last updated: Aug 15 2026 at 08:30 UTC