Comment by resident423

10 hours ago

Remember when people thought solving Erdos problems required intelligence? Is there anything an LLM could ever do that would cound as intelligence? Surely the trend has to break at some point, if so what would be the thing that crosses the line to into real intelligence?

> Remember when people thought solving Erdos problems required intelligence? Is there anything an LLM could ever do that would cound as intelligence?

Hah. It reminds me of this great quote, from the '80s:

> There is a related “Theorem” about progress in AI: once some mental function is programmed, people soon cease to consider it as an essential ingredient of “real thinking”. The ineluctable core of intelligence is always in that next thing which hasn’t yet been programmed. This “Theorem” was first proposed to me by Larry Tesler, so I call it Tesler’s Theorem: “AI is whatever hasn’t been done yet.”

We are seeing this right now in the comments. 50 years later, people are still doing this! Oh, this was solved, but it was trivial, of course this isn't real intelligence.

  • That is a “gotcha” born of either ignorance (nothing wrong with that, we’re all ignorant of something) or bad faith. Definitions shift as we learn more. Darwin’s definition of life is not the same as Descartes’ or Plato’s or anyone in between or since because we learn and evolve our thinking.

    Are you also going to argue definitions of life before we even learned of microscopic or single cell organisms are correct and that the definitions we use today are wrong? That they are shifting goal posts? That “centuries later, people are still doing this”? No, that would be absurd.

    • I don't see it as a gotcha. Just an (evergreen, it seems) observation that people will absolutely move the goalposts every time there's something new. And people can be ignorant outsiders or experts in that field as well.

      For example, ~2 years ago, an expert in ML publicly made this remark on stage: LLMs can't do math. Today they absolutely and obviously, can. Yet somehow it's not impressive anymore. Or, and this is the key part of the quote, this is somehow not related to "intelligence". Something that 2 years ago was not possible (again, according to a leading expert in this field), is possible today. And yet this is somehow something that they always could do, and since they're doing it today, is suddenly no longer important. On to the next one!

      No idea why this is related to darwin or definitions of life. The definitions don't change. What people considered important 2 years ago, is suddenly not important anymore. The only thing that changed is that today we can see that capability. Ergo, the quote holds.

      4 replies →

I've spend a good chunk of time formalising mathematics.

Doing formalized mathematics is as intelligent as multiplying numbers together.

The only reason why it's so hard now is that the standard notation is the equivalent of Roman numerals.

When you start using a sane metalanguage, and not just augmrnted English, to do proofs you gain the same increase in capabilities as going from word equations to algebra.

  • >the standard notation is the equivalent of Roman numerals.

    But the Roman numerals are easy. I was able to use them before 1st grade and I can't touch any "standard notation" to this day.

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.

Well, the famous Turing test was evidently insufficient. All that happened is that the test is dead and nobody ever mentions it anymore. I'm not sure that any other test would fare any better once solved.