64 points smilelamp 1 hour ago 77 comments
bananaflag 1 hour ago | parent
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.
ivantop 1 hour ago | parent
0c3ca83 58 minutes ago | parent
And it's becoming less clear over time that a breakthrough will be needed.
awesome_dude 40 minutes ago | parent
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.
parodysbird 25 minutes ago | parent
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.
portalscriptcon 36 minutes ago | parent
cammikebrown 1 hour ago | parent
jnstrdm05 1 hour ago | parent
0c3ca83 56 minutes ago | parent
There's going to be some hobbyists doing math in their basements, but there's unlikely to be a future for professional mathematicians.
kaffekaka 49 minutes ago | parent
forgotpwd16 12 minutes ago | parent
whatshisface 36 minutes ago | parent
parodysbird 30 minutes ago | parent
That's exactly what the Simons foundation was set up to reject, and it's one of most important funding streams for math
ion_trapper 51 minutes ago | parent
pitchlatte 42 minutes ago | parent
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.
ericpruitt 40 minutes ago | parent
thevinter 16 minutes ago | parent
To address what you actually meant: it's possible but specifications are way easier to verify.
oulipo 10 minutes ago | parent
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)
aktuel 29 minutes ago | parent
ion_trapper 25 minutes ago | parent
afdbcreid 7 minutes ago | parent
computerdork 17 minutes ago | parent
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.
oulipo 8 minutes ago | parent
pfdietz 14 minutes ago | parent
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.
oulipo 11 minutes ago | parent
stillatit 49 minutes ago | parent
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.
jacquesm 46 minutes ago | parent
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.
stillatit 22 minutes ago | parent
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.
jacquesm 8 minutes ago | parent
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). What they do really care about is their ability to understand the discovery and that this discovery has the proper foundations. It doesn't really matter what the answer is if you don't actually fully understand the question.
forgotpwd16 15 minutes ago | parent
thrance 1 hour ago | parent
andsoitis 59 minutes ago | parent
Define "better".
dooglius 56 minutes ago | parent
gavmor 40 minutes ago | parent
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.
likoya 50 minutes ago | parent
conartist6 44 minutes ago | parent
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?
joe_the_user 33 minutes ago | parent
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.
oulipo 12 minutes ago | parent
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
0c3ca83 1 hour ago | parent
This analogy is pants on head stupid. They're talking as though the only thing AI will ever solve is the Langlands program, not as though we have discovered a generic tool.
It's like saying "they drove the car one mile -- and every mile driven leads to more roads that we can trot along, why are you so worried about the future of horses?"
wonnage 58 minutes ago | parent
0c3ca83 52 minutes ago | parent
If you've forgotten how to think for yourself, you can also ask an LLM.
The host of the blog, Tao, was an early booster. He didn't think through the implications, and seems to have expected it to remain unable to do interesting work. Today he's on a "war footing".
I don't think mathematics are uniquely skilled at predicting the future, and the impacts of AI on their profession.
kaffekaka 42 minutes ago | parent
I perfectly understand his point and it is not about being selfishly frustrated by a machine being better than him. Is that really your interpretation of the discourse?
wonnage 40 minutes ago | parent
https://fortune.com/article/ai-godfather-radiologists-obsole...
Ironic that you resort to “think for yourself” as your silly name calling go to btw
ghusto 44 minutes ago | parent
wonnage 37 minutes ago | parent
ion_trapper 27 minutes ago | parent
sjdh76 47 minutes ago | parent
QuesnayJr 29 minutes ago | parent
If we have a theorem proving machine, then we can use it to prove theorems. If we have a machine to solve the Langlands program in one day, then we'll think of more things to prove after that. There's a million unsolved questions in number theory unrelated to Langlands, and if we knew Langlands (and why it was true) we could make new conjectures that our theorem proving machine could solve, rather than having to speculate for 50 or 100 years like now.
The possibility he's not considering is that the machine might be better even at conjectures, and then there really is no role for humans once the machine already knows things our primitive meat brains are too small to understand. But what he's saying isn't "pants on head stupid".
fooker 57 minutes ago | parent
CS had this moment decades ago, sans some theoretical parts that are joining the bandwagon now.
I did a bit of math research in grad school collaborating with my math postdoc roommate. I found the aversion to any computation making its way into the craft to be odd decades ago.
Well, now the proof’s in the AI generated pudding.
bsaul 45 minutes ago | parent
My recent take on AI is that people haven't adapted to the new huge potential of the tool, and don't dream big enough (yet).
It's like seeing a car engine for the first time, lamenting about the future of horses, and not realizing it'll also help us fly.
hmokiguess 30 minutes ago | parent
There’s an immediate resistance towards change rather than embracing it and finding opportunities to improve and work with it.
kaffekaka 29 minutes ago | parent
Singularity? Probably not.
Tech bro dictatorship? Unfortunately a bit more likely.
None of the above? Then we have a small shot at a great future.
Having a machine that solves hard problems must be a good thing.
disfictional 27 minutes ago | parent
ethanlipson 20 minutes ago | parent
There might be a “proof motive” in math which one could argue will drive the full automation of theorem proving. But we must recognize that profit is more universally valuable (i.e. it has value outside the industry in which it was created), whereas proofs are only valuable inside the math community (at least the pure math proofs the labs have been publishing thus far).
bcvvvy 12 minutes ago | parent
You can drive 1000 miles and arrive at the destination on the highway quickly.
Or you can take the slow road and walk. You discover unrelated things, make new relationships, see the scenery, listen and smell what is around you and have time to contemplate things which may or not be related.
This particular tool economy robs us of all these things in the rush to the destination.
I'd sacrifice "progress" a little for some of the better bits of humanity.
Trusteando 4 minutes ago | parent
kccqzy 35 minutes ago | parent
Yup. This is what Terence Tao has been saying about digestion of results for several months now. Mathematics has become a field where results themselves matter less, the social aspect of attracting others to understand your results and explore new problems has become more important.
In a sense it is a little bit like software engineering, where writing code can sometimes be delegated to AI, and is arguably less important than understanding what the customer really wants from this software.
georgemcbay 2 minutes ago | parent
> To me, someone who chooses a worthwhile problem, obtains a proof completely using AI, understands it thoroughly, and uses it to develop interesting further questions or directions has made a substantial mathematical contribution. I would give that person substantial credit even if they supplied no new ingredient in the original proof.
Given the approximate $10-22 million API costs of solving these major math problems currently, we will also have to acknowledge that getting credit for major mathematical contributions could in many cases be less meritocracy and more about funding.
Less capable (but good enough) mathematicians with more capital will have a huge advantage over great mathematicians who are broke.
I'm not a mathematician, but that situation rubs everyone (except those with the most capital) the wrong way.
ur-whale 27 minutes ago | parent
waynecochran 26 minutes ago | parent
stephbook 19 minutes ago | parent
It took us a while to make the planets line up neatly in a heliocentric system. Just last month I read that a whale mother "might" grief while carrying her stillborn child.
The limiting factor is human imagination and comprehension. No offense, but see your comment.
I think AI has already invented new math, but the guys haven't looked for it because they didn't think it possible. And even under their noses, they wouldn't understand what they see.
> It's not what you look at that matters, it's what you see. —Thoreau
pfdietz 11 minutes ago | parent
They have been so far.
waynecochran 3 minutes ago | parent
Could AI create a novel set of axioms (a new math) from which things like RH become a by product? I think that would be hard to miss.
ethanlipson 10 minutes ago | parent
> other skills will matter more: choosing which terrain is worth exploring, steering fleets of airplanes, and explaining what they find to the rest of the world.
These all seem totally achievable by LLM agents, or at least, I don’t see an obvious reason why it wouldn’t be. 3blue1brown’s recent discussion on this subject was a bit better, but he spent the plurality of main body of the video assuming this scenario, devoting less time to the other possibilities. To me, it seems dangerous to build a math career on the foundation that AI won’t be able to explain math well in a few years, let alone a few months (which seems entirely plausible given the recent math progress).