5 ms·

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 tha

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.

crazylogger 6mo ago
"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)?
- dmurray 6mo ago
  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.
virgildotcodes 5mo ago
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.
throwaway198846 5mo ago
Automated theorem provers can't prove this problem. Which non-trivial Math problem you think are thougher than this Erdos problem?
ogogmad 5mo ago
> Proposing 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.

crazylogger 6mo ago

"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)?

dmurray 6mo ago
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.

virgildotcodes 5mo ago

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.

throwaway198846 5mo ago

Automated theorem provers can't prove this problem. Which non-trivial Math problem you think are thougher than this Erdos problem?

ogogmad 5mo ago

> Proposing 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.