“People are complaining that AI is pushing out this 100,000-line formal proof of some major conjecture. I don’t really see what harm this does because you can always ignore this if you want, and then you’re no worse off than before,” Borcherds said. “I think what people are getting upset about is they’re slowly realizing that they are dumb and somehow blaming this on AI, even though it’s not really AI’s fault.”
This is basically why I can't take any mathematician arguments at face value. It seems like the majority of them intertwine some sort of status game with their arguments.
I also realize the "status game" is needed for funding / grants, but that is irrelevant to AI/LLMs, for example, you can ask whether this was the right method to begin with although it "worked" in some way or sense prior to the release of AI/LLMs. To ask the world to change at their pace or at their whim is very unlikely to happen.
Prep the community for what. Every human can make decisions and choices without care for another already.
They are perfectly happy with their choice. They already chose to ignore the papers and that's fine.
What is objectively true is by definition true. What one considers to be true is not necessarily objectively true.
You can chose to live under the "romantic" mathematics era if you so wish for it, we are temporary and our direct influence is at most a few generations. To force the future or that choice to anyone else, I'm sorry, but I rather be delusional than accept that (though obviously untrue). It isn't a choice up to you, at most you provide a path, but you have very little choice over what the future dictates.
At least at the cheap plan level, for 3 or 4 pages AI is better than me at clear math problems. For longer problem or fuzzy objectives, I've seen small errors of bad decisions here and there.
The problem is that AI is very convincing and the text make sense but it's a wall of text that may include lemas, sublemas, theorems, citations and everything you expect in a real solution. But for now in long proof is difficult to be sure that there is no a tiny details that makes everithing invalid.
(My guess is that most of the AI proof in the Mathpocalypse are correct. I think 5 are retracted and 10 fixed, but I expect a few more error, but not too many.)
Meanwhile, in my opinions: Lean or it didn't happen.
4 comments
[ 2.5 ms ] story [ 32.9 ms ] threadThis is basically why I can't take any mathematician arguments at face value. It seems like the majority of them intertwine some sort of status game with their arguments.
I also realize the "status game" is needed for funding / grants, but that is irrelevant to AI/LLMs, for example, you can ask whether this was the right method to begin with although it "worked" in some way or sense prior to the release of AI/LLMs. To ask the world to change at their pace or at their whim is very unlikely to happen.
Youre deluded.
They are perfectly happy with their choice. They already chose to ignore the papers and that's fine.
What is objectively true is by definition true. What one considers to be true is not necessarily objectively true.
You can chose to live under the "romantic" mathematics era if you so wish for it, we are temporary and our direct influence is at most a few generations. To force the future or that choice to anyone else, I'm sorry, but I rather be delusional than accept that (though obviously untrue). It isn't a choice up to you, at most you provide a path, but you have very little choice over what the future dictates.
The problem is that AI is very convincing and the text make sense but it's a wall of text that may include lemas, sublemas, theorems, citations and everything you expect in a real solution. But for now in long proof is difficult to be sure that there is no a tiny details that makes everithing invalid.
(My guess is that most of the AI proof in the Mathpocalypse are correct. I think 5 are retracted and 10 fixed, but I expect a few more error, but not too many.)
Meanwhile, in my opinions: Lean or it didn't happen.