What Is It Like to Do Math Research with Frontier Agents?

TL;DR: I proved novel math results using frontier models.

The experience made one thing clear: regardless of domain, if you have the ability to take big problems and break them down well, these models are a huge lever to compound your abilities. If you are a low-level execution monkey without the ability to see the bigger picture, these models will replace you.

In the last 8 months, the way software is developed has changed completely. As someone who has written software almost every day for a decade, I have a deep touch and feel for the ways in which it has changed. In some ways, it matches (or even exceeds) the hype I see on Twitter, but in other ways it falls short.

Frontier model labs have been teasing that the same step change is here for math research — multiple labs have won IMO gold medals with their models and, as of a month ago, OpenAI announced that GPT 5.5 Pro contributed a new result on a core, well-studied problem. In the same way that you can’t develop a touch and feel for how software development has changed without using the tools to do software development, I didn’t know what to make of these math results.

The trouble is, assessing a model’s math capabilities (and not just math recall) is far more challenging than assessing its coding capabilities — any nontrivial codebase doing anything interesting is probably novel in some way, and you can readily see the agent’s ability to work in-context. The same is not true with math — (almost) everyone’s using the same set of standard definitions, so unless you’re working on the frontier of mathematics, the question you’re posing is likely in a paper somewhere and, by extension, in the model’s training data; the model could simply be recalling the answer to your question rather than developing a novel line of reasoning.

So, to do a test for myself, I decided to work with the models on an open problem in an incredibly niche area of graph theory. I am not a mathematician, but I do have a PhD in CS, a decent math background including graduate-level graph theory, and I have published papers on graph search algorithms that, at their core, heavily leverage graph transformations. I think this is the only area of mathematics where I have sufficient background to meaningfully comment or contribute.

A Graph Theory Adventure

The setup

A few days ago, I stumbled across the 2022 paper Conditional Fractional Matching Preclusion for Burnt Pancake Graphs and Pancake-Like Graphs¹. In it, the authors explore a niche corner of graph theory:

In loose terms, matching preclusion asks how much damage a network can sustain before it loses a particular global pairing structure.

• burnt pancake graphs; a special case of pancake graphs, i.e., graphs formed by different ways you can flip stacks of pancakes that have been “burnt” on one side to mark direction (famously, Bill Gates’ only paper was on an algorithm for Pancake Sorting)
• a special setup for matching preclusion, i.e., the minimum number of vertex or edge deletions needed to preclude a special matching structure

The authors perform an inductive proof of the minimal preclusion edit for burnt pancake graphs, using a computer program (which, despite leveraging clever techniques like dynamic programming, still took almost a day to run) to check the base cases and then a constructive proof for the inductive case. The authors left the same problem for the standard “unburnt” variety of pancake graphs as an open problem, remarking that their approach of enumerating the base cases on a large set of graphs would likely require a computer cluster.

This is an extremely narrow problem, but that is precisely what made it useful as a test. It has a precise target, a published solution to a closely related problem, and small cases that can be checked computationally. At the same time, proving the result for every requires a general argument; simply searching more cases cannot finish the job. If the models could produce that argument, it would be much stronger evidence of novel reasoning than success on a problem that might have appeared in their training data.

I did a literature review (with Codex) and found no real follow-up work for the unburnt formulation, only adjacent problems. Because I understood this problem and the authors’ solution, and because no solution appears anywhere online, this felt like a perfect place to work.

The human insight

By definition, pancake graphs of stack size (denoted ) have degree for every vertex: one neighbor for each of the places to insert the spatula to do a legal flip. As discussed in the 2022 paper, this matching preclusion problem is not allowed to admit degenerate solutions (you aren’t allowed to just isolate a lone vertex), and so one way to construct a preclusion is to isolate a path , creating two leaves and hanging off a shared vertex . Thus, when deleting , two vertices are stranded at once rather than a single vertex. Using the fact that all vertices have a known degree , we know that to construct this path you have to delete all the other edges from and , leaving only their edges to (i.e., by performing deletions).

This line of reasoning provides an upper bound on the size of the fault set, but it felt clear to me that this was also required for a minimal construction of the preclusion. As the 2022 paper authors did, you can just brute-force a reasonably sized base case, but it wasn’t clear to me how to attack the inductive step to prove this was minimal.

Machine magic

If I had to prove this myself, I’d:

• draw a bunch of pictures of and try to construct example fault sets that were cheaper, in order to understand the substructure
• read other adjacent literature to understand their lines of attack and proof techniques
• talk to (or call) a friend for ideation
• reread my graph theory textbook

