Following the recent success of AI in solving longstanding math conjectures, I decided to try it on my favorite math conjecture: Petty's conjectured inequality. Open for more than fifty years, from the field I did my PhD in and left years ago. An AI research team, with some steering on my end, indeed found a proof of a significant special case of that conjecture.
I ran this experiment because I wanted to understand the current state of AI, on a problem where I'm in a relatively unique position to judge the output. This is an account of my observations, and some thoughts on the trajectory of AI in math and beyond.
The result
Petty's conjectured projection inequality has been open in convex geometry since 1971. It's a beautiful piece of mathematics that, if ultimately true, can be understood as a deeper truth behind the familiar fact that among all shapes of a given volume, balls minimize surface area. Petty's inequality would sharpen this. It's a stronger, affine-invariant statement from which the classical isoperimetric inequality follows.
What the AI research system found is a proof for a special class of bodies: those with rotational symmetry around an axis. Not the full conjecture, but significant progress, and the first result for a non-trivial global class of bodies. I've convinced myself that the core arguments are sound, and the proof has been formally verified in Lean.
I've since learned that Florian Mielke-Sulz found two proofs of the same result independently and a bit earlier. I'll defer to him for publication.
The research loops
As of this writing, Fable 5 is probably still the most creative and intelligent model. I used it as the principal researcher and had it delegate work and verification to the somewhat less creative but faster, cheaper, and more diligent GPT 5.6 Sol. Each principal research thread runs in a loop with a standing instruction to manage and iterate on proof attempts, producing new ideas when an attempt doesn't work or gets stuck. Research threads across multiple machines are coordinated through a git repo with rules for maintaining a research log.
I later added a second type of researcher: a GPT 5.6 Sol loop as a wrapper around GPT 5.6 Pro, seemingly the strongest model at math, which is only available in the chat app (or via a very expensive API). This loop, running in Codex, handles coordination with the rest of the program and sends context to GPT 5.6 Pro via browser use. Pretty hacky, but it paid off. Building on the previous work, 5.6 Pro found the critical argument of the proof.
Once in a while I had a thread explain research progress and current focus to me. Sometimes I'd spot a research lane that had maneuvered itself into a rabbit hole with diminishing returns and prompt it to step back and look for new ideas. Occasionally, I pushed a specific idea to be pursued further. When the program seemed to stall, I decided to pivot efforts to the rotationally symmetric case, which was more tractable but still contained real insight for the full problem. The system otherwise ran autonomously, often for a day or night at a time.
The shape of the machine intelligence
It was impressive to watch the AI researchers skillfully experiment with a vast array of existing proof patterns against the problem and finally crack the puzzle. Unsurprisingly though, given its approach, the solution contains no novel methods applicable to a wider range of problems. A high bar, to be fair, but one that all AI results in mathematics so far seem to have failed to clear. In contrast, for problems of this caliber, human solutions often do leave new methods behind, even when they fail. The intelligence at work here appears to be superhuman in breadth and speed but lacking in what I'll call creativity: the ability to generate explanations that are deep and novel relative to pre-existing experience. That it is relatively lacking here is hard to deny. If it weren't, we ought to be seeing far more math breakthroughs than we are given its superhuman ability otherwise.
To what extent does the apparent lack of genuine creativity matter?
In mathematics itself, probably the least. Essentially all mathematical knowledge is available as training data, and a proof is either correct or it isn't, with checking far easier than finding. This verifiability allows for rapid trial and error, producing more data in the process. Compute turns into data. Due to these characteristics, scale alone will likely be enough to eventually solve most open problems, even with limited creativity. How fast this progresses towards AI developing new fields to crack conjectures remains an interesting question.
All of this makes math an interesting laboratory for understanding the limitation. Math is where the lack of creativity is easiest to compensate for, so whatever it still costs there is a lower bound on what it costs elsewhere. Imagine, for instance, an experiment where the AI is seeded with only the mathematics known around 1800. It might well prove, in an ad hoc way, that fifth-degree equations have no general solution formula. But just how much more compute would it need to also invent group theory, the framework that explains why?