Live data from Hacker News

Amateur armed with ChatGPT solves an Erdős problem

scientificamerican.com

221–230 of 607 posts

Re: Amateur armed with ChatGPT solves an Erdős problem

#221
post #202

It seems like alot of scientific advancements occurred by someone applying technique X from one field to problem Y in another. I feel like LLMs are much better at making these types of connections than humans because they 1) know about many more theories/approaches than a single human can 2) don't need to worry about looking silly in front of their peers.

Exactly. Much of the intellectual work is, in fact, intellectual labor . It’s mostly about combining various information in one place — the exact task that LLM far outperforms human. People traditionally misclassified this class of work as “creative”. It’s not really.

This is exactly what creativity is.

Re: Amateur armed with ChatGPT solves an Erdős problem

#222

The LLM took an entirely different route, using a formula that was well known in related parts of math, but which no one had thought to apply to this type of question. Of course LLMs are still absolutely useless at actual maths computation, but I think this is one area where AI can excel --- the ability to combine many sources of knowledge and synthesise, may sometimes yield very useful results. Also reminds me of th…

> "a broken clock is right twice a day" and homo sapiens, glancing at the clock when it happens to be right , may conjure an entire zodiac to explain it.

And homo sapiens, glancing at a system that gets better and better at solving problems, tries to deny it and comes up with the broken-clock analogy.

Re: Amateur armed with ChatGPT solves an Erdős problem

#223

Earlier quoted context omitted.

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.

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

Re: Amateur armed with ChatGPT solves an Erdős problem

#224

Earlier quoted context omitted.

Ask it to formalize it in Lean.

If they aren't "smart enough" to know if it work they most likely are also unable to verify if the Lean formalization is indeed the one that matches the problem they were trying to solve.

Verifying that every step in a (potentially long) proof is sound can of course be much, much harder than verifying that a definition is correct. That's kind of the whole point.

Re: Amateur armed with ChatGPT solves an Erdős problem

#225

Earlier quoted context omitted.

> Each time there's a new model release a few more get solved. I'm no expert, but based on the commentary from mathematicians, this Erdős proof is a unique milestone because the problem received previous attention from multiple professional mathematicians, and the proof was surprising, elegant, and revealed some new connections. The previous ChatGPT Erdős proofs have been qualitatively less impressive, more akin to l…

>one wonders if stoking the model to be unconventional is part of the success I've long suspected that a lot of these model's real capabilities are still locked behind certain prompts, despite the big labs spending tons of effort on making default responses to simple prompts better. Even really dumb shit like "Answer this: ..." vs "Question: ..." vs "... you'll be judged by " that should have zero impact in an ideal…

Just the right "prompt" is exactly what happened here. Lean has been developed and incorporated into it's data set. Also, token responses only vaguely correlate to "human language" and it's been proven transformers develop their own internal representation that has created a whole field called machanistic interpretation. Being able to more correctly "parse", AKA using Lean and the right "Prompts, insights and suggestions", will take a whole new meaning in the future.

Re: Amateur armed with ChatGPT solves an Erdős problem

#226

Earlier quoted context omitted.

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 a…

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.

Re: Amateur armed with ChatGPT solves an Erdős problem

#227
post #202

It seems like alot of scientific advancements occurred by someone applying technique X from one field to problem Y in another. I feel like LLMs are much better at making these types of connections than humans because they 1) know about many more theories/approaches than a single human can 2) don't need to worry about looking silly in front of their peers.

Exactly. Much of the intellectual work is, in fact, intellectual labor . It’s mostly about combining various information in one place — the exact task that LLM far outperforms human. People traditionally misclassified this class of work as “creative”. It’s not really.

Having a new insight that leads to the combination of two distinct ideas is definitionally creative.

You can say this problem needed a low amount of total creativity, but saying it's void of all creativity seems wrong.

Re: Amateur armed with ChatGPT solves an Erdős problem

#228
post #189

Given by the fact that the problem is 60 year old, isn't there a chance this was indirect solved already and the model just crossed informations to figure out the problem? By looking the website this problem was never discussed by humans. The last comments were about gpt discovering it. I was expecting older comments coming to a 60 year old problem. Am I missing something? Great discovery though, there might be probl…

To some extent, does it matter? If models are able to pull and join information that already existed in pieces but humankind never discovered by itself, doesn’t this count towards progress anyways?

It would be very helpful to know in understanding the capabilities of the models; and in getting intuition about where they are best applicable.

If the reason it was able to output the proof is that it happened to be included in an in-house university report written in Georgian, then that would make it less useful for research than if it's new entirely.

Re: Amateur armed with ChatGPT solves an Erdős problem

#230

Earlier quoted context omitted.

If they aren't "smart enough" to know if it work they most likely are also unable to verify if the Lean formalization is indeed the one that matches the problem they were trying to solve.

Verifying that every step in a (potentially long) proof is sound can of course be much, much harder than verifying that a definition is correct. That's kind of the whole point.

That's not what the parent comment meant. They meant checking the Lean-language definitions actually match the mathematical English ones, and that the Lean theorems match the ones in the paper. If that's true then you don't actually need to check the proofs. But you absolutely need to check the definitions, and you can't really do that without sufficient mathematical maturity.
Post reply on HN