[William_BB]

There's a big difference between one shotting a counterexample using AI and using AI to find a counter-example by brute-force.

Both are impressive, of course, but they're hardly comparable.

[eru]

I'm not so sure. People had been trying to use brute force to find counterexamples before.

[William_BB]

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.

[igravious]

"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

[YeGoblynQueenne]

LLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.

[tptacek]

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.

[YeGoblynQueenne]

>> The model was perfectly capable of verifying its correctness.

It's an LLM. It can't do that.

[astrange]

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.

[YeGoblynQueenne]

What are the search algorithms then? DFS, BFS, A*, etc, can you name them?