# Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research

arXiv: https://arxiv.org/abs/2608.15052 · HTML: https://mlsanity.com/paper/2608.15052/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 8 of its 19 references that are in the map.
- First posted on arXiv 15 Aug 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 8 of 8)

- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems](https://mlsanity.com/paper/2604.24021/) (2026)
- [Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory](https://mlsanity.com/paper/2607.06447/) (2026)
- [RMA: an Agentic System for Research-Level Mathematical Problems](https://mlsanity.com/paper/2605.22875/) (2026)
- [ProofCouncil: An LLM Agent for Solving Open Mathematical Problems](https://mlsanity.com/paper/2607.09474/) (2026)
- [Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generation](https://mlsanity.com/paper/2606.10806/) (2026)
- [MechMath Agent Team: LLM Driven Agents for Mathematical Research](https://mlsanity.com/paper/2607.04394/) (2026)

## Abstract (arXiv)

Andy is an autonomous mathematical research agent that turns a mathematical problem into a traceable proof. It solves or verifies a submitted problem, formulates a literature-grounded new problem through a research-value gate, and carries it through proof construction and final verification. It organizes proof steps in an executable DAG, verifies each step independently and binds the result to a certificate, retains verified work whose interfaces remain unchanged during local repair, and records the full path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. Starting from a self-triggered impulsive consensus result, Andy formulates a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The proposed hybrid control combines self-triggered impulses with execution delay and continuous feedback over a recovery window. After each delayed impulse, the feedback cancels the delayed error channel until the pre-impulse history leaves the active delay interval. Sufficient conditions for global exponential synchronization are established, Zeno behavior is excluded for both timing sequences, and a numerical example illustrates the result.