Case Study: Proving √2 Irrational with LPTP and an LLM

This case study examines how an LLM can assist with a formal proof that the square root of 2 is irrational in the Logic Program Theorem Prover (LPTP). The authors define several basic pure logic-programming predicates, sketch the classical proof in LPTP’s natural-deduction-based proof language, and document their interactions with the LLM. The reported outcome is a complete formal proof that was partially generated by the model and fully proof-checked by LPTP, providing a small but concrete example of LLM assistance in logic-program theorem proving.