The NSF Mathematics Institutes: At the Nexus with AI
In October 2025, a scrum of mathematicians spent a week teaching partial differential equations to a computer, using a proof assistant and programming language called Lean.
The event proved a dynamic example of how the fleet of math institutes funded by the National Science Foundation—some long-standing, some founded in the 21st century—pioneer and innovate at the frontiers of science and technology, and at the nexus with artificial intelligence. SLMath’s Fall 2025 programming also featured a seminar, “The Future of Formal Mathematics is Here,” by Tudor Achim, the co-founder and CEO of Harmonic, an AI company dedicated to mathematical reasoning. Dr. Achim introduced Harmonic’s reasoning agent, Aristotle, and engaged in an extended ask-me-anything Q&A with mathematicians, whose queries ran the spectrum from skeptical to enthusiastic.
“Math is changing,” said the mathematician Tatiana Toro, SLMath’s director. “We need to engage with the technology—with the possibilities, the changing needs, and with the skeptics who have concerns.” Dr. Toro also noted, “The key is to keep fundamental math at the center: keeping in mind how the technologies depend on it, and how these tools have the potential to inspire new ideas and transform mathematics.”
Capitalizing on Formalization
The mission of the new institute, ICARM, at Carnegie Mellon, is to empower mathematicians to take advantage of new technologies for mathematical reasoning; which, in turn will make mathematical reasoning faster and more reliable in solving pressing challenges in science, security, and the economy in domains such as health care, data and digital threats, and finance.
The theory of partial differential equations (PDEs), for instance, is important for both applied and pure mathematics. PDEs are the language used to model real-world phenomena such as the dynamics of heat and fluid flow. Dating to the 18th century, their study has long motivated deep research problems and new conceptual developments.
Some mathematicians in attendance at ICARM’s inaugural workshop were experts on partial differential equations, such as the Navier-Stokes equations. Others hailed from different domains but were experts on how to formalize, or translate, mathematical statements—axioms, definitions, lemmas, theorems—into machine-readable code. The eclectic group made for “surprising synergies,” said mathematician Kevin Buzzard of Imperial College London, who attended via Zoom. “I am an algebraic number theorist and would not normally be interacting with PDE specialists. But because I am a longtime Lean user, I can collaborate with a PDE expert and work on writing PDE code in Lean, something which neither myself nor the PDE specialist could do alone.”
Jeremy Avigad, a professor in CMU’s math and philosophy departments, and ICARM’s director, emphasized that the new institute—a resource center, of sorts, staffed with “innovation engineers”—facilitates such collaborations and makes the technology more accessible. “There has been an explosion of interest in AI for mathematics,” he said. “The use of AI with formal libraries and formal reasoning brings exciting new opportunities.”
ART-2-detail-of-dependency-graph.jpg250.29 KBUsing AI tools—the proof assistant Lean and the autoformalization agent Gauss—researchers formally verified mathematician Maryna Viazovska’s Fields Medal-winning work on the optimality of certain 8- and 24-dimensional sphere packings. Pictured here is a detail of the Lean dependency graph visualizing the proof of the 8-dimensional sphere packing—the large circle spotlights the last few steps of the proof leading to the main theorem (for a bird’s eye view of the full dependency graph, see the end of the article).
CREDIT: Sphere Packing Project; David Renshaw, ICARM; Amelia Saul
The Causal Chain
Nearly two decades ago, the computer scientist Yann LeCun (and collaborators) started organizing a series of workshops about machine learning at the Institute for Pure and Applied Mathematics (IPAM) on the campus of the University of California, Los Angeles. The goal was to bring together mathematicians and computer scientists and engineers, theoreticians and practitioners, to help transform the technology.
“IPAM played a pioneering role in bringing the deep learning and mathematics community together in the late 2000s, long before deep learning took over the world,” said Dr. LeCun, formerly a vice-president and the chief AI scientist at Meta, who recently launched a new AI startup, Advanced Machine Intelligence Labs. From 2007 to 2020, Dr. LeCun served on the scientific advisory board of IPAM.
The machine-learning workshops led to a summer school program on “Deep Learning, Feature Learning” in 2012 — the same year that marked the big bang of the modern AI revolution. It was “an incredible success and played a critical role,” Dr. LeCun said of the program. “It really jump-started a community and motivated a lot of young mathematicians to engage.”
“It is crucial to realize that the technology we see now results from fundamental research five, ten, twenty years before in universities and in institutes like IPAM,” Dr. LeCun said. “That causal chain is very often lost.”
Fundamentals and Applications
Mathematics powers artificial intelligence in numerous dimensions, all of which inform and drive the mandates of the institutes. Fundamentally, mathematics underpins AI technology. “Math feeds into AI by supplying ideas about how to design and develop the systems,” said the mathematician Dimitri Shlyakhtenko, IPAM’s director. “In return, the success of AI calls for the development of its mathematical foundations and finding mathematical explanations for its effectiveness.” And, of course, AI is applied widely in the sciences, where mathematics is the universal language.
Over the years, multiple IPAM programs have investigated these themes. To mention but a few: a 2011 program on “Navigating Chemical Compound Space for Materials and Bio Design”; a 2023 workshop on Machine Assisted Proofs highlighted the use of AI to do mathematics; the 2024 “Mathematics of Intelligences” program aimed to establish mathematical foundations of natural and artificial intelligence; and a 2025 workshop explored “Sampling, Inference, and Data-Driven Physical Modeling in Scientific Machine Learning.” And AI figures prominently in multiple ongoing and upcoming events, including a 2026 long program on nuclear fusion; and a 2027 long program on scientific applications of AI focusing on certain areas of physical sciences.
Bridging Sectors and Scaling Up
For the Institute for Computational and Experimental Research in Mathematics (ICERM) at Brown University, a key part of the mandate is met through programs that bridge academia and national labs and industry. “The institutes provide a nimble and responsive environment for new developments, scaling up quickly for experimentation and collaboration,” said the mathematician Brendan Hassett, ICERM’s director.
“Fifteen years ago, it was about developing parallel computing and graphical processing units, and new algorithms that could take advantage of that architecture,” Dr. Hassett said. “Now, we are enjoying the fruits of that work. The computational infrastructure that makes AI models possible relies on that foundation.”
He added, “Engagement of the institutes with new technology, such as Lean, involves lots of intertwined activities. The fact that all of us engage with emerging topics allows them to scale quickly.”
A June 2025 workshop at ICERM zeroed in on “Scientific Machine Learning for Gravitational Wave Astronomy” — the ultimate goal was to maximize scientific insights from ongoing and upcoming cosmic observations. “AI techniques and machine learning are recasting computational strategies in applications like detecting and interpreting collisions of black holes,” Dr. Hassett said. “It’s a major investment by governments around the world that led to Nobel prizes.”
Similarly, the Institute for Mathematical and Statistical Innovation (IMSI), hosted at the University of Chicago, prioritizes interdisciplinary programs targeted at critical societal issues. And at that, “AI plays a role in the majority of our programs,” said the mathematician Kevin Corlette, IMSI’s director.
For instance, the spring 2023 program on “Mathematics, Statistics, and Innovation in Medical and Health Care” investigated the role of AI in improving diagnoses and treatment delivery. And a fall 2025 program was part of a series on “Digital Twins” — predictive computer models that mimic physical or social systems; applications run the gamut from aerospace to infrastructure to weather, and well beyond.
Dr. Gukov, a theoretical physicist and mathematician who also leads the Math + AI = AGI lab at Caltech, was initially skeptical of AI’s utility for his research. “I did an experiment on myself to make a measurement of whether AI is useful or not,” he said. The conclusion: AI accelerated his research by at least a factor of 10, and in some contexts by a factor of 100. “Then I took it seriously,” he said. “Now I’m trying to ask a more ambitious question in my lab: Can AI scale up math research not just by 10-x or 100-x, which is useful for everyday research, but rather by a million-x or billion-x, which is what’s needed for solving big, long-standing challenges like the Millennium Prize Problems.” Dr. Gukov likened it to a game of chess that takes 10 million moves, rather than the average 40 moves. He asked: “Can we develop AI tools that do very deep searches and think so far ahead that they can actually play the long games?”
Dr. Gukov’s experience at the lab informs the institute — and while the lab operates on a long horizon, AIM responds to trends quickly. In May, as part of the AIM Public Lecture Series, mathematician Terence Tao of UCLA, who won a Fields Medal in 2006, will give his perspective on the future roles of AI in mathematics. And in the coming year, AIM is holding a series of its flagship weeklong workshops on the “AI + x” — where ‘x’ is a certain area of mathematics. One workshop is on number theory, another algebra, and the third analysis. In terms of applications of AI tools, Dr. Gukov jokes that analysis often (though not exclusively, of course) means partial differential equations; and partial differential equations often mean the Navier-Stokes equations — currently the most hotly pursued of the Millennium Prize Problems.
A Vision for Mathematics
In recent years, machine learning scientists at Google DeepMind sought out mathematicians to discuss what AI has to offer the age-old mathematical discipline, and what tools practitioners would find especially beneficial. On two recent occasions meetings were convened at the Institute for Advanced Study in Princeton — where in the early 1950s the mathematician and physicist John von Neumann pioneered the architecture of the electronic computer.
“We need to have a clear idea of what we want from AI,” said Akshay Venkatesh, faculty member in the IAS School of Mathematics who won a Fields Medal in 2018; he oversaw the organization of the Google DeepMind meetings. But at once, he noted, “IAS and all the institutes have to take a very flexible approach. We can’t be too committed to the vision of math as it has been in the past,” said Dr. Venkatesh. “We shouldn’t think of AI solely in terms of helping us do what we’re already doing, but also look at how math will be useful in this new broader social and scientific ecosystem.”
