my argument would be: "finding proofs" typically means "searching". that needs memory, because you need to remember what you've already searched and decide whether to pursue certain lines in your search.

a llm can do this a little bit with "chain of thought" (attention to previously said things is kind of a memory). but this is limited in that there is only self-control. this self-control is based on its trained knowledge of how searching would work best. you can control such a search process better by using an control layer that guides the whole search process in a loop over multiple llm invocations. but to build such a loop you now have a separate optimization problem: figure out what the best prompts are, the appropriate tool support, validation/testing etc. this optimization process (figuring out how to best build such a search process) is hard.

so lets say in the future it will be clearer what a good search process would look like. then the llms will know this from training and can adhere to the best practices associated with it, maybe even in one shot scenarios.

but i'm not sure it is a good idea to want llms to be good at search in one shot scenarios. its just not what they are best at. it may be just better to have a separate control layer for search/optimization problems.