AoA: Theorem Proving Agent over the Abstract Syntax Tree of a Redesigned Language

The paper introduces Agent over AST (AoA), an interactive theorem-proving agent that operates on an abstract syntax tree rather than serialized proof text. The model emits JSON representations of Minilang’s AST and uses tree-edit operations that combine proof actions with the resulting subgoal states. According to the abstract, on common success sets from miniF2F and NTP4VC-Pearl against Amazon’s Isabelle Agent, AoA reduces normalized input-cache API cost by 2.3–4.7x, token usage by 2.9–6.9x, and tool calls by 3.9–8.9x, while completing proofs 1.4–2.0x faster and solving substantially more problems on the harder verification benchmark.