Hacker News Reader

Comment by applfanboysbgon | Hacker News Reader

Two points:

- Hasn't been peer reviewed yet, so take with a grain of salt. This applies to all claimed proofs, not just AI-generated ones. Even humans hallucinate proofs too!

- The prompt is on page 27 here[1]. It is ten pages of advanced mathematics priming the model in the right direction, apparently informed by a year of prior research. That doesn't invalidate the result if it is genuine, but it is worth noting that this wasn't a matter of "ChatGPT, solve this unsolved problem. Make no mistakes." and required substantial domain expertise and human research beforehand.

[1]https://arxiv.org/pdf/2607.13335

View on HN

It is lean-verified, so it can be trusted unless the Lean statement of the hypothesis is not an accurate description of the hypothesis.

Saying “solve this problem” doesn’t get good results most of the time with humans either, it’s entirely underspecified so the person assigned that problem may solve it in a variety of unacceptable ways or not at all or perhaps worse solve the wrong problem because you weren’t clear about its definition. This actually happens all the time. What matters is the ability to communicate clearly and with precision as well as the “harness” which for humans is procedure, training, planning and management.

> Saying “solve this problem” doesn’t get good results most of the time with humans either

Sure. That is not even remotely the point I was getting at. Already we see the thread filling up with comments about how human skills are irrelevant, using a mathematics PhD applying his expert skills in a way that the people who are saying that could never have done to justify their inane conclusion.

The subtext of this whole post (or at least a subtext that some might read), is "we don't need mathematicians/programmers anymore" or "we will need much fewer mathematicians/programmers". So the fact that this result required a year of prior research and a 10 page prompt of specialized knowledge goes against that subtext. You still needed the human just as much to get to the result, and the LLM ended up being a tool to find the last bit.

Digression: You can link directly to a page in a pdf with a url like this: https://arxiv.org/pdf/2607.13335#page=27

> but it is worth noting that this wasn't a matter of "ChatGPT, solve this unsolved problem. Make no mistakes."

It wasn't the case for this, but when OpenAI disproved the Unit Distance Conjecture, it was really done autonomously by an automated AI pipeline with a completely AI-generated prompt. No human expertise required at all in the process (well, except for the final human verification).

Without human verification, an LLM can generate correct or incorrect proofs but it can't tell the difference. A human is necessary to be able to tell one from the other.

Saying that's a solution "done autonomously by an automated AI pipeline" is like saying that a self driving car that can only take you to the nearest train station after which you have to ride the rain to where you're going is "autonomously" driving you to your destination. Which is exaggerating the autonomy of the system, rather.

The automated AI pipeline also had an automatic grading model to try to reduce false positives.

But anyway, my point was that in that case the prompt involved was indeed pretty much "hey, ChatGPT, solve an unsolved problem, thanks."

Yes, but there's no way to tell how many times the prompt was tried before a proof was found; and that only stopped when a human said it could stop.

Reply on news.ycombinator.com