After it bulldozes the problem, can you not then use the LLM to help you understand the solution, bit by bit?
Mathematicians are saying the current papers are pretty inscrutable and use terminology unfamiliar in the math sub fields in which the models are generating proofs.
Computing has the same issue. If we swapped a PLC programer with your average SV software engineer for a week both of them would have a really bad time.