But I did none of that. Instead, I gave the line of reasoning above, plus the 2022 paper, to Codex. Codex only has access to GPT 5.5 Low to Extra High, not Pro, so I asked Codex’s 5.5 xhigh to use the Chrome connector to spin up five 5.5 Pro sessions, attack the problem in parallel using this intuition as a guide from five different angles, and have the Codex xhigh session itself ultimately assemble these ChatGPT results into a coherent final proof.

To be honest, I expected muddled sophistry, but what came out was an interesting (and correct!) construction of a proof. It contained two key ideas:

• focusing the accounting on creating the left-behind “witness set” of isolated vertices, not the fault set as done in the 2022 paper
• constructing a cost function that it used to perform the core accounting of costs for this witness set

These reframings should be credited to ChatGPT, not me. My intuition that was minimal turned out to be correct, and my description of the isolated and may have suggested that the problem could be sliced this way. But it did not occur to me to make the witness set the central object of the proof or to construct around it.

Of course, a clever-looking proof from a language model is cheap; the difficult part is determining whether it is actually correct. I checked the result in layers. First, the Codex session wrote a Python program that enumerated every witness set and confirmed the base case computationally. Next, I iterated on the definitions until the general argument was clear enough for me to audit directly. Finally, I gave the proof to fresh instances of GPT 5.5 Pro, Gemini 3.1 Pro, and Fable 5 and asked them to search adversarially for gaps and counterexamples.

Only after that process did I trust the result. The original output had been dense with jargon, but beneath it was a surprisingly cogent argument. We eventually arrived at the proof as written in the paper. I think its use of witness sets is elegant enough — and sufficiently different from the 2022 paper’s approach — to be worth publishing.

A second surprise: presentation

I’ve never been happy with the expository writing quality of LLMs. I think I write pretty well, and I like to think my writing is clear, direct, and information-dense while forwarding a new perspective. I feel that LLM writing is almost always the opposite. I semi-regularly write technical blog posts, and I’ve tried to give LLMs a solid, coherent bullet-point argument structure with the sole task of turning it into fluent prose, and every time I’ve abandoned trying to even salvage its output in favor of writing it myself.

I planned to write up the proofs myself by hand, but as an exercise I asked Fable 5 to take the core proof I’d developed, written in a creole of LaTeX and Markdown, and turn it into the paper. Shockingly, I actually felt its presentation was quite good. I think some of this can be attributed to the fact that Fable is a better writer than other models (GPT 5.5 writes like a redditor with a personality disorder), but I think a lot has to do with the structured nature of mathematics papers. Unlike CS papers, math papers start with a short, technical introduction / related work hybrid section, provide an overview of the main results, and then immediately dive into a series of proofs. In my opinion, Fable did an excellent job capturing this structure and provided a phenomenal first draft that only required a bit of expository polishing throughout.

After several rounds of polishing, Panagram certified the final paper as 100% human-written.

My Takeaways

These tools really are general purpose levers for people who see the bigger picture and have the clarity of thought to break things down cleanly.

In undergrad, I distinctly remember doing problem sets where, given a big problem, I had a deep intuition for how to break it down into subproblems, but I would sometimes struggle with recalling all the different low-level proof tactics. Because of this, I worked alongside another student who had trouble breaking the big problems down correctly but had phenomenal low-level proof abilities. I would break the problem down into subproblems and give a sketch of why I thought this was a reasonable high-level trajectory; then he’d take the lead on doing the low-level proof. We’d ultimately succeed or fail on the proof, and these outcomes would better inform my intuition about which subproblem formulation to try next.

For people who do math research using my high-level intuition style of approach, these tools are an enormous lever. Not only are you no longer bottlenecked on your low-level proof ability, your intuitions can get sharper, faster. The workflow above is essentially a GRPO loop for your own mathematical intuitions; it lets you take far more shots on goal, as well as do a post-game analysis to get a better touch and feel for why a shot did or did not work across multiple different agent efforts, at the speed you can read and type.

People who do math research using exceptional low-level proof-tactic abilities will see only modest value from these tools. They will likely get better by studying the agents the same way top Go players got better after learning from AlphaGo, but their productivity will likely remain roughly the same.

If you’re a software engineer, these conclusions should sound quite familiar: if you can do system design, coding agents are huge levers; if you are merely an implementation monkey, you’re getting cooked. A K-shaped future awaits.