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

Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this e…