The AI proofs are a side-product of benchmarking current and in-development models on especially hard problems. They're clearly cost effective for frontier AI firms, and free for the taking as far as human mathematicians are concerned. The real issue with them is that they look like bizarre nonsense as written, so they need mathematicians familiar with those specific areas of math to "decode" and digest them.
It's not obvious that this is a given. "Cost-effective" implies a comparison between cost and output. OAI spent millions to race human researchers on Navier Stokes, and that doesn't even account for the training cost. And how does one value the output? OAI is for some reason still hiring armies of humans instead of automating roles like "AI support engineer" or "Product Designer" (https://openai.com/careers/search/).
Calling the proofs a "side-product" is also rather dubious when OAI employs a team of mathematicians specifically to train its theorem proving capabilities.
Mathematicians are primarily understanding-oriented.
Leveraging AI to tackle new frontiers without true understanding converts mathematicians to engineers.
But in this case, isn't use of llm / generative ai to tackle new frontiers just another instrument to be used to understand the universe?
An engineer picks up a telescope, and uses it to build new applied technologies, a scientist uses the data it produces to answer new mysteries.
No one's saying, "we have to be careful with the information the telescope produces".
It seems to me that all of these hundreds of proofs we've seen recently are glorified academic exercises, whose purpose is curiosity for its own sake without any practical application, or we'd already hear about at least one of them being implemented to some gain somewhere. It's all woefully unimpressive. It's not like anything stops mathematicians from trying to find more elegant solutions to their machine solved pet problems, since that's what they were going to try and do anyway despite it being completely pointless in practice.
Nope.
(https://mathoverflow.net/questions/43690/whats-a-mathematici...)
btw people has massively improved the lower bound (from 1-2^-182 to about 1-2^-10) in the past couple of days: https://github.com/CrocSwap/integer-mult-bounds
> sub-O(nlogn) proof disproves that
How? Re-iterating, creating and understanding new proof techniques is the point of most of modern mathematics. Your statement is that proving a particular result is evidence of AI creating and understanding new proof techniques. I don't see how that follows, and I'm inclined to believe Tao is right for now.
And yes, results matter too, but if we stop at our current body of techniques and strip-mine results then we'll kneecap our future selves.
We should name the explicit mechanism that was employed - telling the model to "believe in yourself".
There is something quite humorous but also poetic about how the manipulation of this term worked. Doubtless in the model's weights lies the echoes of generations upon generations of humans telling each other to believe in themselves.
In pursuing the "new frontier" as you rightly put it, mathematicians would do well to remember the same. It's ok, don't be afraid of the future. Believe in yourself.
I don't really know the answer to that. I am happy when my own work is replaced by automated tools ("script yourself out of a job every six months!").
It's like getting scooped. If you just founded a startup based on tech XYZ, should you be happy when someone releases an open source XYZ? Should a news reporter be happy when another network breaks the story they were working on? On the one hand, society got the value of the thing you wanted to do. On the other hand, now you need to find something else to do, which might be really annoying.
This is exactly what happened with that counterproof chat he posted a month or so ago - AI gave us an answer, he used AI to back into insights about the answer.
You don't address seismic shifts with a sweeping new approach, they are too multifaceted and present complexities and conflicts. He can say AI should help human understanding, which is a good end goal, but that doesn't mean AI dumping solutions isn't progress. That doesn't mean if AI builds 5,000 proofs in Lean and no human ever looks at them that they aren't useful, especially if other LLMs can access and build on those results.
This is exactly, exactly the same as when computers took over. "Oh, we don't need accountants any more" - not true, we just need acountants to deal more with human concerns than adding columns of numbers. That is called human progress, not a threat to humanity.