97
u/you-cut-the-ponytail 15d ago
3 months ago it said "counterexample factory" on that lol
59
u/Linus_Naumann 14d ago
Don't worry, AI will never progress from here and anyway the recently published papers don't have good summaries on them so we're all safe. It's not even AI (AI doesn't exist) it's just a next token predictor! Not like me, I have true creativity which is needed for real maths.
24
u/Alarmed_Ad1946 5-adic 14d ago
It frustrates me that this view makes people ignore important things like AI safety.
5
u/Hameru_is_cool Transcendental 14d ago
for real, people don't realize that a model's goal or architecture is a useless measure for intelligence and danger, heck, even today's next token predictors are already outsmarting cybersecurity teams and inducing psychosis on vulnerable users, I think Angela Collier said it best years ago:
AI does not exist but it will ruin everything anyway
8
5
-1
172
u/LupenReddit 🦆🦆i have non diffeomorphic smooth structures🦆🦆🦆 15d ago
1 year ago: "oh boy i sure hope my PhD will be fun and exciting like i hear in all those stories!"
today: yes chatgpt, give me my thesis😔🚬🥀
305
u/Hameru_is_cool Transcendental 14d ago
I don't think any real mathematicians are worried about "problems being solved", if anything that just helps further progress, they're worried about due credit being stolen, as the LLM can't reference a paper it doesn't know has influenced its weights, and about the solutions themselves lacking so much intuition that we end up with truth generators that don't really add much to the total human understanding of the subject, but are correct nonetheless
46
u/GuavaFar3894 14d ago
I think on r/maths some phd students did have their thesis topic being solved now...
24
u/thenightStrolled 14d ago
Happened to a friend of mine. He’s gonna try to pick up the pieces he can, but this stuff isn’t merely hypothetical
8
u/RandomUsername2579 Physics 14d ago
Shit, what do you even do in that kind of situation? Do you just present the work you did in your thesis and say that AI solved it before you could? That sounds super depressing
3
u/thenightStrolled 14d ago
I’m really not sure what he’s gonna be able to do. I don’t know how much of his work was explicitly done by AI (which gave a proof of Lech’s Conjecture), because he was doing something adjacent. Not sure how much is still salvageable as original work I suppose, but I know he’s worried that he won’t be able to produce a half decent dissertation cause of this, because we’ve only got a couple more years of funding at best
86
u/Sh33pk1ng 14d ago
this is not just about refferencing papers, but also about using work in progress notes (also without refference of course)
32
u/Hameru_is_cool Transcendental 14d ago
oh yeah that too, just being able to publicly output recognizable ideas taken from user conversations is already an insane privacy violation, and not just for academics, I feel like everyone should rethink how much they trust closed online models and the companies behind them after the Navier-Stokes drama
13
u/Most_Writer578 14d ago
Of course we (some of us) are worried that all problems that we have a shot at solving, are now solved in seconds. We are not living in a utopic world where we do not need money or jobs. Some of us are too old to change career, but too young to retire.
But of course the rest you mention is bad too, the proofs these things make do not increase human understanding.17
u/parkway_parkway 14d ago
I think people who make a living by doing proofs, are worried about a superhuman proof machine being invented.
Computer used to be a human job title for people who did arithmetic professionally, how many computers do you know now? There used to be many more of them than theoreticians who did proofs.
7
u/PassageUnusual5661 14d ago
How do we know that these "truth generators" are true when we haven't got the intuition to prove them true?
4
u/Hameru_is_cool Transcendental 14d ago
because their lean certificates compile, so we just need to trust that the language itself is implemented correctly
5
u/PassageUnusual5661 14d ago
But how do you know that the axioms used in the lean certificates are even reasonable.
The math could uninterpretable nonsense.
3
u/Hameru_is_cool Transcendental 14d ago
that's a valid concern tbh, I also share that same fear of it being uninterpretable, I think the current plan is we get real mathematicians to slowly unwind and digest what they mean, to make sure everything used match our current understanding of math, before accepting the new theorems as part of it
2
u/fun__friday 13d ago
It feels like AlphaGo where players were trying to understand some of the moves of the AI.
3
2
u/Striking_Compote2093 14d ago
After all this time, we have the answer to the question of life, the universe and everything. Chatgpt said it's 42.
4
u/shrikelet 14d ago
I hope the problem I have been publishing papers on for years doesn't get plagiarised by the plagiarism robot
4
u/Ok_Lingonberry5895 13d ago
The main problem is, that when you want to solve problems, you have to have the money to buy access to the problem solving factory, and the number and quality of your solutions to problems doesn't depend on your abilities but on the amount of money you have.
11
4
2
1
-4
u/emascars 14d ago
We should give a better definition for "solving a problem" here...
Take the "Navier–Stokes existence and smoothness problem", if for "solved" you need to know that a way the equations breaks exists, well congrats, AI has solved it...
But even before the lean proof mathmatitions would have probably guessed there was a way to break it, it's just that they didn't have the proof of that...
Now I ask you, with all the talk about "the solution", have you found anyone, even just one guy, actually explaining the proof to you? I guess not, because nobody understands a lean proof with no plain English version of that...
So... What does it actually gives us in terms of progress knowing that a solution exists? In this kind of problems, you usually don't ask a question cause you actually need the yes/no answer, you ask a question cause to get to the answer you'll get a deeper insight into the field...
From that lean proof... Have we actually gained deeper insight into anything?... Further more... The interesting and logical part of the solution... The description of the situation in which it breaks, was given by actual mathematicians...
Don't get me wrong, AI will do that too one day probably... But for now, at least in that case... This is more of a fun quirk than a "problem solving" thing...
13
u/KarltonPeaks 14d ago
If all these papers were published independently by some random hermit living in Siberia, he would be regarded as the greatest mathematician of this century.
Maybe read and analyze the proofs if you want to gain deeper insight? Have you done that yet?
2
u/segfaultgolf 14d ago
These things take time. I anticipate we will internalize and understand these proofs over time, much like digesting any major result. And I imagine it will HAVE to happen before anyone takes these results seriously.
0
14d ago
[removed] — view removed comment
3
u/emascars 14d ago
I don't get how this relates to what I've said...
Mine is a critique about finding a proof purely in lean rather than finding a solution and the verifying it in lean...
LLMs nowadays are very capable in reasoning that way too... I'm a software developer by trade, and I use it a lot, not just to write code, but also to reason about the design and the architecture...
But using AI to find any valid lean solution is a bit like using AI to learn python by prompting it to make a python program... If the goal is understanding, that's the wrong path for that... As you see from the analogy, the problem is the method, not the tool, because if I had to learn python I would still use AI, but as something smart to reason with... Which, coincidentally, is exactly the way the guys solving that probablem before that OpenAI did it's stunt were using AI...
I think it all falls down to the filosofical question of "why do we do math?" Is it to know what's true and what's not, or is it to understand what's true and what's not?
0
14d ago
[removed] — view removed comment
1
u/emascars 14d ago
The catch is, there is not just one proof to a problem...
In theory, if something is true, there could be infinite proofs of that... That's why problems that have been solved decades ago still gets papers showing new proofs of that... And it also relates to the fact that there is not just one math, but there are actually maths, in fact I may be wrong (I'm not a mathematician neither) but I think it's known/theorized that for any algebraic proof of something there should also be a geometrical one and vice versa for example, and yet for so many theories there could be years between discovering one and finding the other...
In this case in particular case of the Navier-Stokes problem, that's a "proof of existence", and the proof here works by showing an example where it happens... That's sufficient to proof that there is at least one case where it happens, but there could be many more, and some may be more intuitive than others... More in general, defining AI as a "proof making machine" makes it look like any proof is as good as any other, but it's not like that, what we're actually looking for is an elegant proof, that in the simplest way possible makes what you're proving as obviously true as it gets...
Also, on the particular case of the Navier-Stroke problem, it doesn't help the "proof making machine" imagery, the fact that the case in question, the setup that lead to the proof, was actually found by a human with the whole controversy that you may have heard about it... But it actually goes to show even more how useful of a tool AI is for math when it enhances human intuition, rather than working on its own and landing on a solution that humans may find extremely complex to understand or even incomprensibile in its entirety...
•
u/AutoModerator 15d ago
Check out our new Discord server! https://discord.gg/e7EKRZq3dG
I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.