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

2026/07/20 by Fred Mesnard, Étienne Payet, Wim Vanhoof
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic

paper · pdf · doi:10.4204/eptcs.450.5

Abstract

We present the interactions with an LLM (Large Language Model) aiming at proving that √ 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 written by Robert Stärk 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 √ 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.

Related

• Can Large Language Models put 2 and 2 together? Probing for Entailed Arithmetical Relationships
• Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs
• Case study: solving P-99 with LPTP and an LLM
• From Blind Solvers to Logical Thinkers: Benchmarking LLMs' Logical Integrity on Faulty Mathematical Problems
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning