A new era in mathematics may be on the horizon—one that some researchers have long desired. Mathematicians could soon use computers to verify proofs quickly and rigorously, ensuring published proofs are correct and providing a foundation for further advances. Such a tool could help experts grapple with the accelerating pace and volume of mathematical research.
Computer programs that check mathematical arguments, such as proofs, have existed for decades. But translating a human-written proof into the strict programming language of a computer—a prerequisite for verifying it using these existing tools—is extremely time-consuming. This translation, known as formalization, can sometimes take months or even years.
With the development of the first large language models, mathematicians’ hopes rose: perhaps machines could one day do this translation automatically. Unlike human languages, however, formal programming languages allow no variation whatsoever. Every term, symbol and reference must be precisely defined.
On supporting science journalism
If you’re enjoying this article, consider supporting our award-winning journalism by subscribing. By purchasing a subscription you are helping to ensure the future of impactful stories about the discoveries and ideas shaping our world today.
But now a start-up called Math, Inc., is reporting initial success in formalizing proofs. Its artificial intelligence, named Gauss, has formalized two complex proofs related to arranging spheres in higher dimensions by mathematician Maryna Viazovska. She received the Fields Medal for one of these proofs in 2022. The mathematics community’s response to Gauss’s formalization has been muted, however, partly because the project did not unfold as many experts had hoped. As other AI-and-math start-ups explore formalization, this case offers hints as to what mathematicians might expect in an uncertain future.
A Packing Puzzle
In 2016 Viazovska became a central figure in mathematics by solving a decades-old puzzle: How can spheres be arranged in the most space-efficient way? To find the single most space-efficient solution, you must first prove that all of the other infinitely many arrangements of spheres require more space. It took until 1998 to prove that a pyramid-shaped arrangement—like a stack of oranges at the supermarket—is indeed the densest option in three-dimensional space.
But arranging spheres becomes significantly more complex in higher dimensions, which allow for more arrangements and symmetries. Viazovska used a particularly elegant solution that exists only for eight- and 24-dimensional space: transferring the most space-efficient three-dimensional arrangement to these higher dimensions and then showing that the gaps opened up by the transfer are exactly large enough to accommodate a single additional sphere in each one.
She first tackled the eight-dimensional space proof, for which she received a 2022 Fields Medal. Her colleague Henry Cohn, a mathematician at the Massachusetts Institute of Technology, persuaded her to team up with several collaborators—including Stephen Miller of Rutgers University, Danylo Radchenko, now at the Institute of Advanced Scientific Studies, and Abhinav Kumar, then at Stony Brook University—to develop a proof for 24-dimensional space. Within a week they had succeeded.
But could these proofs be formalized and verified by a computer? In 2023 Viazovska met Sidharth Hariharan, who was then studying for his master’s degree in mathematics at Imperial College London and working with a formalization process called Lean. They began exchanging ideas. “We were simply two curious people who wanted to learn something—that’s how it started,” he says.
The two decided to formalize Viazovska’s proofs by translating every term, definition and theorem referenced into Lean code. They joined with colleagues to launch a website documenting their formalization project in June 2025. The team broke down Viazovska’s original work into many small subtasks, documented them online, and made them available for collaboration so that the larger Lean community could reserve a subtask to work on.
Meanwhile mathematician Auguste Poiroux, a Ph.D. student at the Swiss Federal Institute of Technology in Lausanne, helped launch the start-up Math, Inc., in the late summer of 2025. “We want to make it possible to automatically transfer the content of a paper or book into Lean code and check it immediately,” Poiroux explains.
Math, Inc., became aware of the project by Hariharan and his colleagues and made contact. “In the fall of 2025, the people at Math, Inc., told us they had been able to formalize smaller parts of our project and shared some of their results with us,” recalls Hariharan, now a Ph.D. student at Carnegie Mellon University. “Then the communication stopped. We didn’t know how far along they were—or even if they were still working on it.”
“We were a very small team,” Poiroux says. “We realized we couldn’t simultaneously improve our system and work on Hariharan’s project. So we focused on the AI.” In the following weeks, the Math, Inc., team members further developed their agent-based language model, called Gauss.
Eventually, the software seemed capable of translating a mathematical work into Lean code and automatically checking it without human intervention. “We took Viazovska’s eight-dimensional proof as a test,” Poiroux says. “And suddenly, the system output the entire formalized proof. That totally surprised us.”
The Future of Mathematics
Poiroux and his colleagues were thrilled. Hariharan’s team did not feel the same. “We were, to say the least, very surprised,” Hariharan says. “It was our project; we put a lot of work into it over two years—and then Math, Inc., solves it.”
Hariharan and his colleagues had planned for part of the formalization to be the basis of a student’s undergraduate thesis. “But that’s how it is, I guess. AI is disruptive,” Hariharan says.
“In the excitement, we didn’t fully consider the consequences,” Poiroux says. “I understand that, from the outside, it might have looked as if we had deliberately kept our progress secret. We will definitely be more careful in the future.”
Math, Inc., then tackled the second Viazovska proof, which addressed optimal sphere packing in 24 dimensions. “In this case, we only gave Gauss the paper, nothing else,” Poiroux says. “And the system transformed it into around 120,000 lines of Lean code.” The code has since been verified.
Math, Inc., is now collaborating with Hariharan and other experts to further advance autoformalization and cover more of mathematics. “For many areas, the building blocks are still missing in Lean—we couldn’t formalize proofs [in those areas] at present,” Poiroux says.
When large parts of mathematics are able to be formalized, new possibilities will open up. Math, Inc.’s systems are more than mere translation machines: they can detect and correct minor errors in papers, and this capability hints at a potential future in which superior AIs oversee all of mathematics—and maybe even surpass humans in research.
“When our models understand mathematics in its entirety, they can think about it in a completely different way,” Poiroux says, “and potentially deliver entirely new results.”
This article originally appeared in Spektrum der Wissenschaft and was reproduced with permission. It was translated from the original German version with the assistance of artificial intelligence and reviewed by our editors.