Four centuries ago, Sir Walter Raleigh, the New World explorer and courtly favorite of Queen Elizabeth I, asked his assistant a stupid question. He was gearing up to lead an expedition to South America to search for a mythical city of gold and bring its riches back to London.
Cannonballs, Raleigh asked his mathematical assistant Thomas Harriot: How many per stack?
Raleigh wanted to know if there was a formula for the number of cannonballs in regularly stacked piles—an immensely practical question, since space below-decks on a British merchant ship or man-o-war was at a premium.
An important, if obscure, B-list English mathematician and astronomer, Harriot was no dummy. He knew the answer. He drew a chart of triangular numbers for Sir Walter, the exact “formula” the great man wanted. The explorer was satisfied. He could now count cannonballs at a glance.
Raleigh left to find his lost city of gold, and after two fruitless expeditions and one 10-year imprisonment, he was executed for treason by King James I in 1618. Harriot, on the other hand, obsessed about the cannonballs. Close packing. Efficient packing. Alternative stacking.
With Raleigh in jail, Harriot brought the problem to the attention of the most brilliant mathematician of his day, German astronomer Johannes Kepler. Considering the 6-sided symmetry of snowflakes falling over the Vltava River in Prague one winter night, Kepler decided pyramidal stacking was most efficient, though he never was able to prove the “Kepler Conjecture,” as it became known.
The story might have ended there, but three centuries later, German mathematician David Hilbert resurfaced it as one of 23 unsolved mathematical problems during a now famous 1900 lecture in Paris that helped to set the research agenda for the field of mathematics for the 20th century. These 23 were hard problems—desperately hard—and all the better, Hilbert said.
“A mathematical problem should be difficult,” Hilbert told his audience. But proving the Kepler Conjecture turned out to be harder than Hilbert ever imagined.
From Hobby to Obsession
Eighty years after Hilbert, mathematician Thomas Callister Hales began studying the Kepler Conjecture as a nerdy pastime. “A hobby,” he said. “Something I did in the evening after doing my real research, so to speak, during the day.”
After years of tinkering, however, he decided to make it the main focus of his research, and in 1994 he began attempting a computer-based proof. This was not his first choice. “I was hoping I would find a conventional proof,” he said.
Mathematicians and computer scientists often complain about computational “brute force” approaches to solving problems, sometimes even calling them stupid. Why? Because rather than relying on straight logical deduction, these proofs employ methods of exhaustion, having computers beat out and compare every single case until the truth is revealed. Hales’ brute-force proof, for instance, calculated and compared density calculations for every possible configuration of a stack of spheres, showing that none was more efficient than the one Kepler proposed.
“A mathematical problem should be difficult.”
A brute force approach can give you the right answer, but it might not help you understand why that answer is the right one. This is a problem for some mathematicians, for whom mechanistic understanding is everything. “You are looking for the things to take away,” said Carnegie Mellon University philosopher and mathematician Jeremy Avigad. Fundamental. Conceptual. Insights.
The Kepler Conjecture was different in this respect, Avigad said, because Hales’ massive computer-based proof did, in fact, lead to expansive new conceptual insights, including new work by Ukrainian mathematician and 2022 Fields Medal winner Maryna Viazovska and others in the last decade on the optimal packing of spheres in 8- and 24-dimensions (Try picturing that, Sir Walter!)
Initially, the Annals of Mathematics, where Hales first sent his proof for publication, set up a team of 12 expert referees to peer review it. The task was so daunting, however, that the referees dropped out one by one. Finally in 2004, after several years, the journal pulled the plug. They punted, citing chief referee László Fejes Tóth, who himself did important early work on the Kepler Conjecture in the 1950s, and claiming they were “99 percent certain” the proof was correct. But they could not continue the final mile of the marathon validation.
By then Hales had grown 100 percent frustrated. “Living with the proof every day for so long,” Hales said earlier this year, “it had all become very obvious to me.”
So he formed a project called Flyspeck to verify the proof with the help of collaborators and software-based proof checkers, drawing on commercial libraries of mathematical logic to systematically validate a mathematical proof line by line. It took a decade, but in 2014, Hales and his colleagues announced they had done it. Three years later, they published their results—so convincingly that some, including Avigad, argue the Kepler Conjecture should be renamed Hales’ theorem. Fait accompli!
Every single logical and computational step had been translated into formal mathematical logic, brute force made legible.
“For the first time I was really just able to let go,” Hales said. “I had been holding all the details of the proof in my head for all those years.”
The Forest for the Trees
As our machines get faster and smarter, the question of automation versus understanding in mathematics, of stupid versus smart, is becoming more fraught. Whereas traditional computer programs test out thousands of logical rules one by one, the sheer scale of which is often impossible to parse, today’s AI programs predict which next step might work based on past patterns. That means the AI programs can sometimes offer up elegant shortcuts, but they may just as easily struggle to explain why. Either way, humans are often left in the dark.
In May, ChatGPT autonomously solved a famously difficult math problem without human intervention, disproving the 80-year-old Planar Unit Distance Problem first posed by Hungarian mathematician Paul Erdős in 1946 after he fled the Nazis and rode out World War II in New Jersey.
The Planar Unit Distance Problem was one of Erdős’s favorites. It takes a simple two-dimensional plane and asks what is the maximum number of point pairs that can be placed exactly one unit apart. Erdős conjectured that there’s an upper limit on such pairs in traditional square grids, but proving this eluded him. He tried for years. He even sought to interest others and offered various cash bounties. No small amount of energy was spent, but it remained unsolved until earlier this year, when an OpenAI team announced ChatGPT had disproved it.
“This is the first example of a result produced autonomously by an AI that I find exciting in itself,” Daniel Litt of the University of Toronto wrote in a companion piece to the proof.
Fields Medal winner and Cambridge University mathematician William Timothy Gowers, who also contributed to the companion piece, said when he first heard of the proof on a Zoom call this spring, he was worried. He thought it meant an AI had just done something no human could do. But it turned out the AI hadn’t done that at all. Instead, it did what nobody was trying to do: ask the stupid question of assuming the conjecture is false and disproving it by finding a counter example.
That put Gowers’s mind at ease.
Erdős and everyone else had always assumed that a square grid was the most optimal planar arrangement, but ChatGPT found just that counter example—a chaotic, complex, and decidedly un-gridlike grid, which according to the OpenAI team provided, “an infinite family of examples that yield a polynomial improvement.”
As our machines get faster and smarter, the question of automation versus understanding, of stupid versus smart, is becoming more fraught.
“A counterexample,” Gowers wrote, is not the same as a positive proof. It was something a computer could come up with by trying lots of things and at some point getting lucky, he wrote. “Without needing ‘deep insight!’”
Not what Erdős was thinking, but a remarkable achievement nonetheless. “What other unseen wonders are waiting in the wings?” Thomas Bloom of the University of Manchester pondered in the same companion piece OpenAI published with the proof.
Already there have been copycats. Just a couple of months after the Erdős proof appeared, Anthropic mathematician Levent Alpöge published a solution to the 87-year-old Jacobian Conjecture in a single tweet that Claude had come up with while he was watching this summer’s World Cup Final. The conjecture says certain types of multi-variable “polynomial” functions have an exact opposite inverse function. And just this month, a team at Anthropic attacked a nearly 170-year-old problem called the Riemann Hypothesis, which is perhaps the hardest of Hilbert’s 23 challenge problems. While the chatbot Claude did not solve it, experts credit the AI with making real progress.
Smart or Stupid?
Shortly after the OpenAI Erdős proof appeared in May, a group of mathematicians published a let’s-pump-the-brakes document called the “Leiden Declaration on Artificial Intelligence and Mathematics,” which lays out the core values of mathematicians and details how AI threatens those values and the field as a whole.
“The increasing involvement of technology companies in mathematical research raises the risk that research questions may come to be prioritized because of their amenability to automated mathematics, rather than expert judgment of their deeper significance,” the declaration reads in part. “Indeed, broader understanding of the field may be permanently lost in the process of automation.”
Some worry the successes we are seeing this summer could not only cede too much ground to machines, but also fuel a territorial land race where amateurs rush into mathematics, rack up big hits, and solve thorny problems without actually being able to explain what the solutions mean.
Such a gold-rush of amateur prospecting could create a perverse disincentive. Open sharing of work in progress could disappear as professional mathematicians seek to keep things secret in order to prevent their glory from being poached at the eleventh hour.
“In this world, talking about one's work in progress—or even indicating that the models can solve a given problem—is increasingly dangerous,” Toronto mathematician Litt said in a talk called “The End of Mathematics” earlier this month at OpenAI in California. “I've recently been told by multiple colleagues that they are unwilling to discuss work in progress for this reason.”
Amateur mathematicians are already starting to try their hands at some brutal calculations, sometimes successfully. Earlier this year, a 23-year-old amateur mathematician Liam Price posted a ChatGPT solution to another Erdős problem.
“I am all for increased democracy, but if it means people not understanding what they are doing then we are in trouble,” said Geordie Williamson, the director of the Sydney Mathematical Research Institute, in an email. (He was commenting generally on the state of AI in math, not specifically Price’s proof.) “What is between our ears has always been the bottleneck.”
But Williamson is of two minds. He also believes that AI can enable new forms of mathematical understanding. Five years ago, he was part of a collaboration that showed how machine learning can help mathematicians do creative work. In the journal Nature, they described how an AI iterative workflow led to new discoveries in topology, uncovering a relationship between the unchanging “invariant” properties of knots under various transformations.
“It is surprising that a simple yet profound connection such as this has been overlooked in an area that has been extensively studied,” Williamson and his colleagues wrote in the paper, “yielding results that are both interesting and deep.”
One of the advantages of AI, evidenced by both the OpenAI Erdős proof and the Anthropic World Cup Final tweeted proof, is that it is excellent at asking stupid questions like what-if-this-famous-conjecture-we-assumed-true-is-actually-false. AI models can afford to be wrong. They have no egos. They suffer no professional embarrassments. They harbor no publish-or-perish career concerns. They have no qualms asking something stupid or trying something fruitless or barking up the wrong tree.
The Kepler Conjecture revealed a similar truth: Asking a question that seems stupid because the answer is obvious can open up new worlds of understanding. Stupid can yield its opposite and brute force can produce elegance. Perhaps we have to trust that human intelligence will ultimately find a way to decode whatever mathematical truths our machines manufacture, to translate stupid into smart. 
Enjoying Nautilus? Subscribe to our free newsletter.
Lead Image: Runawayphill / Shutterstock
