3 ms·

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 hallucin

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 https://arxiv.org/pdf/2607.13335

throwthrowuknow 3mo ago
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.
- applfanboysbgon 3mo ago
  > 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.
- camdenreslink 3mo ago
  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.
lozenge 3mo ago
It is lean-verified, so it can be trusted unless the Lean statement of the hypothesis is not an accurate description of the hypothesis.
andy12_ 3mo ago
> 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).
- YeGoblynQueenne 3mo ago
  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.
  - andy12_ 3mo ago
    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."
    - YeGoblynQueenne 3mo ago
      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.
varenc 3mo ago
Digression: You can link directly to a page in a pdf with a url like this: https://arxiv.org/pdf/2607.13335#page=27 https://arxiv.org/pdf/2607.13335#page=27

throwthrowuknow 3mo ago

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.

applfanboysbgon 3mo ago
> 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.
camdenreslink 3mo ago
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.

lozenge 3mo ago

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

andy12_ 3mo ago

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

YeGoblynQueenne 3mo ago
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.
- andy12_ 3mo ago
  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."
  - YeGoblynQueenne 3mo ago
    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.

varenc 3mo ago

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