Comment by thesmtsolver2
11 hours ago
When will LLM folks realize that automated theorem provers have existed for decades and non-ML theorem provers have solved non-trivial Math problems tougher than this Erdos problem.
Proposing and proving something like Gödel's theorem's definitely requires intelligence.
Solving an already proposed problem is just crunching through a large search space.
Automated theorem provers can't prove this problem. Which non-trivial Math problem you think are thougher than this Erdos problem?
So the only intelligent people in history are those who invent new fields of mathematics, got it.
You can just about make out those goalposts on the surface of the moon with a good telescope at this point.
"Hi ChatGPT, propose and prove something radically new in the genre of Gödel's theorem."
How is this not just another proposed problem (albeit with a search space much larger than an Erdos problem's)?
I think the point the GP is making is that Gödel's theorem wasn't part of any "genre". Gödel, or somebody, had to invent the whole field, and we haven't seen LLMs invent new fields of mathematics yet.
But this isn't a fair bar to hold it to. There are plenty of intelligent people out there, including 99% of professional mathematicians, who never invent new fields of mathematics.