undefined

points

[-]

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

by throwthrowuknow13 hours ago|

prev|

[-]

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.

by camdenreslink12 hours ago|

parent|

[-]

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.

by applfanboysbgon13 hours ago|

parent|

prev|

[-]

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

by varenc9 hours ago|

prev|

[-]

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

by andy12_9 hours ago|

prev|

[-]

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

by YeGoblynQueenne3 hours ago|

parent|

[-]

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.