Case study: proving √2 irrational with LPTP and an LLM

Proving mathematical properties within a logic programming (LP) context often involves infinite search spaces, making standard resolution-based engines like Prolog insufficient for proving negative results such as the irrationality of the square root of 2. To address this, the authors utilize the Logic Program Theorem Prover (LPTP), a system based on natural deduction that allows for formal verification of logic programs. The study investigates whether an LLM can assist in constructing these formal proofs by acting as a partner in an interactive feedback loop.

The researchers established a collaborative workflow between the human developer and the LLM. The process began with the human defining the high-level proof skeleton in LPTP syntax. For the required auxiliary lemmas, the LLM was tasked with generating formal proofs. When the LPTP proof checker identified an error, the specific incorrect derivation step was fed back to the LLM, which then attempted to correct its reasoning. This iterative process continued until the proof was either accepted by the system, or the human provided additional hints or the proof itself when the model failed to converge.

The authors demonstrated that an LLM can effectively navigate the formal requirements of LPTP, successfully generating proofs for most of the required lemmas. While some complex lemmas required human intervention or hints, the LLM proved capable of handling the majority of the proof construction, including correcting its own errors based on feedback from the formal checker. This case study highlights the potential for LLMs to lower the barrier to entry for formal verification by automating the tedious aspects of proof construction while relying on a rigorous, machine-checked foundation.