Sports Editor Abyan Memon discusses the alleged breakthroughs OpenAI has made in the maths world.
Two separate announcements by OpenAI revealed a frontier AI model had produced 722 mathematical manuscripts, including on the Navier-Stokes existence and smoothness problem, whose significance is raised by its inclusion in the Clay Mathematics Institute Millennium Prize Problems list.
Roar sat down with the President of KCL Mathematics Society, Sebastian Janssen, to understand his outlook on these developments. Informed by his perspective, we attempt to make sense of the news for a wider university audience.
Defining Terms
A mathematical proof is a logical argument that demonstrates the validity of a mathematical statement. The proof must demonstrate with certainty how the proposition follows from accepted definitions and previously established results. Aside from practical applications, mathematical proofs provide foundations for subsequent mathematical reasoning. Hence, mathematical proofs cater to the appetite for knowledge and innovation.
For example, an imaginary number is the square root of a negative number. Imaginary numbers are used by scientists and engineers to model and better understand the alternating currents in many electrical systems.
An Error-Prone Mindset
Lean is a programming language and proof assistant that mathematicians use to formalise mathematical proofs, which it then checks against a set of predefined rules, definitions and axioms.
Following OpenAI’s announcements, mathematicians from King’s College London and University of Cambridge found a discrepancy between OpenAI’s written paper on Navier-Stokes and its Lean formalisation of it.
This discrepancy means that the Lean formalisation establishes a weaker result than the one claimed in the written paper, meaning the two versions are not fully consistent with one another. This itself does not mean the original proof has failed verification.
However, it raises the question of whether, in trying to provide a solution and follow Lean’s rules under any circumstance, the AI model may have found a trade-off in sacrificing consistency across its work.
Furthermore, a sign error was discovered in another of OpenAI’s papers, leading the company to withdraw it along with two dependent papers.
While an isolated error does not necessarily undermine the use of AI in mathematics, it does raise questions about the reliability of AI-generated arguments and the extent to which they require independent verification.
The Interpretation Issue
The intellectual work required to advance mathematics, beyond simply bringing a solution into existence, is far from minimal. Platonism in the philosophy of mathematics is the position that mathematical truths exist independently of our discovery of them.
Whether that is the case or not, the existence of a solution alone does not constitute a meaningful mathematical discovery.
Interpretation, translation and identification of applications are all important in advancing mathematical knowledge. For example, the existence of imaginary numbers alone does not allow us to understand alternating currents; it is partly our conscious understanding of their properties and interactions that allows us to apply them meaningfully.
“Humans are still the ones who are mathematicians. We still have to understand what is going on to be able to ask how to solve another problem that’s linked to the solution, or just build further off this problem. Without that understanding, we don’t really have what mathematics gives us. It has to be communicated to us and interpreted by us to be valid mathematics.”
Sebastian Janssen, President of KCL Mathematics Society
Potential Win-Lose Trap
The 722 mathematical papers published by OpenAI are now down to 719 after the discovery of a sign error in one paper led to OpenAI withdrawing three papers.
The significance of these papers depends on their mathematical contribution and whether they are verified. Sebastian holds the possible verification of the Navier-Stokes paper to high regard, stating, “… that would be, I think, the biggest thing to happen in mathematics this century.”
However, if a paper is recognised to be significant, we may fail to recognise whether that significance is an isolated breakthrough or something the AI model can replicate in its mathematical research. The possibility stands that a short-term fortune may lead to a long-term misfortune of overestimating AI capabilities.
A New Role
The future of mathematics need not involve choosing between relying solely on using the human mind or on checking AI-generated work. As OpenAI’s work undergoes human verification, new approaches may arise on how to incorporate AI into the traditional mathematical research workflow.
This is a position Sebastian holds, “moving into the future, (our purpose) may not be to solve the problems, but to come up with them and be able to verify solutions (…) the middle work is now essentially being offloaded.”
The Political Aspect
Not everyone will necessarily accept a new role for mathematicians and discussions could turn into debates over how mathematics is defined. Whether the question of AI use creates such a significant rift in the mathematics community that we see intellectual divisions turn into competing philosophies is yet to be seen.
The current clash in opinions amongst mathematicians reflects the initial intrigue and scepticism one might expect.
About the author
