Posted by _alternator_ 14 hours ago
Jokes aside, this seems like a pretty weird take. What's stopping mathematicians to make this renewable?
Why not spend some time and effort (presumably using AI) to pose new open problems that are fundamental in nature?
Not that different from when trying to read an out-of-control vibe coded codebases, or an sloppy AI long email that someone may send you at 9 AM.
It's about what is non verifiable versus verifiable. The same way it produces "slop" code (which, if you give it test cases, will be 100% correct), it also produces "slop" math.
Code that serves a business function, it's ok if its slop. Math that serves directly a business function also can be slop.
But most open problems are not directly for a particular usecase. People agree widely to attack it due to the perceived possibility of encountering useful mathematical objects along the way, that will then expand the world's mathematical toolset. This is not something that you can easily express in a verifier, and is thus something that is hard to force an LLM system to do.
You are right in that understanding it retrospectively is possible, but that is not going to be as useful as the desired "elegant" objects that expand and unify mathematics. You can't represent these concepts in verifiers.
Again, if you let AI rip at something like say "beat shannon capacity" and suppose it comes up with MIMO as paulraj did, great! It's useful and you can retrospectively understand it, say by expanding shannon to multiple dimensions, as foschini and telatar did. But most math problems are not in that category.
The question then is, if AI is really good at this type of math, how much of the existing mathematical community+process is necessary? I think it will still be necessary, just maybe in fewer cases. Wherever the primary purpose of the math is in a domain and that domain has a verifiable target, we can directly optimise it to that verifiable target in-domain rather than reach for the mathematical community. How well will this work? We'll see. It's not clear if it's even possible to represent most problems this way.
Both of these are simply incorrect - serving a business function means it's valuable to that function.
I meant what you're saying. That it's OK if it's slop if it serves a business function.
Edited
But within next 10 years as costs drop significantly and even more improvements are made, yes it is very likely that almost every single existing math problem will get a serious AI cracking done on it
1. I give you a proof, you tell me if it's correct
2. I give you a theorem, you give me a correct proof
3. I give you nothing, you give me a theorem
1. is largely solved by modern LLMs and they took a big step toward 2. today with the Navier-Stokes proof. But they're definitely not there yet. It's unclear what progress is being made toward 3. for the time being that remains the realm of humans.
> Pure mathematics is dead. Long live mathematics. I think all of interesting mathematics is applied mathematics in the end. Powerful AI means that the level at which we can do applied mathematics will be so much higher, though, and many more people will be able to be "mathematicians". The importance of pure mathematics is often argued for by citing examples of important applications that used pure mathematics invented a long time before the application became apparent. We can reverse this argument: by properly developing the mathematics our applications need, we surely will obtain all of interesting pure mathematics.
Perhaps the pace of applied mathematics would rise sharply, given cheap intelligence. And this* may end up being the forefront driving progress in mathematics.
*Or maybe a split between the human domain and the practical real world. Where the human domain might end up with a variation of a "No machine contributions" policy. Sorta like the recent gcc policy.
I would like to see the Clay Institute give zero recognition for formalizations without human-readable proofs. That would incentivize OpenAI to scram or create something that's actually useful.
Mochizuki's claimed proof of the ABC conjecture is not unintelligable; it has errors. There are no proofs written by humans that are not human-readable, because in order to come out of a human mind, the proof must have fit there originally.
The four color theorem states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. It was the first theorem proved with substantial computer assistance. The theorem was proved by showing there could not be a counterexample. The authors made a list of maps where if a minimal counterexample existed, it would be one of these maps. There were 1,834 maps in that list, and each one was checked by computer. You could turn each of those cases into a picture or paragraph, but the resulting artefact would not meet my definition of human-readable.
Human-readable does not just mean in English. Humans can only hold a few objects in their short-term memory at once, not hundreds. Though some proofs require significant background knowlege, any proof written by a human will respect the fundemental limits of the human mind. There are no proofs written by humans that are not human-readable, because in order to come out of a human mind, the proof must have fit there originally.
I suspect large lean proofs generated by LLMs do not respect the fundemental limits of the human mind. If no human can read and understand them, no one can extract value in the form of reusable techniques, additional problems, progress towards related problems, and everything else Tao mentioned. If LLM proof generators can be made to write proofs with the same value as humans, that would be great! OpenAI would be a celebrated collaborator if they created as much value as a human does.