[alan-crowe]

I've been thinking of the issue like this: a traditional approach to symbolic artificial intelligence frames problem solving as a search of a tree. Do you go depth first, dodging infinite branches? Or breadth first (do you have enough memory?). What about iterative deepening?

Sometimes the solution is in the tree, but it is too deep, and one runs out of time before it is found.

Statistical based learning could act as a branch predictor. Sometimes guiding the search to go very deep in the right place and find the hidden solution. Sometimes guiding the search to go very deep in the wrong place; one runs out of time as usual.

Notice the strength of hybrid approach. One isn't accepting the probably correct answer of the statistical part. It is only a guide, and if the answer is found, and the symbolic part of the software is correct, the answer will be reliable.

I think this is already being done with maths problems. The LLM is writing proof attempts in Lean. But Lean is traditional symbolic AI. If the LLM can come up with a proof that Lean approves, then it really has a proof. From your comment I learn that Stockfish has already got something like this to work very well.