alt Hacker NewsWhen 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.
Replies
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)?
Automated theorem provers can't prove this problem. Which non-trivial Math problem you think are thougher than this Erdos problem?