The biggest problem is LLM tends to produce over engineered, very complicated proofs that are an eyesore even for relatively simple problems. Give it a beautiful Olympiad geometry problem and LLM will tear it apart into ugly algebraic calculations, turns all lines and circles into equations and calculate their intersection points that spans multiple pages because it is a guaranteed way to solve it. Correct, but hardly any use to the user.
I’m not deep in to math but the op tweets make sense to me. In that it’s not just the final proof that mattered, but the mind and understanding of the person who arrived at the answer. An LLM dumping the answer can’t elaborate on it, can’t tell the story of how they got there, etc. But it also deprives someone else of that achievement and learning.
You can see it in the way we structure college courses: engineering curricula often cover in one semester what mathematicians study over one or two years.
This is because have fundamentally different goals: being able to use results in calculation versus having a deeper understanding of the subject matter.
I don’t know if it is valid. It is unverifiable. I still found some basic algebraic mistakes in top models as late as 3-4 months ago, not sure about it now. But that’s not what I want anyway, so I often put “Do not brute force” in my prompts.
So instead of us "knowing it is valid", we don't. We need to put in extra effort, because someone felt like doing only half the work and dumping it on the community to fix.
We don't know the current system can work well enough at this scale, because that's un-knowable. We know it can find some of the problems. We don't know it can find all of them.
We do know it takes more effort - that's knowable. Increased data takes increased processing.
Whether the community has the required effort available, seems unlikely, considering the expertise required to be able to assess these things hasn't changed. Only the ability to generate them has increased.
You don't have to go through it. You can ignore it if you wish. There is no obligation on you to check it.
I feel your concern stems from the risk that there is additional noise everyone needs to cut through.
In reality this isn't any tom, dick or Harry giving you their vibe code output.
They have spent millions of dollars on this output, so there is a filter. The biggest filter of them all, funding.
Furthermore, LLM's have given us another gift semantic search, we can easily check your work against theirs, this is valuable insight so instead of researchers wasting decades and fortunes pursuing an avenue that shows no value (this includes methods), they can purse new avenues they know what to avoid, in the same breath they know what to work towards.
That's capitalism. The luddites weren't complaining because there was a new technology making their jobs less interesting or due to the "loss of a craft", they were doing so because it was taking over an industry and taking their jobs.
How something is proven is often more important than what is being proven. There are underlying systems and patterns that, when understood properly, improve our model of mathematical (or physical) reality.
With convoluted and inelegant proofs, AI may fail to uncover those systems and patterns. As a most concrete example, it may fail to recognize some problems as isomorphic to other problems. Brute force solutions are a depth-first search.
To improve human mathematical understanding, AI is probably best used as a “copilot” (lol) rather than a black box oracle, like these AI companies appear to be doing.
If you're after new methods. Then new methods is the goal, the answer to the question is not the goal then. The animated response indicates the answer wasn't just a byproduct.
There is still something to glean from the answer. You have a further constraint. Otherwise whatever "new method" proposed may as well be hallucination, potentially taking you in the wrong direction away from the answer.
This line of thought is not unique, stonemasons made obsolete by uniform brickword suddenly were "worried about the art and preserving traditions".
You’ve provided a bunch of cliches but not really anything substantial against my primary point: that in math the “how” is often much more important than the “what”, but in AI-generated proofs the “what” is the goal and the “how” is sent whizzing by on the terminal while you press enter.
Tao points out that without the mechanism for disseminating the techniques used to construct the proof, the proof by itself is fairly useless. It’s not like the existence of the proof directly increases GDP or human health or flourishing in any direct way.
