Posted by smilelamp 15 hours ago
Of course if you solve any existing problem, new ones appear. That's not the point. The point is that AI will be able to advance on any problem better than any human.
There's going to be some hobbyists doing math in their basements, but there's unlikely to be a future for professional mathematicians.
That's exactly what the Simons foundation was set up to reject, and it's one of most important funding streams for math
The proof with the 11/12 constant, the simplest one, has already prompted what looks like chagrin from some. It's an unexpected combination of known results/techniques, a combination that apparently fell into a blind spot so it wasn't picked up before (even though it could have been, even 20 years ago).
I think these results are showing there was a lot of low hanging fruit that human mathematicians didn't have the breadth or mental bandwidth to find.
To address what you actually meant: it's possible but specifications are way easier to verify.
In general, once the proof has been formalized, it's supposed to be the proof of the correct theorem (that's what the Lean proof-checker checks)
the obverse would be to assert that Lean (or any other theorem prover) is infallible under all circumstances, present and future - an even weightier claim in my opinion.
But on the other hand, agree with you that the chances that one its bugs causes a solved proofs to be wrong is probably very, very low. Yeah, each version of Lean obviously must be run against hundreds if not thousands tests of existing proofs to ensure it's working correctly...
... Although, one thing that is a little worrying is that some mathematicians have said the Lean code generated in these OpenAI proofs is supposedly really complex and undecipherable. It might be pushing Lean to corner cases that are not well tested.
So as long as the "somewhat simple" core that checks to proof is correct, it doesn't matter if the "programming language" has bugs: either in the end the "proof assembly code" generated by the program is right and is validated by the core, or it's not, and you need to revise your proof, or to check for either a bug in the programming language (it didn't generate the proof you were expecting), or in very rare case detect a bug in the simple "core"
I never advanced in math past high school, but my assumption would be that we as a society aren't paying mathematicians to have fun[0]. The discoveries mathematicians make must translate into real improvements in engineering and other life improving fields. So why would we pay mathematicians to work on math much the same way, if a new machine-led way makes these discoveries faster and cheaper?
[0] Being a little facetious. I know I don't know what I don't know.
With math you never know up front what 'real improvements in engineering and other life improving fields' will require some key bit of it that someone interested in pure math came up with a decade or two (or 10) before we found an application.
Obviously. In my ideal world even the janitors at the same institutions would have a blast, it's just not usually the end-goal reason humans are hired.
>With math you never know up front what 'real improvements in engineering and other life improving fields' will require some key bit of it that someone interested in pure math came up with a decade or two (or 10) before we found an application.
Right, but would it have made a difference for the application layer if that key bit of "pure math" had been discovered by a human (that had a great time) or a machine? That's my point about games being a bad analogy.
For instance, almost all of cryptography is applied math. If your opponent understands the math better than you do you might end up with your secrets compromised.
Math is about as 'pure' a science as there is, the touchstone of applicability is missing the point entirely, it is first and foremost about understanding things at one of the most fundamental levels (even more fundamental than physics) that there is.
Nobody cares all that much about the discovery (except that we name things for the person that discovers it, it's sort of analogous to the discovery of a new piece of land). And given that the pay usually sucks this is a nice thing to be able to do. What mathematicians usually do really care about is their ability to understand the discovery and that this discovery has the proper foundations (other pieces of math that are also understood). It doesn't really matter what the answer is if you don't actually fully understand the question or the foundation the answer builds on.
Define "better".
LLM agents are perfectly capable of "advancing" my codebase down bizarre, esoteric rabbitholes. Meanwhile, the value remains undelivered.
Many crystals, likewise, are advancing their fantastic complexities in the deep, dark recesses beneath the crust of the earth, but does it make a sound? Who gives a shit.
Many paperclips, indeed, can be churned out. Even we can be converted into paperclips, remember.
And it's becoming less clear over time that a breakthrough will be needed.
We chose the problems to value. Literally every step of a proof is equally proved as the starting point. The choice of the starting point is what makes the problem, and it's a normative choice, which is to say it is a social choice.
I would like to be optimistic about the whole thing falling apart, but I don't know that it will.
They are saying this thing will soon obsolete human thought; meanwhile I use these tools every day and can't get it to refactor a React app cleanly without making a mess.
It's telling that OpenAI's decided they're going to sell ads in ChatGPT. Instead of, you know, using their AI themselves to produce all these valuable and revolutionary breakthroughs they claim it's capable of making.
If you have a super-intelligent AI that can cure cancer, just sell the cure for cancer already?
Intelligence is very rarely the limiting reagent in progress.
At issue with AI is that it's searching an existing corpus for fragments of solutions generated by humans - that's not necessarily novel, and we've not yet worked out how to make the machines actually invent.
Otherwise we're just creating a black box, easily manipulated by their owners, who would be ruling over human lives. That's not what people want
When AI writes proof no human can understand, it doesn't advance mathematics this way. Maybe AIs can understand their own proofs - meaning not just verify them but extract a machinery/broader-perspective (but I wouldn't count on it). But even machinery an AI isn't necessarily useful for humanity/society.
If that was true it would of course be significant.
If you had no morals, 2 trillion dollars to spend, ability to commit intellectual property theft without consequences, and most of the smartest people in the world actively working to advance your cause... ...you really think you couldn't compete with the clankers?
The wildcard is that we have no idea what the model after that will be capable of, or the model after that.
I would agree with you if these models were available to mathematicians, and OpenAI wasn't effectively competing with them by spending millions of dollars in compute to rush out solutions.
if these models were available to mathematicians
Why do I get this feeling that people who complain about these models not being accessible are the same ones who are anti-data center build out, thinks AI is in a bubble, and thinks AI labs are evil.
In other words, they want cheap, available access to highly intelligent models, but they believe everything about AI industry is wrong.
From TFA:
"I’m ready to board the plane, because I want to see what’s there. At the same time, I would add that people who previously have been walking around on earth with their eyes closed are not going to recognize anything however high they fly; I still believe that many of the skills that mathematicians have now will not only be transferable but vital to the new world order."
That sounds a bit disconnected and rude.
If we don't interview candidates based on results, what is it? Politics. It already was. I had a JEMS paper in grad school and got zero postdoc offers. Many other cases.
The real shift is that math will become a hobbyists game. Make money other ways and then spend your money on humans and tokens to solve your problems.
[1] https://archive.org/details/colossus-the-forbin-project-1970...
here is the direct link of the video which starts at 1800 seconds.
Offtopic: Fun fact but aside from archive.org there is also a way to have a link which links to any direct video at any time.
Someone made a good HN article about it that I vaguely remembered[0]
[0]: https://www.autodidacts.io/how-to-deeplink-to-specific-part-...
Machine proofs are useful machine understanding. You don't read the proofs, that's holding it wrong. You point another agent at the proof and prompt "use these ideas to prove this lemma that's useful to me". And it works, agents are faster given access to the proofs than without.