Comment by ogogmad

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