AI in Math – More problems, more problems

Last time I wrote about AI in mathematics, I discussed autoformalisation – taking a human proof and translating it into a formal proof which can be verified by a computer. Although I didn’t touch on it too much, this was far from controversial. Some described a proof in Lean concerning optimal packing of spheres in ℝ⁸ completed by Math Inc’s autoformalisation agent Gauss as ‘drive-by proving’. A team of mathematicians set out to formalise a problem to understand it further, and a large AI company, building on their work, finishes the formalisation. In doing so, it is unclear what has been contributed to human understanding during the process.

Since writing that article, it appears that AI companies have not learnt from the backlash. Originally announced by a coffee shop in Islington, Anthropic recently announced a LEAN-formalisation of Fermat’s last theorem. This was the exact subject of a research project run by my former professor, Kevin Buzzard. I am glad to know that this research project will still continue (being able to contribute a lot more to the mathematical community than a headline from Anthropic). However I recommend reading Professor Buzzard’s discussion of the topic, which is both heartfelt and hopeful.

I touched in my previous article on autoformalisation on the next horizon for AI in mathematics. Rather than merely formalising problems, AI may be used to actually assist, or even independently solve problems. It appears that that horizon has appeared much more quickly than even the optimistic AI-bros could have hoped.

OpenAI releases 700+ mathematical preprints overnight

Recently, OpenAI has released more than 700 mathematical preprints solving advanced mathematical problems. These preprints are all LEAN-verified (i.e. formalised), so the math community is certain that these are not ‘AI-slop’, although there is still a question of the value of these papers. These papers were all written using an unreleased AI agent.

The problems with this approach are many:

Firstly, dumping papers in this manner could wipe out the research of people (particularly early career researchers and students) working in this area. While it is understandable that OpenAI want to show off the capabilities of their models, this is not the first scandal that has beset AI companies working in mathematics. In my opinion, the backlash to the recent Navier-Stokes proof should have been enough for OpenAI to reconsider their approach to mathematics research. Any goodwill remaining in the math community has presumably been harmed by this scattershot approach.

Secondly, it is unclear as of yet how useful these papers will be. As demonstrated in the Gauss circle-packing debacle, a LEAN-verified result does not contribute greatly to human understanding. There is of course a natural-language paper which has been produced alongside the LEAN result, but it is unclear as of yet the quality of these papers, and whether they actually contribute significantly.

Lastly, following the release of the OpenAI trove, a recent preprint has been causing waves which calls into question proofs in LEAN as a whole. Importantly, I want everyone to understand that LEAN (assuming there are no errors in the compiler) verifies a LEAN-written statement as true. No one is calling into question this process. What is being questioned, is how natural-language statements (the basis of human readable math) are translated into LEAN statements. Is anything lost in the translation process that means the verified proof does not match the natural language problem? Because this may be inconsistent, a human has to check the top level statement which has been proved (to be clear this is not an issue for the OpenAI Navier-Stokes proof).

What is more interesting in this paper is that an AI agent can take a wildly different approach to proving a theorem than requested by the user. Therefore, if a human-made proof is formalised using an AI agent, it might not be clear to say the corresponding human-made proof is correct. Put differently, the LEAN proof proves a top-level statement, and not any intermediate steps of the proof.

As an example, I might say “statement X is true and I have proved it by integrating some variable, please formalise this in LEAN”. The AI agent may then return a proof of statement X but the proof may use induction rather than integration. In this case, we can say that statement X is true, but we can’t be sure my working is true. This is of course a massive problem when the proof of Fermat’s last theorem for example produced 13 million lines of code. The math community is put in the unenviable position of knowing that the theorem is correct, but not now knowing if all of the statements used to get there are correct.

I am sure that there is more to be said on the topic of AI assisted math. The recent statements of major mathematicians make it clear that AI in math is not going anywhere, but also call for issues with AI-assisted or agentic research to be addressed urgently.

In many ways, math is a microcosm for the wider world, and the problems faced here will no doubt soon be faced in other industries. I therefore leave you with the words of 25 Fields medalists on the subject:

“The issues the mathematical community faces now are similar to issues that other scientific and creative professions are facing, and indicate issues that all of humanity might face: how to make sure that, as AI changes the way work is done, we do not lose sight of what that work was meant to achieve in the first place."