The new era in mathematics that some researchers have long hoped for may be on the horizon. Mathematicians will soon be able to use computers to quickly and rigorously verify proofs, ensuring that published proofs are correct and providing the basis for further progress. Such tools could help professionals tackle mathematical research at an accelerating pace and volume.
Computer programs that check mathematical arguments, such as proofs, have existed for decades. However, translating human-written proofs into a computer’s rigorous programming language (a prerequisite for validating proofs using these existing tools) is extremely time-consuming. This translation is known as formalization and can sometimes take months or even years.
The development of the first large-scale language model raised expectations among mathematicians. This means that someday machines may be able to do this translation automatically. However, unlike human languages, formal programming languages do not allow any variation. All terms, symbols, and references must be precisely defined.
About supporting science journalism
If you enjoyed this article, please consider supporting our award-winning journalism. Currently subscribing. By subscribing, you help ensure future generations of influential stories about the discoveries and ideas that shape the world today.
But now a startup called Math, Inc. is reporting early successes in formalizing proofs. The artificial intelligence, named Gauss, formalized two complex proofs related to the arrangement of spheres in higher dimensions by mathematician Marina Wiazovska. She won the Fields Medal for one of these certifications in 2022. However, the reaction of the mathematical community to Gauss’s formulation was modest. One reason for this is that the project did not develop as many experts had expected. As other AI and math startups seek to formalize, this case offers a hint at what mathematicians can expect in an uncertain future.
packing puzzle
In 2016, Wiazovska became a leading figure in mathematics when she solved the decades-old puzzle of how to arrange spheres in the most space-efficient way. To find the most space-efficient single solution, we must first prove that infinitely many other sphere arrangements all require more space. It took until 1998 to prove that the pyramid-shaped arrangement of oranges in a supermarket was actually the densest option in three-dimensional space.
However, in higher dimensions the arrangement of the spheres becomes significantly more complex, allowing for more arrangements and symmetries. Viazovska used a particularly sophisticated solution that exists only in 8- and 24-dimensional spaces. That is, we transferred the most space-efficient three-dimensional configuration into these higher dimensions, and then showed that the gaps opened by the transfer were large enough to accommodate one additional sphere in each space.
She first worked on the proof of eight-dimensional space, and was awarded the 2022 Fields Medal for her work. Her colleague Henry Cohn, a mathematician at the Massachusetts Institute of Technology, persuaded her to team up with several collaborators, including Stephen Miller at Rutgers University, Danilo Radchenko, now at the Institute for Advanced Study, and Abhinav Kumar, then at Stony Brook University, to develop a proof for 24-dimensional space. Within a week they were successful.
But can these proofs be formalized and verified on a computer? In 2023, Viasovska met Sidharth Hariharan, who was then studying for a master’s degree in mathematics at Imperial College London and working on a formalization process called Lean. They started exchanging ideas. “We were just two curious people who wanted to learn something, and that’s how it started,” he says.
The two decided to formalize Viazovska’s proof by converting all referenced terms, definitions, and theorems into lean code. Together with colleagues, they launched a website in June 2025 to document the formalization project. The team divided Viazovska’s original work into many smaller subtasks, documented them online, made them available for collaboration, and allowed the larger Lean community to reserve subtasks to work on.
Meanwhile, mathematician Dr. Auguste Poiroux, a student at the Swiss Federal Institute of Technology in Lausanne, helped launch the start-up company Math, Inc. in late summer 2025. “We want to automatically transfer the content of papers and books to Lean Code so that we can check it right away,” explains Poiroux.
MASS learned of Hariharan and his team’s project and contacted them. “In the fall of 2025, the folks at Math, Inc. told us that they were able to formalize a smaller part of our project and share some of the results with us,” recalls Hariharan, who is now a Ph.D. Student at Carnegie Mellon University. “Then we lost communication. We didn’t know how far along they were or if they were even still working on it.”
“We were a very small team,” Poiroux says. “We realized we couldn’t improve the system and work on Hariharan’s project at the same time, so we focused on AI.” Over the next few weeks, Math, Inc. team members further developed an agent-based language model called Gauss.
Ultimately, the software transformed mathematical work into lean code that could be automatically checked without human intervention. “We took Viazovska’s eight-dimensional proof as a test,” Poiroux says. “Then all of a sudden, the system outputs the entire formalized proof, which completely surprised us.”
the future of mathematics
Poiroux and his colleagues were excited. Hariharan’s team didn’t feel the same way. “We were very surprised, to say the least,” Hariharan said. “This was our project. We spent two years and a lot of effort, but Math, Inc. solved it.”
Hariharan and his colleagues planned to use some of the formalization as the basis for students’ undergraduate papers. “But I think it is what it is: AI is disruptive,” Hariharan says.
“In all the excitement, we didn’t really consider the consequences,” Poiroux said. “We understand that from the outside it may have appeared as if we were intentionally keeping our progress private. We will definitely be more careful going forward.”
Math, Inc. then worked on the second Viazovska proof, addressing optimal sphere packing in 24 dimensions. “In this case, we just gave Gauss the paper and nothing else,” Poiroux says. “And the system translated that into about 120,000 lines of lean code.”The code was then validated.
Math, Inc. is currently working with Hariharan and other experts to further advance the automatic formalization and cover more mathematics. “In many areas, Lean still lacks building blocks and has not been able to formalize proofs.” [in those areas] At the moment,” Poiroux said.
If large parts of mathematics can be formalized, new possibilities will open up. Math, Inc.’s systems are more than just translation machines. You can detect and correct small mistakes in your paper. This feature hints at a future in which superior AI will oversee all mathematics and perhaps even surpass humans in research.
“When our model understands mathematics holistically, it allows us to think about mathematics in completely different ways and potentially yields completely new results,” Poiroux says.
This article was first published Wissenschaft spectrum Reprinted with permission. Translated from the original German version with the help of artificial intelligence and reviewed by our editors..
