‘Like space aliens landing’: Symposium weighs effect of AI on the future of mathematics

Three Fields Medalists, researchers from OpenAI and DeepMind and dozens of mathematicians and computer scientists gathered at Stanford last week to envision how artificial intelligence (AI) might transform mathematics.

Over two days of keynotes and panels held at the Stanford Institute for Economic Policy and Research, a rough consensus emerged: AI tools are already reshaping how mathematics is done, but the field’s hardest problems, such as defining the right concepts, understanding why a proof works and deciding what questions matter, remain human.

That throughline appeared in several of the symposium’s marquee talks. In a keynote on new mathematical workflows, Fields Medalist Terence Tao from the University of California, Los Angeles (UCLA) argued that the field needs to move beyond asking whether AI can generate or verify proofs. He identified what he called an “incentive gap” and introduced the concept of “proof digestion,” the process of streamlining, explaining proofs to others and connecting them to past literature and future directions. 

“The correct metric is not so much whether the proof has been generated or whether it has been verified, but whether someone can give a talk about it and take questions,” Tao said. “The measure of success is whether what we can do enables people to think and understand more clearly and effectively about mathematics.”

Michael Freedman, also a Fields Medalist, framed the challenge in structural terms. The goal, he said, is guiding AI agents to remain on a reasonable track within that space of input combinations. He later considered the possibility of AI-verified proof certificates of problems that mathematicians care about but do not understand as “one of the most fascinating and exciting events…kind of like space aliens landing.”

Sébastien Bubeck from OpenAI addressed the problem-solving abilities of GPT-series models in probability, combinatorics and optimization. 

“Maybe we can outsource thinking in the next few years, but understanding [is something] that you cannot outsource. You have to do the understanding for yourself,” he said.

Several speakers focused on the state of formal mathematics, which is the effort to render proofs in languages that machines can check. The results so far are striking but uneven.

The proofs that earned Maryna Viazovska of École Polytechnique Fédérale de Lausanne the Fields Medal in 2022 were formally verified in February 2026 through a collaboration between mathematicians and Math, Inc.’s autoformalization model, Gauss. 

“It sparked a lot of discussions in the math community and in the math formalization community,” Viazovska said.

Leo de Moura, co-founder of the Lean theorem prover, considered machine-checked mathematics in the age of AI. Even as tools improve, he emphasized the necessity of human guidance: “It’s your responsibility to check if the statements and definitions capture the intents of the paper…this is still going to be a human activity.”

Kevin Buzzard, a professor at Imperial College London, focused on auto-formalization and identified a more basic obstacle. AI is increasingly capable of handling proofs, he said, but existing formal libraries are full of holes. “There’s an awful lot of mathematics [that] is actually missing…most of us humans aren’t actually engaged in formalizing mathematics,” he said, making the prevention of AI incorrectly formalizing definitions an important issue.

Other talks showcased the current capabilities and limits of AI systems applied to mathematical research.

Thang Luong of Google DeepMind presented Aletheia, a math research agent powered by Gemini Deep Think that generates, verifies and revises solutions in natural language.

“I think we really want to make things transparent to the community. I think there’s a lot of news about AI having conquered math, but I think that’s not quite precise,” he clarified.

Adam Brown, also from Google DeepMind, formerly at Stanford Physics, outlined benchmarks to measure LLM performance. He is optimistic about models improving due to future “algorithmic progress, where we figure out how to do much more with the same amount of data and compute.”

AI in mathematics has already changed how some universities function. Andrea Bertozzi, who serves as AI lead for the math department at UCLA, presented examples of AI in applied mathematics, including an AI-driven grading tool and UCLA’s work on the Defense Advanced Research Projects Agency (DARPA) Exponentiating Mathematics program, which aims to develop an AI co-author capable of proposing and proving useful abstractions. “The train is leaving the station and the students are driving the train,” Bertozzi said.

The symposium was co-organized by assistant mathematics professor Jared Duker Lichtman, in partnership with the Futures of Mathematics Institute (FMI). It was co-sponsored by Renaissance Philanthropy, BroadRiver Asset Management, OpenAI, KeyBank and Stanford HAI. 

Other faculty attendees included Nobel Laureates, Stanford economics professors Paul Milgrom and Guido Imbens and Turing Award Winner and computer science professor Pat Hanrahan. Employees of frontier AI labs and other industry firms also participated, as did many graduate students, including a large cohort from the University of California, Berkeley.

Ravi Vakil, mathematics professor at Stanford and current President of the American Mathematical Society, urged the mathematical community to “stay involved in the discussion and aware of what’s going on,” he said. “One thing which is very upsetting is that the discussion around it in the wider world is very ill-informed and full of hyper dystopianism.”

The post ‘Like space aliens landing’: Symposium weighs effect of AI on the future of mathematics appeared first on The Stanford Daily.