Quite a fair and accessible article on the whole. These bits stood out
A senior colleague of mine found one of his favourite problems among those solved and attempted to read the accompanying paper. He told me it was so unintelligible that, had he received it as an editor at a mathematics journal, “it would have gone straight into the bin”.
Reactions to the OpenAI drop have been mixed, ranging from “obviously the most significant moment in mathematical history” to “mathematicians aren’t so thrilled at this giant pile of turd dumped at our doorstep”.
Says to me that, even if some of these proofs are found to hold water, human understanding of mathematical proofs is absolutely essential. To explain it to other people, understand the implications for future results, to know what it really means, is now even more important.
To explain it to other people, understand the implications for future results, to know what it really means, is now even more important.
I think the thing a lot of the non-mathematical community doesn’t understand is why this is important. I suspect a lot of people imagine a future where AI can build one result on another into a tower of useful math, and the math produced being incomprehensible is a human limitation, not a fundamental problem.
What they don’t understand is that the LLMs aren’t really much better at understanding these messy sorts of proofs than we are. They’re able to move forward one step because the foundation they’re building on is solid, but what they’re building isn’t that useful even to future LLM work.
I’m a software engineer by trade, and I work with LLMs daily. Give them a solid codebase, and a plan, and they will implement features at an impressive rate. But the architecture will be haphazard, and if you just let them keep going without a well understood structure to the code, eventually they’ll hit the point where they’re introducing more bugs than fixes, and the whole process falls apart.
I think we’re going to see an analogous situation with mathematics. LLMs are great at building the next floor of the tower, but to make real progress we have to build those into a solid foundation before we can build higher.
The codeification of mathematics might make AI-assisted mathematics even better in the future. Proof assistants like Lean or Coq are essentially functional programming languages that allow you to rigorously prove statements via code.
Where a regular AI-generated proof might need a human to verify, an AI-generated proof in Lean would only need a mathematician to verify that the statement to be proved is the correct code-ification of the mathematical problem. This would allow for the “next floor” to be built even quicker, because no human verification is needed anymore. It’s just a question of “Does it compile?”, because the logic is baked into the programming language itself.
But for this to work, many, many theorems and lemmas need to be formalized in Lean. Many mathematicians and computer scientists already volunteer, but the sheer number of theorems is too much. Maybe generative AI will be able to help with that. Maybe it already does, but I’m not in the loop enough.
Yeah, I think it’s going to improve a lot. Though, I actually think the Lean proofs only provide so much benefit.
The LLMs operate in a lot of ways remarkably similarly to how we do. It’s just as important for them to be able to “chunk” ideas into coherent blocks as it is for us. Lean code still allows writing what I would describe as spaghetti-code proofs, and doesn’t require building your theory with the sort of coherent building blocks that lets you build high.
I think the real improvements will come as we learn to use LLMs to write more structured and elegant proofs, and at least for the near term, I think that that favors the human language approach over the Lean-first approach.
I’m definitely not totally confident of this, and wouldn’t be shocked to be wrong though.
