대화형 정리 증명 (Interactive theorem proving, ITP)은 프로그램 검증과 형식화된 수학의 근간을 이루지만, 수동 작업의 부담으로 인해 확장성에 한계가 있습니다. LLM 기반 증명 에이전트는 이러한 노력을 완화할 것으로 기대되지만, 과도한 토큰 소비와 API 비용이 주요 장애물로 남아 있습니다. 우리는 이 비용의 원인이 공통된 근본 문제에 있음을 추적했습니다. 현재의 에이전트들은 직렬화된 구체적 구문 (concrete syntax) 위에서 동작하며, 증명을 소스 텍스트로 출력하고 별도의 줄 번호 기반 쿼리를 통해 증명 상태를 복구합니다. 이로 인해 모든 수정 사항이 이후의 줄들을 밀어내게 되어, 오류와 상태의 위치를 반복적으로 재조정해야 하는 상황이 발생합니다. 이러한 구체적 구문에 대한 의존성은 최근 LLM 기반 증명에서 SOTA (State-of-the-Art)에 도달했으나 LLM의 학습 코퍼스에는 너무 생소한 최신 증명 언어인 Minilang의 채택을 가로막기도 합니다. 우리는 에이전트를 소스 텍스트에서 추상 구문 트리 (Abstract Syntax Tree, AST)로 격상시킴으로써 두 가지 문제를 모두 해결합니다. 모델은 도구 호출 (tool-calling) LLM에 친숙한 Minilang AST의 JSON 표현 방식으로 증명을 제공하며, 증명 작업과 상태를 하나의 증명 트리로 융합하는 트리 편집 모델 (tree-edit model)을 통해 증명기를 구동합니다. 이를 통해 각 작업은 자체적인 하위 목표 (subgoal) 상태를 보유하게 되며, 트리를 통해 직접 읽을 수 있습니다. 우리는 이러한 설계를 \emph{Agent over AST} (AoA)로 구현했습니다. miniF2F 및 NTP4VC-Pearl 공통 성공 세트에 대해 Amazon의 Isabelle Agent와 비교했을 때, AoA는 API 비용을 2.3--4.7배 절감하고 (입력 캐시를 고려한 정규화 기준), 토큰 사용량을 2.9--6.9배, 도구 호출을 3.9--8.9배 줄였으며, 수행 속도는 1.4--2.0배 더 빨랐습니다. 동시에 더 어려운 검증 벤치마크에서 훨씬 더 많은 문제를 해결했습니다.