Earlier this year, Sidharth Hariharan, a graduate student in mathematics at Carnegie Mellon University, received news that sent him rushing into his adviser’s office with tears in his eyes.
He had just gotten an email from Maryna Viazovska, a professor at the École Polytechnique Fédérale de Lausanne in Switzerland and a 2022 winner of the Fields Medal, the highest honor in mathematics.
For more than two years, she and Mr. Hariharan had been leading a team of six mathematicians in an effort to break down one of Dr. Viazovska’s most celebrated proofs into distinct logical steps, a task known as formalization.
But hours earlier, Dr. Viazovska had received a tip-off from a colleague: They’d been scooped.
Or, as she soon became fond of putting it, they’d “gotten Gaussed.”
Gauss is an artificial intelligence system built by Math, Inc., a California start-up. It had taken the team’s road map for formalizing Dr. Viazovska’s result — a solution to the densest possible arrangement of eight-dimensional spheres, popularly known as the sphere-packing problem — and completed it in just five days.
While A.I. is popularly associated with stumbles in arithmetic (like ChatGPT’s meme-worthy failure to correctly count the number of R’s in the word strawberry), technology companies have poured vast resources into reasoning systems that can solve open math problems. Recent progress has turned into an arms race between A.I. competitors eager to show off machine intelligence through success in a field that is often held up as the pinnacle of human intellect.
In late May, OpenAI announced that one of its models had disproved an 80-year-old theorem that was long assumed true by mathematicians; Google DeepMind followed up with solutions to nine more. Then, just days after OpenAI published its result, a team of mathematicians used the same techniques to solve another open theorem, pointing to the potential for A.I. to become a useful tool, or even a partner, for mathematicians exploring new ideas.
“About 12 months ago, you could still say that these are curiosities or overblown and can’t be useful,” said Terence Tao, a Fields Medal-winning mathematician at the University of California, Los Angeles. “Now you can’t hold that position.”
For the thousands of graduate students in the United States currently envisioning their futures in pure math, and who learn the craft through many of the same skills and problems that A.I. is beginning to master, dire prognostications can be hard to avoid.
The OpenAI paper was a “shock,” said Carl Schildkraut, a graduate student at Stanford University who worked on the follow-up paper that extended the A.I.’s technique, adding that his fellow graduate students were “not generally optimistic” about their prospects. But a closer look at the result also made him appreciate the narrowness of the A.I.-generated math.
“When we humans work on math, we often ask ourselves questions like, ‘What ideas am I building?’ or ‘What’s actually going on here?’” he said.
In early June, a global group of mathematicians published a declaration acknowledging the benefits of A.I. while also urging caution. The mathematicians are concerned about A.I. companies’ unwillingness to reveal basic insights into their methods, failure to properly credit human authors and eagerness to conflate mathematical prowess with the idea of machine superintelligence. Math, Inc.’s tagline, for example, is: “Solve math, solve everything.”
Patrick Massot, a mathematician at the Laboratoire de Mathématiques d’Orsay in France, compared the company’s scoop to an “atomic bomb” that would make projects radioactive to young mathematicians, even if that meant missing out on valuable training or the opportunity to develop new ideas.
The scoop also distilled some of the simmering fears about what is lost in automation. It has been seen by some mathematicians as not just a breach of academic etiquette but a threat to the future of the field: If anyone can be Gaussed, why will scholars bother with certain problems in the first place?
And why will anyone pay them for it?
‘You Wonder if It Was All in Vain’
The sphere-packing problem is easy to visualize in three dimensions: Picture a stack of oranges on a farmers’ market stand. What is the tightest possible configuration? The answer, first proposed 400 years ago, is exactly the stack of fruit you pictured, but it is difficult to rule out every other iteration. A proof evaded mathematicians until 1998.
Sphere-packing in higher dimensions, such as eight, is harder to visualize, involving points in space that are defined by more than three numbers. Dr. Viazovska’s proof forged surprising connections between two different subfields of math, geometry and number theory — connections that the team hoped to explore in more detail as it formalized the proof.
When Mr. Hariharan approached her about formalizing her solution, she saw it as a learning opportunity. “Maybe the easiest way would be to formalize something smaller by myself,” Dr. Viazovska said. “But that’s not very fun.” At first, she taught him the high-level concepts while he taught her the software, called Lean, that they would use in their effort. Then, together with four other mathematicians, they developed a road map for spelling out the logic of her proof, step by step.
After about a year of work, the group opened the project to outside collaborators. It was no surprise that a number of A.I. companies, which use Lean to teach their systems about math, jumped in to help. But at the time, the best systems could produce only short snippets of useful code.
So last fall, when Math, Inc. told the group that Gauss had solved about 30 unfinished pieces of the proof, Mr. Hariharan and his colleagues were enthusiastic. They asked the company to share its full results. Instead, the start-up went dark.
Auguste Poiroux, a doctoral student at the École Polytechnique who also works for Math, Inc., said the company had turned its focus toward a new version of Gauss. The company decided to return to the sphere-packing problem only months later, using it as a test case for its upgraded system.
Shockingly, Mr. Poiroux said, the improved Gauss completed the whole proof.
Even more shocked was Dr. Viazovska, when an excited Mr. Poiroux gave her a glimpse of the “accidental” solution, as he described it. “I quickly saw that the excitement was not shared,” he said. He asked her to hold off on informing Mr. Hariharan, whom she emailed soon afterward.
Mr. Hariharan’s next call was to his parents in Dubai. “You wonder if it was all in vain,” he said. “Why did you spend two years of your life on this in the first place?”
“Trust your guru,” his parents told him. “Trust in the process.”
That night, Jesse Han, Math Inc.’s chief executive, messaged Mr. Hariharan that he was boarding a red-eye flight to Pittsburgh. They met in a Starbucks the following morning, along with Mr. Hariharan’s adviser, Jeremy Avigad, who rushed from the gym after “the fastest shower of his life,” he recalled. After Dr. Han proposed disclosing the result immediately and moving on to a related formalization project, the academics erupted, arguing that the original goal of the project, to better understand Dr. Viazovska’s proof, was far from complete.
“The outcome itself is certainly very impressive, but it’s also not what we wanted for our project,” Mr. Hariharan said.
But after speaking with fellow mathematicians and reviewing the code, they eventually agreed to a statement that acknowledged Gauss had produced a correct formalization months ahead of schedule.
They also concluded that months of work still lay ahead in making that code actually usable for people. “We still wanted to see it through,” Mr. Hariharan said.
A Rush to ‘Declare Victory’
One way to think about the situation faced by young mathematicians is as a warp-speed version of the automation affecting work in other industries, bringing both opportunities and fears of obsolescence.
“I knew personally what it was like to be a Ph.D. student and have your whole identity wrapped up in a project like this,” said Dr. Han, who formalized a major result during his degree. But for as much as he learned during that process, he would have gone so much further, he believed, with A.I. assistance. “I would have been delighted if this type of result had happened,” he said.
Dr. Han said that the scoop was unintentional — a consequence of dizzyingly fast A.I. improvements — and that he had hoped for a “celebratory” response. Instead, he felt “ambushed” by the angry messages from former colleagues, he said, which began as he touched down that early winter morning in Pittsburgh and had not let up since.
Talia Ringer, a computer scientist studying formalization at the University of Illinois, said that the grief that rippled through math departments was similar to what they recently felt as a graduate student in computer science as automation arrived in programming.
“They weren’t going to subsume the work I was doing, but they were going to claim to subsume the work I was doing,” Dr. Ringer said.
The desire by A.I. companies to “declare victory” over certain problems, said Vaughan McDonald, a fifth-year math Ph.D. at Stanford, means that even when the human work that made automation possible is acknowledged, it generally doesn’t make the headlines. That has helped kick up a certain amount of schadenfreude toward a lofty academic field.
“People are saying: ‘Oh, there shouldn’t be math jobs. Get wrecked, mathematicians,’” Mr. McDonald said. “I think that’s terrible.”
Mathematicians point to a power imbalance between shrinking math departments and well-funded start-ups, which can choose to drop sums equivalent to annual funding for multiple grad students on a single problem. A Math, Inc. employee told Mr. Hariharan’s team that the company had spent more than $100,000 on computing the sphere-packing solution.
But mathematicians bring “tremendous value” to A.I., Dr. McDonald said, in the intellectual work they do to enable automation. “They’re not necessarily being properly recognized or compensated for that,” he said.
At times, the tensions have boiled over into public rancor. When Dr. Han spoke at a meeting of Exponentiating Mathematics, a Defense Department program, he again described the sphere-packing project as “finished” and misidentified the original authors. Dr. Avigad then stood up and “let him have it,” as he later put it, in front of a stunned crowd of mathematicians. The start-up’s behavior “wasn’t good for them; it wasn’t good for math; it wasn’t good for anybody,” he recalled saying.
After Dr. Avigad finished speaking, an audible “whoa” broke the silence in the room.
Dr. Han said that those were miscommunications, but that the “fear and Ludditivism” in response had “hardened my resolve” to use A.I. to “formalize all of mathematics.”
Meantime, Mr. Hariharan’s team is using A.I. tools to streamline Math, Inc.’s code for the sphere-packing proof, collaborating with Mr. Poiroux to remove redundant statements in it (such as theorems proving why 2+2 = 4) and convert the more cryptic sections into readable language. Though at times a slog, Mr. Hariharan said the process had yielded a “nonzero amount of insight,” both into Dr. Viazovska’s math and into how A.I. works.
Mr. Hariharan is also interning this summer with Axiom Math, another A.I. math start-up — though he is not sure, he said, what role A.I. will play in his long-term plans. But when he returns to his studies this fall, his next project will not focus on formalization.
“The next theorem that I formalize, I want to have been the one to prove it,” he said.
The post They Spent Years on a Math Problem. Then They Were Scooped by A.I. appeared first on New York Times.
