I would say the mathematical proof could be extended or modified by infinitely many variants, so LLM could be used as a heuristic to guide the search based on similarities or previous approaches or just based on the context of the failing cases.