Jul 2026
AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
AoA lifts the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directl...
Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang et al.
· arXiv.org · 0 citations