Case study: proving sqrt(2) irrational with LPTP and an LLM | Digital Library | PAMCET | PAMCET