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.
I think GIT is a negative answer to a problem originally posed by David Hilbert. It was not proposed by Goedel originally. I think Goedel's main new idea was (i) inventing Goedel numbering (ii) using Goedel numbering to show that provability from a finite FOL signature, and a single FOL formula, is reducible to an equation involving primitive recursive functions (iii) devising a method to translate FOL statements about arbitrary primitive recursive functions into statements about only the two primitive recursive functions + and ×.
Later work establishing the field of computability theory (or "recursive function theory" as it was then known) generalised the insights (i) and (ii). In light of that, Goedel's only now-relevant contribution is (iii).
> When will LLM folks realize that automated theorem provers have existed for decades
This is very misinformed. Automated theorem proving was, sadly, mostly a disappointment until LLMs and other Machine Learning techniques came along. Nothing like the article's result was remotely within reach.
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.
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.