Case study: proving sqrt(2) irrational with LPTP and an LLM

Abstract: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.

In Proceedings ICLP 2026, arXiv:2607.17707

Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Symbolic Computation (cs.SC)

arXiv:2607.21187 [cs.LO]

(or arXiv:2607.21187v1 [cs.LO] for this version)

https://doi.org/10.48550/arXiv.2607.21187 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

EPTCS 450, 2026, pp. 67-80

https://doi.org/10.4204/EPTCS.450.5 Focus to learn more DOI(s) linking to related resources

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.