64 points smilelamp 1 hour ago 76 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 56 minutes ago | parent
And it's becoming less clear over time that a breakthrough will be needed.
awesome_dude 38 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 23 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 34 minutes ago | parent
cammikebrown 1 hour ago | parent
jnstrdm05 1 hour ago | parent
0c3ca83 55 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 47 minutes ago | parent
forgotpwd16 10 minutes ago | parent
whatshisface 34 minutes ago | parent
parodysbird 29 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 49 minutes ago | parent
pitchlatte 40 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 39 minutes ago | parent
thevinter 14 minutes ago | parent
To address what you actually meant: it's possible but specifications are way easier to verify.
oulipo 8 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 28 minutes ago | parent
ion_trapper 23 minutes ago | parent
afdbcreid 6 minutes ago | parent
computerdork 15 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 7 minutes ago | parent
pfdietz 13 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 9 minutes ago | parent
stillatit 47 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 45 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 20 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 6 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 13 minutes ago | parent
thrance 58 minutes ago | parent
andsoitis 57 minutes ago | parent
Define "better".
dooglius 54 minutes ago | parent
gavmor 38 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 48 minutes ago | parent
conartist6 43 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 32 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 10 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 59 minutes 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 56 minutes ago | parent
0c3ca83 50 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 40 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 39 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 42 minutes ago | parent
wonnage 35 minutes ago | parent
ion_trapper 25 minutes ago | parent
sjdh76 46 minutes ago | parent
QuesnayJr 28 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 55 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 43 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 29 minutes ago | parent
There’s an immediate resistance towards change rather than embracing it and finding opportunities to improve and work with it.
kaffekaka 27 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 25 minutes ago | parent
ethanlipson 18 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 10 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.
kccqzy 33 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.
ur-whale 25 minutes ago | parent
waynecochran 24 minutes ago | parent
stephbook 17 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 9 minutes ago | parent
They have been so far.
ethanlipson 8 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).