As an applied probabilist, you often want to focus on the bigger proof strategy, but end up spending a lot of time with annoying integral computations and long

As an applied probabilist, you often want to focus on the bigger proof strategy, but end up spending a lot of time with annoying integral computations and long strings of basic manipulations. For example, "compute an integral transform of X", "apply method A to get an asymptotic series expansion of Y", or "derive a concentration inequality for Z". I've found that it is often much faster to get e.g. o3-mini-high to do these first to verify if the answer might help in your proof, like a broader CAS replacement. Then you can go through the working yourself later once the strategy is clear; clean it up, make it rigorous, etc. Overall, this saves me a fair bit of time. Many still seem to believe that these models are completely unreliable for these sorts of arguments, but I've found the error rate to be around 10% per prompt, about on par with a good student. You get good at checking whether the argument is on track or not, so you can just rewrite the prompt a few times with more detail until a solution looks decent. I've never had much success with the types of prompts you describe, and I find comfort in knowing that these LLMs seem (at least at present) unable to solve broader research questions. Often, you need to give much more direct questions in the style of textbook questions so it doesn't get too "creative" or "lazy".