Case study: solving P-99 with LPTP and an LLM | Fred Mesnard et al. | ResearchPod