On 29 October 2026 Noema published A New Dawn For Mathematical Progress by Atoosa Kasirzadeh, a philosopher and mathematician, research scientist at DeepMind and assistant professor at Carnegie Mellon University. Her starting point is the results of recent months. On 4 September Anthropic announced the complete Lean formalization of Fermat’s Last Theorem, produced by Claude agents in eleven days. Then came the Navier-Stokes singularity of 8 September, the 722 manuscripts of 6 October and the announcements of 26 October, including the refutation of the ETH. Kasirzadeh writes that another Millennium Prize problem fell that day. OpenAI’s announcement, however, claims only the existence of Yang–Mills theory, which is one part of the problem, without the mass gap.

Two models of progress

Kasirzadeh calls the first model the checklist. Progress consists of ticking off a list of problems fixed in advance: the Mathematical Olympiad, Fermat’s Last Theorem, Freek Wiedijk’s hundred theorems to formalize, the Clay Mathematics Institute’s Millennium problems. Credit goes to whoever ticks first. It is the same logic as AI benchmarks, and it is the ground on which models are advancing fastest. Terence Tao speaks of an age of proof post-scarcity, in which proofs stop being a scarce resource.

The second is the generative encounter: mathematics advances when it meets a real problem that is on no list and draws new structures from it. The essay gives two examples.

  • George Dantzig, after his doctorate at Berkeley, worked for the US Air Force on planning military logistics, which was done by hand by thousands of clerks. To describe it he formulated linear programming, a name taken from military jargon, where program meant a plan: a linear objective and a set of linear constraints, which together define a convex polyhedron with the optimal solution at a vertex. The simplex method searches for that vertex by moving along the edges. When resources had to be whole units, planes or pilots, integer programming grew out of the same path.
  • Norbert Wiener, at MIT, started from an anti-aircraft problem: where to aim when the pilot changes course. He treated pilot, aircraft and gun as a single system with feedback and derived the theory of statistical prediction and filtering from it, then the cybernetics of 1948. His predictor was not widely deployed: the military contract went to a simpler Bell Labs design. The mathematics that came out of it remained.

Kasirzadeh adds that the hierarchy between pure and applied mathematics is a cultural prejudice that AI is forcing us to correct. Dantzig had already said so in an interview quoted in the essay: “Mathematicians are snobs.”

Four open fields

According to Kasirzadeh the urgent work lies in four clusters of problems that appear on no list:

  • provably safe cyber infrastructure;
  • a mathematical science of deep learning, still in its infancy;
  • the mathematics of multi-agent control, drawing on security, mechanism design and game theory;
  • the epistemology of machine-generated proofs, when they are too long or too alien to be understood.

She proposes moving the question from “Who proved it?” to “Who decided this was worth proving, why, and how did we make sure it was right?”. She closes by asking what would happen if a system came to decide which questions matter as well, and leaves the question open.

What I think

I recognise myself in Kasirzadeh’s question because it is the one I ask about AI systems in general. When producing answers is cheap, the work shifts to which questions to ask and how to verify the answers. This is what I mean by the human part of a governed superintelligence. I believe it also holds for the question the essay closes with: keeping people inside the system, at the point where what matters is decided.

On verification I would add a distinction. Lean’s kernel, the small program that checks every step, certifies that the proof is correct with respect to the statement, not that the statement is the right one. For Fermat the match was checked by an automatic comparison with the statement already in Mathlib, the library written and reviewed by the community. I discussed this for the ten certified proofs of August. Deciding what to formalize and checking that the formalization says what we mean remains human work. It is the fourth field Kasirzadeh names.

The first and third fields are close to the work I do every day, the security of infrastructure and the control of agents that interact with each other. In healthcare, security and public administration problems arrive the way Dantzig’s did, with constraints nobody has yet written in mathematical form. I believe that is where mathematicians and models can work together best. In mathematics, rigour has never held back creativity.

Cover image: the hominids and the monolith from “The Dawn of Man” sequence of “2001: A Space Odyssey” (Stanley Kubrick, 1968), recreated at the Museo de Cine Colin Arthur. Photo by MiguelAlanCS on Wikimedia Commons — CC BY-SA 4.0 — https://commons.wikimedia.org/wiki/File:Museo_de_Cine_Colin_Arthur_11_-_2001_A_Space_Odyssey.jpg — licence: https://creativecommons.org/licenses/by-sa/4.0/