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

arXiv: https://arxiv.org/abs/2607.21187 · HTML: https://mlsanity.com/paper/2607.21187/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 25 references that are in the map.
- First posted on arXiv 23 Jul 2026.

## Builds on (most cited first, 4 of 4)

- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs](https://mlsanity.com/paper/2511.18760/) (2025)
- [Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification](https://mlsanity.com/paper/2504.17017/) (2025)

## Abstract (arXiv)

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.