Search papers, labs, and topics across Lattice.
This study explores the use of a Large Language Model (LLM) in conjunction with the Logic Program Theorem Prover (LPTP) to formally prove the irrationality of the square root of 2. By leveraging basic logic programming predicates and the natural deduction framework of LPTP, the authors illustrate how the LLM can assist in generating human-readable proofs. The key result is a complete formal proof that integrates LLM-generated content with rigorous verification by LPTP, showcasing a novel collaboration between AI and formal logic systems.
A collaboration between an LLM and a formal theorem prover yields a complete, human-readable proof of the irrationality of sqrt(2).
We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of the square root of 2. Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.
