By now, it's old news that after consuming roughly six billion output tokens, producing 13 million lines of Lean and proving more than 30,000 theorems over 11 days, Wiles's 1995 proof of Fermat's Last Theorem was formalized - Anthropic Post. This process is more properly called autoformalization.

While this is a momentous occasion and further proof that coordinated agents can dramatically reduce the labor that would be required by humans for many higher-order tasks, it was the method by which this was accomplished that caught my eye. In the first attempt, the agents "quickly lost track of the project's state and stopped collaborating effectively." It was only after switching to Prove2Me that the formalization was completed. Prove2Me uses a directed acyclic graph (DAG) of theorem statements. This provided a structured means of observing dependencies and what work was available, performing the work, and creating new dependencies and work items. Critically, this reduced memory degradation, which I will discuss momentarily. Instead of having one "manager agent", a work graph is created, workers can mostly be stateless, and as work is performed, the graph is updated. It's not hard to see that this is a big boon to parallelization, critical to formalization of a complex proof like Fermat's Last Theorem. But this type of work structure is not just pertinent to mathematical proof formalization. It supports a wide variety of agentic work patterns.

I have previously described (but not on buttondown) my method of working with coding agents. My AI-assisted coding practice is "pair programming" rather than autonomous agent campaigns. I use a "mixture of experts" pattern for most of my projects. I have an architecture agent (it's actually just an LLM chat session), one or more coding agents (normally Opus in GitHub Copilot, but more on this later), a code review agent, and myself. Over the last couple of years, I have created increasingly more structured patterns around this interchange of design and code, but I still end up performing what you might either call "human clipboard" or being the human intermediary in a Moltbook-style collaboration (agents talking to agents).

For a particular coding task or project, I create a master architectural document, iterate this design with the architecture agent and the coding agent (who is always a first-class design partner) and when "everybody is happy", the markdown file is committed to the repo. For more complicated projects, architectural decision records (ADRs) are also created.

During coding, I review all of the diffs and read all the code as it is written (I know, so old-fashioned!). Issues that come up in coding cause more design conversations with the architecture agent and this occasionally results in edits to existing, or the creation of new ADRs. Each PR goes through a human and agentic code review (typically Codex via GitHub CLI).

Although this sounds structured, it is both laborious (lots of markdown crossing the clipboard) and not very efficient in terms of context management. Without going down the deep rabbit hole of context maintenance in agentic coding sessions, let's just say for now that loss of relevant context is both annoying (repetition and bugs) and expensive.

Another interesting revelation in the Anthropic article is three ordinary consumer Claude Max subscriptions, coordinating entirely through Prove2Me, formalized Vinogradov's Three Primes Theorem in 3 days. The important point here is that the coordination structure itself scales down to smaller problem domains and much smaller resource budgets. That raises a further question especially interesting to me: how far can better external structure let us downscale the model itself?

The DAG provides several things at once:

• external memory
• problem decomposition
• synchronization
• provenance
• scheduling

The agent should not have to remember the project. The system should maintain the project state and compile the context required for each particular piece of work.

I've started calling this idea, somewhat unimaginatively, State Management of Compiled Context (SMCC). The spine of SMCC distinguishes two different kinds of state:

• Common Context - repo-wide facts which each node inherits what applies: architecture, invariants, conventions, known hazards, canonical terminology, build/test commands, avoid or "never do" constraints;
• Node-Local Context - the facts relevant to one task: dependencies, files, assumptions, open questions, acceptance criteria.

Completion of work is not just a checkmark, it emits context deltas: discoveries, changed assumptions, new dependencies, artifacts and proposed updates to shared state. Once accepted, those changes propagate through the graph, updating or invalidating downstream context as appropriate. This is a key improvement: we stop depending on conversational memory for cohesion.

This decomposition and downscaling insight is especially interesting since I am developing local inference primarily for the purpose of agentic pair programming. When I had basically unlimited tokens in a very large context window, I would often run extremely long sessions with a large amount of ambient context. This convenience was actually just a "lazy crutch." It turns out that a massive context window does not have perfect recall of every token in that context window and it is extremely wasteful (expensive). Better structure will reduce how much capability has to reside inside of each inference.

Instead of:

enormous model x enormous context x long-lived cognition

We can migrate to:

smaller model x decomposition x persistent state x retrieval x deterministic verification x smaller inferences

A basic software engineering lesson is that many problems which look like reasoning problems become much easier when represented as state-management problems. We have largely ignored that lesson with coding agents. When an agent forgets a fundamental repo invariant, our instinct has been to give it more context, better retrieval, or a smarter model. But some knowledge should not live in model memory at all. It should live in explicit state. We keep trying to solve state-management failures with more cognition.

Does this sound familiar? It should, basically this is the equivalent of a classic software production pipeline. It has many of the same elements: dependency graphs, source control, build systems, tests, static analysis and CI artifacts. Until now, we have been wrapping agents in conventional (LLM) orchestration rather than exploiting traditional structures as the persistent cognitive substrate.

And even if the structure does not decompose the problem to the level of Qwen 30B or similar, it makes large model cloud coding agents much more efficient (and therefore better suited to the task and less expensive to operate).

There is a key correlation to agentic safety. Others and I have written that we need to put safety into the deterministic end of the agentic systems, primarily via information flow control. This kind of graph foundation has at least two key advantages over the traditional orchestration we have been using:

• Observability is almost built-in - the graph is a durable trace of work, dependencies and state transitions.
• Human supervision improves because review happens at meaningful engineering boundaries, not over giant transcripts.

This shares some key attributes with runtime-control systems such as FIDES and Safe Agent Framework (SAF).

I struggled mightily with "what is wrong with how I code with agents" over the last couple of years. I think I finally understand what has been wrong. We have been doing this upside down (or backwards).

I have been compensating for the missing layer manually as I act as the state manager: carrying architectural decisions, discoveries, invariants and implementation progress from one agent interaction to the next. The markdown clipboard worked because it maintained the state that the agents themselves could not reliably maintain. But it was manual, untyped, inconsistent and dependent on me remembering what mattered.

The key insight then becomes:

Agents should inherit the structure of the engineering system in which they operate, rather than forcing the engineering system into the structure of a conversation.

In follow-on posts, I will dive into more of the architecture and implementation details of this idea. I am really excited about building an initial implementation and using it in all my future work. Maybe this will allow me (us) to escape the "upside down". 🙂