Pierre de Fermat was a 17th-century mathematician.
LeBrecht Music & Art, YAY Media AS/Alamy
In a bustling central London hotel lobby, tourists gear up for a day of sightseeing under sweltering heat. Meanwhile, hotel staff reset the dining area post-breakfast as scholars convene in a windowless conference room, questioning humanity’s role in mathematics as Artificial Intelligence (AI) achieves unprecedented theorem-proving capabilities.
This gathering is infused with a mix of confusion over recent advancements in computer intelligence, excitement about untapped possibilities, and a tinge of anxiety for the future. Scholars are eager to delve into Fermat’s Last Theorem, utilizing state-of-the-art AI models for the task.
Fermat’s Last Theorem, a puzzle for mathematicians over centuries, was conclusively proved by Andrew Wiles in 1993. The theorem declares that there are no integer solutions for a, b, and c in the equation aⁿ + bⁿ = cⁿ for any integer n greater than 2. While simple to articulate, its proof is notoriously complex.
Currently, Kevin Buzzard, a professor at Imperial College London, leads an ambitious five-year initiative to convert Wiles’ extensive proof into a machine-readable format using a coding language called “Lean.” This conversion aims to verify correctness and serve as a foundation for ongoing research.
Formalizing mathematical theorems transforms them from traditional pen-and-paper contexts, organizing these ideas for computational analysis and systematically examining their logic to unveil any inaccuracies. Mathlib, a central repository, houses over two million lines of formalized mathematics.
This workshop unites mathematicians, computer scientists, and AI specialists eager to contribute to Buzzard’s project, aiming to incorporate Fermat’s Last Theorem into Mathlib by leveraging advanced AI tools for efficiency.
The atmosphere is vibrant as participants crowd around laptops featuring diverse interfaces for leading AI models. While an alternative quiet room awaits for those seeking solitude, it remains unoccupied.
Tasks are dissected and tackled collaboratively, with human prompts guiding the AI. Remarkably, the project’s codebase surged from 20,000 to 40,000 lines on the first day alone, showcasing the rapid integration of AI capabilities.
The Fermat formalization project, initiated in 2024, began with slow progress as Buzzard meticulously coded. However, since December, the pace has accelerated significantly with the advancements in AI’s mathematical prowess. A noteworthy incident in May saw a machine solve an 80-year-old problem, redefining expectations in the field. Consequently, Buzzard felt compelled to reassess the project’s aspirations.
“I was always secretly confident we would succeed. But with AI’s rapid advancements, my instinct is prompting me to reconsider our approach,” Buzzard reflects.
Wiles’ intricate proof not only spans around 100 pages but is also grounded in approximately 2,000 pages of earlier mathematics from the mid-20th century. Initially, Buzzard aimed to formalize only Wiles’ pivotal paper, trusting the underlying mathematics as accurate.
However, Buzzard now envisions a comprehensive approach, tackling the entire theorem’s structure. Despite his confidence in achieving the project’s objectives within five years, the evolving landscape of AI and workshop outcomes will dictate future progress.
Among the researchers is Han Lu Su, who self-taught Lean through ChatGPT just six months prior. Now, she is deeply involved in this cutting-edge domain.
Many of her colleagues still lean on traditional methods, making the AI innovations showcased here a glimpse into the discipline’s potential future. “The industrialization of intellectual processes is unfolding,” Su asserts. “AI tools perform so efficiently that it prompts us to consider our role further,” she adds, referencing how the AI model Claude simplifies complex tasks.
The event features various tools, from open-source options to the latest elite models from American startups. Although participants refrain from disclosing specific token expenditures—costs associated with AI access—most agree they likely exceed thousands of pounds daily. “I’m burning tokens like there’s no tomorrow,” Su admits.
To tackle intricate mathematical challenges, groups must prioritize quality alongside quantity. On the workshop’s first day, Su and a colleague attempted to formalize the same mathematical concept; she crafted an 800-word solution while her colleague achieved a 400-word version. Both solutions could equally substantiate the theorem, but the brevity and efficiency of concise proofs enhance AI’s capability for future processing and human comprehension.
However, AI-generated code can often become cumbersome and slow, Buzzard warns. Utilizing non-standard functions within Lean risks compilability issues with future updates.
Due to potential inefficiencies, the stewards of the Mathlib library remain cautious about integrating extensive AI-generated Lean code, even if it successfully proves theorems. Currently, the library’s code is meticulously crafted by mathematicians to ensure efficiency, clarity, and readability. The workshop’s output may deviate from those standards.
“We’re layering additional complexity on top—let’s call it ‘slop’—and now we face the question: can we build upon this foundation effectively?” Buzzard queries.
These advancements also spark philosophical and existential inquiries for mathematicians. While research tools evolve, the very nature of their work is shifting. In a more optimistic scenario, AI could redefine and expand the realms of mathematics, potentially surpassing human intuitions.
“We engage in this work because we cherish it and recognize its significance. Yet, with AI’s emergence, we must ask ourselves, what does this signify for us? If a machine proves a theorem beyond human comprehension, what have we truly achieved?” Buzzard ponders.
Such inquiries grow increasingly pressing as the mathematics becomes highly abstract, encompassing concepts like 38-dimensional spheres. “Does this abstract realm even exist if humans aren’t there to acknowledge it?” Buzzard muses.
Topics:
Source: www.newscientist.com
