A dramatic episode in the mathematics community has highlighted both the promise and the disruption of artificial intelligence. At the center of the story is Sidharth Hariharan, a graduate student at Carnegie Mellon University, and a team of mathematicians led by Fields Medal winner Maryna Viazovska. For more than two years, they had been working to formally verify Viazovska’s celebrated proof of the eight-dimensional sphere-packing problem, translating it into a rigorous, machine-checkable format using the Lean proof assistant. Then an AI system called Gauss completed the same task in just five days, tells The New York Times (full article available to subscribers).
Developed by California-based Math, Inc., Gauss used the team’s publicly available roadmap and rapidly generated a complete formalization of the proof. The achievement stunned mathematicians because formalization is often viewed as a painstaking process that deepens understanding of a theorem’s underlying ideas. While the AI-generated result was technically correct, many researchers felt it bypassed the intellectual journey that made the project valuable.
The event arrives amid accelerating advances in mathematical AI. OpenAI and Google DeepMind have recently demonstrated systems capable of contributing to solutions of longstanding mathematical problems. As AI becomes increasingly capable of reasoning and proof generation, mathematicians are grappling with questions about their future role in the discipline. Some see these tools as powerful collaborators that can accelerate research, while others worry that automation could discourage young scholars from pursuing ambitious projects.
The controversy also exposed tensions between academia and AI companies. Researchers criticized the lack of transparency surrounding AI methods, concerns about attribution, and the tendency of some firms to portray mathematical achievements as evidence of approaching machine superintelligence. Critics argue that such narratives undervalue the human work required to create the knowledge and frameworks that make automation possible.
Despite the disruption, the story ends on a nuanced note. Hariharan’s team continues refining the AI-generated proof, using both human insight and AI tools to make it understandable and useful. Their experience suggests that the future of mathematics may not be a contest between humans and machines, but a complex partnership that reshapes how mathematical knowledge is created, explored, and shared.