Qiyuan Xu

Introducing AoA (Agent over Abstract Syntax Trees), our proof agent built on Isabelle/HOL. 🎯 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: ✨ 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. ✨ 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. 📄 Paper: arxiv.org/abs/2607.16372 🦾 Source code: github.com/xqyww123/Isa-M… 🙏 Huge thanks to my amazing co-authors @joshuaongg21 , @realReasonWang , @WendaLi8 , @haonanlp , Luke Ong, and @conrad_watt — it has been a true honor working with you all.

Also appreciate the author @realReasonWang !

AoA is fully productized, supporting Windows, Linux, and macOS. One-line install: conda create -n isabelle -c conda.qiyuan.me -c conda-forge isabelle-ai One-line usage: theorem "sqrt 2 ∉ ℚ" by aoa 🦾 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`. 🛡️ 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.

@arxiv Also, it's 6202, 4 thousand years after the rise of AI and LLM. So why don't you introduce an AI-based automatic moderation system instead of squeezing your human reviewers

Is your arXiv submission on hold? We promise it's not a conspiracy 😬🛸 Unfortunately, a record year for submissions=record queue of holds. If you (understandably) want to vent your frustration, the following can help us track the issue: 1. Category 2. Submitting Author 3. Title

@arxiv 1. cs.PL 2. Qiyuan Xu 3. Theorem-Proving Agent over Abstract Syntax Tree of Redesigned Language Please I'm not a robot. The article is not generated by AI. We spent a half year working on this work. 🥲🥲🥲

@EigHtNovel your songs definitely deserve!

@XeroEssential thank you!!😭