Are we just collecting lots of AI-proof-shaped stamps?

Thanks to AI, famous mathematical conjectures are seemingly getting overturned faster than red cards at a World Cup. But there’s something that’s been bugging me about all these new AI proofs.

Take the recent mathematical proof – or rather disproof – of the Jacobian conjecture by Fable, announced on X:

It’s a remarkable finding, which has solved a puzzle that has frustrated mathematicians for decades. And in many ways, it’s the best in mathematical elegance and accessibility: a proof that can fit in a tweet and could be verified by any mathematics undergrad, or even a bright high school student.

Like many others, the first thing I did when I saw it was put the (x, y, z) co-ordinates into the equation to check it held up. But, like others, I then wondered how Fable had managed to spot such an elusive equation. And that’s where I hit a wall. It’s unlikely Fable found it by brute force alone – after all, humans have been trying for decades – but it’s still not clear exactly what it did behind the scenes.

Back in 1985, mathematician Jean-Pierre Serre expressed caution about the rise of proofs that ran to hundreds of pages, which hardly any humans could be expected to understand or check:

‘What should one do with such theorems, if one has to use them? Accept them on faith? Probably. But it is not a very comfortable situation.’

Serre was talking of proofs that were hard to verify. In contrast, AI proofs like the above are fairly easy to check. But the path the AI took to get there is often beyond reach. We have the what, but we frequently lack the why.

To paraphrase Serre: what should we do with such proofs?

In a recent talk, mathematician Terence Tao points out that there is more to mathematical research than just showing things are true:

For a proof to actually contribute to the broader field, it is not enough for it to be correct and easy to read. It also needs to be accepted and valued by the community. Other mathematicians need to digest the result and incorporate it into their own work.

Authors can assist in the digestion process by describing their own insights and stories from when they were working on the problem. However, current AI tools are quite opaque about their problem-solving process. This is particularly true for proprietary models whose inner workings remain a corporate secret.

Tao concluded with a suggestion that the ultimate goal of mathematical research is to have verified solutions that are ‘digested, accepted, and incorporated into the definitive theory of the field’.

Nobel laureate Ernest Rutherford supposedly once said that ‘all science is either physics or stamp collecting’. In his view, the distinction came about because physics aimed to derive fundamental laws and mathematical principles, whereas other fields merely observe and categorise.

Many fields would rightly take issue with this generalisation, but the quote still came to my mind this week. Because I realised that I now knew a famous conjecture was false, but I didn’t have much beyond that.

Are we just collecting lots of little AI-proof-shaped stamps? In the long run, I expect it won’t be that simple. AI has the potential to show us a lot of things we’ve so far missed. But ‘show’ is the operative word here. It won’t be enough to tell us lots of things are true (or false); we’ll need the tales and theories that others can build on.

If you’re interested in reading more about mathematical proof and AI, you might like my latest book Proof: The Uncertain Science of Certainty.