Three days of agent-driven mathematics

I’m not a mathematics researcher. My expertise is harness engineering and agent orchestration: building systems that let agents work independently, share useful results, and produce evidence that survives checking.

Over three days, I applied that to a research project on multiplying very large integers. By October 11, I had submitted 55 pull requests to a rapidly evolving community effort.

The question sounds elementary: how efficiently can two numbers be multiplied? At enormous sizes, the answer depends on intricate algorithms. This project studies an exponent saving, called κ, within a proposed mathematical framework. A larger κ means a better theoretical growth rate. It doesn’t mean your laptop suddenly multiplies numbers that much faster.

My first submission was PR #43. From there, the work expanded into circuit design, search algorithms, memory reuse, exact verification, and formal certificates.

The working setup ran from my Mac, with searches and verification distributed across my two DGX Sparks. Agents had separate workspaces, bounded compute allocations, and distinct responsibilities. Some explored changes close to the current best construction. Others investigated larger departures or checked whether a proposed improvement actually held up.

The difficult part was keeping that work coherent while the underlying research changed. An agent could spend hours improving a construction, only for another contributor to publish a stronger starting point. We had to preserve useful discoveries, move them onto the new construction, and check the combination again.

Even two individually valid improvements could interfere. In one case, different agents were changing overlapping parts of the same computation. Their gains couldn’t simply be added. The work had to be separated, recombined, and priced as one complete construction.

Early improvements came from changing the order of operations. In PR #48, reordering a family of sums allowed more intermediate storage to be reused. The resulting construction removed 847,550 wires from its accounting while preserving the outputs.

Later, the agents started changing the circuits themselves. One result was counterintuitive: doing more arithmetic locally could make the overall construction cheaper. A circuit with 29 additions instead of 27 created more opportunities for reuse and reduced the auxiliary storage required. That became PR #181, followed by further circuit changes in PR #200.

This made the choice of objective crucial. Minimizing the number of additions alone would have missed the improvement. Candidates needed to be evaluated through the full accounting pipeline.

Some of the most useful work established where to stop searching. PR #212 showed that a particular kind of tuning had at most roughly 1.8% left to gain on the fixed construction. That gave us a concrete reason to look for a different design.

In PR #296, an exact constraint solver proved the existing local design optimal within the specified search class. But another equally optimal design allowed substantially more reuse elsewhere. A separate module also reached its proven local minimum. Together, these produced a better construction.

That distinction kept recurring: the best isolated component wasn’t necessarily the best component to assemble into the whole.

The headline number also hid useful contributions. PR #233 improved one major component by about 1.28%, but another component remained the bottleneck, so κ didn’t move. Much later, PR #417 raised another component’s limit by about 2.2%, again without changing κ. Both created room for subsequent improvements.

Verification became a substantial part of the work. In PR #256, we exported a construction as an explicit numbered program that Jacob Sussman’s reference checker could inspect, and connected it to his Lean framework. That established specific machine-checked properties; it did not formally prove the entire multiplication theorem.

We also improved the tools themselves. A change to how retired registers were organized reduced one complete verifier run on a Spark from 128.2 seconds to 49.7 seconds, with its selection behavior preserved. That was a measured engineering improvement, separate from the mathematical bounds. PR #175

This was deeply collaborative work. My submissions built on other contributors’ circuits, layouts, and proofs. Later packages reused our pairing methods, physical-circuit checks, and kernel-checking machinery. Progress traveled through code and certificates as well as through larger values of κ.

By my latest submission in this snapshot, PR #432, the reported conditional saving was approximately 0.00101975. Other submissions reported larger values under different mathematical interfaces. Those distinctions matter: a promising construction, a successful finite replay, and a complete theorem are different levels of evidence.

What interests me most is how much substantive work this setup made possible. The agents explored constructions, found improvements, established limits, and produced artifacts others could examine and reuse. My contribution was building and operating the system around that work—and making sure each result carried enough evidence to be useful.