A coordination framework for formal proof development with Kiro

Large language models (LLMs) and coding agents are increasingly capable of proving difficult mathematical theorems and completing formally verified Lean programs. Yet, existing agentic provers rely on the backend models’ capabilities while lacking the ability to explore when they get stuck: when a proof resembles patterns the model already knows, it might succeed quickly. When it doesn’t, the model can spend thousands of tokens repeating failed tactics, lose track of intermediate results, or abandon the proof altogether.

We develop a prover harness, MAESTRO, in Kiro CLI that gives LLMs a systematic framework for exploring, decomposing, and making structured progress on difficult problems. The prover constructs a shared proof skeleton and organizes the work across specialized agents that explore independent proof obligations concurrently. A persistent coordinator evaluates their feedback, repairs broken proof structure, and decomposes difficult goals into smaller lemmas when direct attempts fail. This turns proof generation into an iterative process of planning, proving, diagnosing, and revising.

We test on a series of challenging benchmark datasets, including ArxivLean (research-level mathematical theorem proving) and FormalQualBench (graduate-level mathematical theorem proving). Across these, Kiro CLI with GPT and Claude models consistently solves more hard problems than Codex and Claude Code with the corresponding models. We apply Kiro CLI to prove the six problems from the 2026 International Mathematical Olympiad (IMO, held July 15–16, 2026). Kiro CLI solves all six problems in 1 hour 46 minutes. Previously reported total times were 8 hours 18 minutes for Humanfia and 24 hours 56 minutes for AxiomProver. We also find that Kiro CLI can discover and test novel proof strategies, suggesting potential applications in mathematical research.

Kiro CLI strengthens base LLMs’ proving capabilities

We evaluate Kiro CLI across several established benchmarks and compare it against plain agent harnesses, Codex and Claude Code, using the same underlying base models. These benchmarks are:

• PutnamBench, formalized undergraduate Putnam competition problems.
• FormalQualBench, graduate qualifying-examination problems.
• ArxivLean, theorem statements drawn from recent research papers.
• Neural Theorem Proving for Verification Conditions (NTP4VC), verification conditions extracted from real-world software-verification projects.

Together, they span diverse levels and domains of formal reasoning. Across this spectrum, Kiro CLI consistently achieves higher solve rates, with the gap becoming particularly pronounced on the harder research-level problems. This suggests that the gains are not simply because of stronger base models. The specialized coordination machinery in MAESTRO makes a substantial difference in how effectively those models can solve difficult mathematics.

We evaluate Kiro CLI across five reasoning-effort levels for GPT 5.6 Sol and Claude Opus 5 on a dataset comprising six challenging IMO 2026 problems, formalized by AxiomMath. With GPT 5.6 Sol, Kiro CLI solves five of the six problems at low effort and all six at medium effort or higher. By comparison, Codex solves none at low effort, three at medium, five at high, and all six at the two highest levels. With Claude Opus 5, Kiro CLI solves all six problems at every effort level. Claude Code solves three at low and medium effort and five at each higher level. These results demonstrate that our harness substantially strengthens the base models’ theorem-proving capabilities.

Figure 1: Solve rates across five reasoning-effort levels on the IMO 2026 problems

Kiro CLI outperforms existing custom solutions

We compare Kiro CLI with existing proving systems on the IMO 2026 dataset. Across all six IMO 2026 problems, Kiro CLI completes the proofs in 1 hour 46 minutes. Compared with 8 hours 18 minutes for Humanfia, 8 hours 57 minutes for Pramaana, and 24 hours 56 minutes for AxiomProver, Kiro CLI is 4.7×, 5.1×, and 14.1× faster, respectively. The advantage is consistent across the individual problems, suggesting that the coordination framework improves not only success rate, but also the efficiency with which difficult proofs are found.

Figure 2: Proof-completion times for Kiro CLI vs. existing custom solutions on IMO 2026

The core of the Kiro CLI prover: Coordination

The core of the Kiro CLI prover harness is coordination. Rather than treating theorem proving as a collection of independent lemma-solving jobs, it maintains a single evolving proof plan. Prover agents work on individual obligations and return checked lemmas, counterexamples, partial proofs, and structured reports about what is or isn’t working. A persistent coordinator reads this feedback together with the current Lean development and continuously revises the global proof architecture. It can preserve useful results from a failed branch and repair broken interfaces between lemmas. When a helper is false, it retracts both the helper and the downstream structure that depends on it. The coordinator can also introduce new abstractions, redirect workers, or leave productive branches alone. This allows local discoveries to influence the entire proof rather than being lost inside isolated attempts. In particular, the prover can recognize a flawed decomposition and restructure the proof around new evidence. Moreover, it can discover novel mathematical arguments.

Example 1: Repairing the proof architecture

We see this behavior in an Opus 5 run on the Quillen–Suslin theorem from FormalQualBench. At one point, a worker proposed simplifying the proof by keeping track of only part of the algebraic structure after a localization step. A later worker found a concrete counterexample showing that this simplification had thrown away information that was essential to completing the proof. In fact, the proposed intermediate lemma was stronger than what the original theorem required and would imply a substantially harder open statement.

Rather than repeatedly trying to prove the bad lemma, the coordinator recognized that the proof had been decomposed incorrectly. It recorded the counterexample, rejected later proposals that made the same mistake, and redesigned the intermediate interface so that both complementary pieces of the structure were preserved. After this information was carried through the remaining steps, the two pieces could be recombined into a global basis and the proof completed.

Example 2: Discovering novel proof strategies

Coordination can also lead Kiro CLI to discover new mathematical constructions. One example comes from the ArxivLean theorem Real Matrices as Linear Combinations of Three Orthogonal Matrices.

Both the original paper and our prover begin with the same standard simplification: reduce the matrix problem to a problem about its singular values. From there, however, the proofs diverge. The original paper first solves the easier case in which all singular values are distinct. When some values are repeated, it slightly perturbs the matrix to remove these repetitions, applies the distinct-value construction, and then uses a limiting argument to recover the original matrix. Our prover instead found a direct construction that works even when singular values are repeated. It groups the singular values into overlapping two-dimensional blocks and chooses intermediate values so that neighboring blocks fit together consistently. These local constructions then telescope into three global orthogonal matrices whose linear combination gives the original matrix.

Thus, it doesn’t merely translate the argument from the paper into Lean. It introduces different intermediate objects and reorganizes the proof around them, producing a route that directly handles the case for which the original proof uses perturbation and compactness.

Conclusions

Proof development isn’t only a collection of frontier model workers working individually. What matters is how we organize the work. MAESTRO in Kiro CLI is built around this observation: individual provers explore locally, while a persistent coordinator accumulates evidence and continuously reshapes the global proof. Through this coordination-heavy design, the prover has reached nearly saturating performance on several benchmarks of competition-level formal mathematics, while also showing promising results on substantially harder, research-level problems. You can find more technical details about MAESTRO in our paper, Maestro: Agentic Formal Proof Development by Coordination.

About the authors