AI Claimed to Verify a Proof; A Ph.D. Student Says Work Remains
Heidi Opdyke
- Associate Dean of Marketing and Communications, MCS
- Email opdyke@andrew.cmu.edu
- Phone 412-268-9982
Sidharth Hariharan approached Fields Medalist Maryna Viazovska after a lecture at the Ecole Polytechnique Fédérale de Lausanne (EPFL) to learn from one of the world’s leading mathematicians.
Hariharan’s curiosity evolved into an international research effort to formally verify Viazovska’s proof and placed him at the center of a growing debate: How will mathematics change when AI can produce and verify proofs?
“There’s so much discussion now on how we can use AI for good, should we be using AI, what are the ethics and what are the considerations,” said Harihan, a Ph.D. student in Carnegie Mellon University’s Department of Mathematical Sciences. “I’m incredibly happy that’s been the outcome.”
Taking on a landmark proof
In 2022, Viazovska earned the Fields Medal, one of the highest honors in mathematics, for solving a major problem known as sphere packing. The challenge is to determine the most efficient way to arrange spheres in different dimensions. Viazovska proved the optimal configuration in 8- and 24-dimensional spaces. Understanding the mathematics behind arranging spheres could have practical applications in fields such as cryptography, space exploration and long-distance communications.
With Viazovska’s support, Hariharan assembled a team of researchers from across the world including professors he met at Imperial College London, where he earned his master’s degree in mathematics. Over the next year, the team developed computer code to start independently verifying Viazovska’s proofs. Hariharan and teammates also used AI tools, such as Claude, to refine their code and explore new ideas.
The team published their initial code on GitHub, a website where developers and researchers openly share code. By making the work public, they hoped to invite feedback and gain further input and support from other mathematicians.
An AI startup changes the game
Soon after Hariharan and his colleagues publicly shared their work, Math Inc., a company focused on using artificial intelligence to address mathematical problems, reached out. Initially, the company offered to collaborate, applying AI tools to the formalization process. Hariharan was enthusiastic, saying he believes in the power of AI to transform mathematics.
“I see a lot of potential,” Hariharan said. “I can see a world where AI models are trained to better understand mathematical exploration.”
Math, Inc. started out as an enthusiastic contributor, sharing how their AI formalization model, Gauss, had determined some intermediate steps in the proof verification process. Hariharan and his collaborators implemented the Math, Inc. code into their own repository, but the company stopped regular communication not long after.
In January 2026, Math, Inc. contacted Hariharan with news. The latest version of Gauss had verified Viazovska’s proof within two weeks, a process that would have taken Hariharan and his contributors months. After Math Inc. shared their results with news outlets, Hariharan’s project gained international attention.
Becoming a voice in mathematics’ AI debate
After Math, Inc.’s publication, Hariharan became a leading voice on the use of AI in mathematics. He said he is hopeful about how AI can be used in the discipline.
“I’ve talked to a lot of people, and I really see this sort of potential,” Hariharan said. “You can use AI and formalization more generally for learning. I’m a big advocate for that, because that’s what I did.”
One of Hariharan’s supporters is his advisor at Carnegie Mellon. Jeremy Avigad, professor of philosophy and mathematical sciences at Carnegie Mellon and director of the National Science Foundation Institute for Computer-Aided Reasoning in Mathematics (ICARM), is a leader in formalization.
“Sid has become an international spokesperson on formalization and the role of AI, which is a heavy burden for such an early-career researcher,” Avigad said. “The entire mathematics community is grappling with the effects of AI on the profession. Sid has helped us all understand the challenges and think about how to address them.”
As interest grew, Hariharan spoke to researchers in the U.S. and internationally to share the progress on the work and AI’s growing role in mathematics. One of the highlights was a presentation at the International Congress on Mathematical Software, a satellite conference of the International Congress of Mathematicians, where he shared the team’s results and outlined a vision for the project’s next phases.
Other researchers gained insights from Hariharan’s experiences. Anthropologist Rodrigo Ochigame, assistant professor at Leiden University, and mathematician Jim Portegies, assistant professor at the Eindhoven University of Technology, helped cowrite the Leiden Declaration on Artificial Intelligence in Mathematics. The declaration advocates for action to address challenges that could arise from using AI in mathematics research. Though the declaration accepts AI as a tool, the writers said that humans should be at the center of mathematics research. Over 3,000 mathematicians have signed it. Ochigame and Portegies reached out to Hariharan after Math Inc.’s publication.
“They told me they were thinking about me while writing this declaration, and similarly, I was thinking about the declaration a lot when figuring out how to respond to everything,” Hariharan said.
Hariharan gained a voice in another startup that is creating AI tools for mathematicians. Axiom Math invited Hariharan to be an intern over summer 2026. As part of his time with Axiom Math, he helped the company improve its own and navigate how best to work with mathematicians.
“These models are getting better, and to actually see what some of the difficulties are in improving them has been insightful for me,” Hariharan said.
Hariharan has spoken with researchers from other companies, including Meta and mathematics startup Harmonic, offering opinions on their tools and insights into how they can best assist researchers. He said that he plans to stay involved with the AI in mathematics community.
“I want to stay in academia, but I want to keep in touch with the AI and math space,” Hariharan said. “I want to be in a place where I can benefit from this technology without getting caught up in the hype.”
What comes next
Though Math, Inc. verified Viazovska’s proof is correct, Hariharan said the formalization process requires more work.
“What happened was a milestone, and a very interesting milestone at that, but it isn’t the end of the project,” Hariharan said. “The scope of our project is a great deal broader than what Math, Inc. achieved.”
Hariharan and his collaborators found the Math, Inc. code was difficult to read, so they are formalizing the rest of the proof by improving and adding to the code they had written before the startup got involved. They are following the principle of canonization, where mathematicians verify theorems and proofs in a way that allows others to reuse and replicate their findings.
The team uses AI tools like Claude for editing or for creating smaller pieces of code, but Hariharan believes that human mathematicians create formalization breakthroughs.
“I think AI is capable of formalizing mathematics but not canonizing it,” Hariharan said. “Its effectiveness depends on your use case. Proven a new result and want to check if it's correct? Fire up your LLMs, they'll translate your proof into Lean. But can they build reusable formal infrastructure? Not yet.”
Hariharan said he is still searching for collaborators. He said he hopes that he can finish this project and move forward, creating his own proofs and finding new ways to use computational tools in mathematics.
“We are grateful for the support of the wider math community, and we continue to welcome contributors,” Hariharan said. “We’re not finished yet, but we’re getting closer.”
