The announcement says:
reply> This was solved by GPT-5.4 Pro (prompted by Price)
See the discussion here: https://www.erdosproblems.com/forum/thread/1196
"are we talking pure LLMs, or existing AI solvers augmented with LLM"
replyWhy do these distinctions matter?
is it an LLM, or symbolic, or a combo, or a dozen technologies stitched together. Who cares. It is all automation. It is all artificial.
True, it's an achievement either way. But if an "out of the box LLM" can solve difficult math problems it is an achievement by the LLM vendor. Otherwise it is an achievement by the people doing the vertical integration.
replyIn the context of evolving LLM this is the crucial distinction.
The distinctions matter since computational proofs have been around for decades.
reply