The success in Go was very much not dumb search. Where dumb search had failed to achieve the level of even a very weak player, the neural net's "intuition" about good moves without any search was already very strong. Only the combination was superhuman, and that was anything but the dumb search that had been tried before.

Today's announcement is also not about proving Lean theorems by "dumb search". The success is about search + neural networks.

You're attacking critics for criticizing the solution that has failed, while confusing it for the solution that works to this day.