🔗 원문 전체 보기 → Scientific American
요약
A start-up has surprised the scientific community with a breakthrough: translating a modern proof into a programming language for verification using AI. But not everyone is celebrating
본문
March 26, 2026
5 min read
What happens when AI starts checking mathematicians’ work
A start-up has surprised the scientific community with a breakthrough: translating a modern proof into a programming language for verification using AI. But not everyone is celebrating
Olga Pankova/Getty Images
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