AI is great at reducing the search space and using human-like reasoning (in a brute-force way) to carry out the brute-force search. I'm not surprised by this result. This is exactly what AI should excel at, with human guidance.
"using human-like reasoning (in a brute-force way)"
that's self-contradictory -- what brute force means is doing an exhaustive search of a search space (brute forcing it)
using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree
That's not what happened here. This isn't a proof; it's a counterexample. The model was perfectly capable of verifying its correctness. You could have verified it by hand if you wanted; the verification is trivial. Finding it was the hard part.
Are you doing the "LLMs don't know how many R's are in 'Raspberry'" thing here?
A bunch of people on the original thread about the Conjecture were like "we need to wait and see if real mathematicians verify this proof it's probably just LLM psychosis", because they don't understand that the counterexample is a trivial calculation. Checking it isn't hard; any AP calc student can do it quickly. It's finding the counterexample that's the challenge.
It's as if someone presented a SHA-2 collision, which anyone could just feed to `openssl sha256` to see, and then naysayers were like "we need to wait for independent verification because the LLM can't know if that collision was real".
Checking, it how? I mean can you describe the mechanism? How does an LLM "check" that something is (or isn't) a counterexample? Does that involve pattern matching, formal verification or model checking, some other approach?
In this case, the same way I would -- calling out to SymPy.
Once you verify (with SymPy or another CAS, like Mathematica) that the given function has the claimed Jacobian determinant (which involves only taking partial derivatives and taking a determinant) and the given inputs map to the same output (which involves only evaluating polynomials with some inputs), you're done.
>> using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree
So according to the OP there's a search of a tree and it also uses pruning btw, so I want to know what search they mean. Why are you asking?
Sorry, that's just egregious abuse of terminology. Either you're pruning the branches of a tree (or other graph, potentially) when you're doing a tree search, or you don't do pruning. Specifically advice taking (if that's what you mean) is not pruning.
It's a direct quotation from your comment, not a "scare quote". How does "implicit search" do pruning? Can you explain?
Edit: Turns out "implicit search" is actually a thing in the literature, albeit introduced in a single paper I could find that claims Diffusion Modelling does it:
