The traditional approach to solving optimization problems has been to use a robust and well-tested general-purpose solver. However, it is well-known in the community that instance-specific structure can be exploited to get large speedups compared to general-purpose solvers, albeit at a loss of solver flexibility and high implementation cost. In this post I show that LLM coding agents can easily and cheaply write specialized solvers from scratch, obtaining 10x speedups on average for narrow instance families. This suggests a new paradigm for building optimization solvers that uses LLM tools to automatically detect and exploit instance-specific structure.

Since models have gotten so much better at math, proofs and coding, I started thinking about other productive uses of the ever cheaper and more intelligent tokens, other than proving theorems and solving open math problems.

Towards harnessing models’ capabilities for accelerating real-world problems, I think it’ll be incredibly useful to build a comprehensive dataset of optimization problem instances, and agents have gotten smart and cheap enough to make this happen. I started with semidefinite programs (SDPs) as they constitute a relatively small class that I’m quite familiar with.

Five months have passed since I first built a harness to automatically prove and verify a conjecture from my PhD work. Since then, there have been many step changes in LLM capability, necessitating many revisits/refinements of my workflows. In this post, I summarize these observations, reflect on the rapid progress of LLMs, and lay out my thoughts on how to prepare for the future.

At the start of 2026, I noticed that LLM agents are becoming more capable at solving math problems, and began to use them for theorem proving. Early April, I ran an automated theorem proving experiment on a nonconvex optimization problem from sum-of-squares optimization, an extension of of my PhD work.

The goal was to give an agent a formal theorem statement in Lean, a computational search toolkit, and a verification harness, then let it autonomously work through the whole cycle that my coauthors and I previously went through: search for counterexamples, infer structure, write a mathematical blueprint, formalize the proof, and keep going until Lean accepted the final theorem.

Over roughly three days of continuous work, the agent produced about 58k lines of Lean, 2k lines of Julia, 7.5k lines of LaTeX, and more than 200 commits before finally proving the theorem.

I’ve been using OpenAI’s Codex for programmatically verifible tasks that can take a long time to complete, such as formalizing a proof in Lean, or using autoresearch to iteratively improve ML models. Codex tends to stop at reasonable-looking milestones even when the next step is obvious, which can be a pain when I want it to run unattended. A Stop hook that injects a continuation prompt fixes it.