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

Source: arXiv:2607.21187 · Published 2026-07-23 · By Fred Mesnard, Étienne Payet, Wim Vanhoof

TL;DR

This paper presents a detailed case study integrating a Large Language Model (LLM) with the Logic Program Theorem Prover (LPTP) to formally prove the irrationality of the square root of 2 within a pure logic programming framework. Starting from the classical proof by contradiction, the authors encode the problem in LPTP's natural deduction proof language and partially generate lemmas and proof steps via the LLM Claude (Anthropic's model). They then validate and refine these proofs using LPTP's proof checker. This iterative human-in-the-loop process yields a fully formal, machine-checked proof, including foundational results such as the evenness of numbers and properties of squares, which had to be established from Peano arithmetic encoded in Prolog predicates. Comparisons with automated theorem provers (ATPs) show that while ATPs can prove some lemmas, they struggle with the main theorem and complex lemmas, underscoring complementarity between LLM-guided proof generation and formal proof checking.

The study demonstrates how LPTP, a lightweight, Prolog-based prover with natural deduction proofs, can benefit from an LLM to fill in proof gaps, navigate complex inductive reasoning, and generate auxiliary lemmas in formal logic. The approach leverages LLM capabilities for syntactic and semantic reasoning in a niche formalism but relies critically on proof checking to eliminate hallucinations and ensure correctness. The resulting proof establishes non-rationality of sqrt(2) in a machine-verified manner and concretely shows that proving properties of infinite search spaces (like those in logic programming) is feasible with this hybrid approach. It paves the way for AI-augmented formal verification of logic program properties.

Key findings

• The LLM Claude directly proved 5 out of 10 intermediate lemmas and 9 out of 12 final lemmas in LPTP syntax without human hints.
• Certain challenging lemmas (e.g., evenpp:evenp) required human hints or partial manual proofs, highlighting current LLM limitations in complex inductive proofs.
• Automated theorem provers (Vampire and E) succeeded on 5 of 10 lemmas initially and 9 of 12 in the refined version but failed to prove the main irrationality theorem within 20 seconds timeout.
• The feedback loop using LPTP's ability to identify the first incorrect proof step makes LLM proof generation practical by enabling local corrections.
• The formal proof checker ensured that all machine-generated proofs were verified for logical correctness before library integration, preventing introduction of false axioms.
• The classical proof by contradiction for √2 irrationality was fully formalized, including definition of coprime numbers, evenness, divisors, and square computations in Peano arithmetic encoded in logic programming predicates.
• The integration of an LLM with LPTP is the first known attempt for this prover and shows a pathway for AI-enhanced proof development in logic programming verification.
• Proofs involved detailed inductive schemas and logic program completion semantics, carefully translated into the LPTP specification language.

Threat model

n/a - This is a theorem proving and formal verification study rather than a security paper. The relevant model treats the LLM as an untrusted proof generator whose outputs are verified by the trusted LPTP proof checker, thereby preventing acceptance of incorrect proofs.

Methodology — deep read

1. Threat Model & Assumptions: The work considers theorem proving agents rather than adversaries. The interaction involves human users, an LLM (Claude) without direct deductive soundness guarantees, and the LPTP proof checker which enforces correctness. The LLM cannot introduce accepted false proofs as the checker only validates correct derivations.

2. Data: The mathematical domain is formal logic programs encoding Peano arithmetic, divisibility, gcd, etc., from existing LPTP libraries (nat and gcd). Lemmas and propositions are expressed in the first-order logic based LPTP specification language, with terms like zero (0), successor function s/1, and predicates for arithmetic and parity. No external datasets beyond LPTP libraries were used.

3. Architecture / Algorithm: The process starts from an informal classical proof of irrationality. The authors define key predicates (divisor/2, coprime/2, square/1) within LPTP. Lemmas about arithmetic properties are stated in LPTP's natural deduction style. The LLM is prompted with lemma statements and the LPTP manual/libraries to generate candidate proofs in LPTP syntax. The LPTP proof checker tests these proofs for correctness, either accepting or rejecting partial proofs and reporting the earliest incorrect inference step.

4. Training regime: Not applicable for the LLM (off-the-shelf Anthropic Claude Opus 4.5 and 4.6). The LLM uses in-context learning, ingesting LPTP documentation and two LPTP libraries (Peano numbers and lists) as context. No fine-tuning reported. Hyperparameters use Anthropic's default decoding. Human users direct the order of lemmas to prove and provide hints or manual proofs when the LLM struggles.

5. Evaluation protocol: Each lemma proof generated by the LLM is checked by LPTP for soundness. If rejected, the first error is sent back to the LLM for improved proof generation. This iterative loop continues until the proof checks or is manually completed. Outcomes recorded include direct proofs (DP), back-and-forth proofs (BF), proofs with human hints (PH), or proofs given (PG). Additionally, state-of-the-art ATPs (Vampire, E) are run with 20s timeout on the same lemmas for comparison, though their proof output is incompatible with LPTP proof checking.

6. Reproducibility: The authors release the full data and code of their experiment publicly on GitHub, including LPTP proofs and LLM interaction scripts. The LPTP system is open and well-documented, facilitating experiment reproduction. The LLM model used is proprietary but publicly described.

Technical innovations

• First integration of an LLM (Claude) with the LPTP proof assistant for logic program verification using natural deduction proofs.
• A practical feedback loop employing LPTP’s proof checker to provide pinpointed error localization enabling efficient iterative proof refinement by the LLM.
• Encoding of classical number theory results like √2's irrationality fully within a logic programming framework using Peano arithmetic predicates and formal completion semantics.
• Demonstration of complementarity between off-the-shelf first order ATPs and LLMs, with proof-checkable natural deduction proofs generated only by the latter.
• Use of informal natural language hints alongside formal lemma statements in LPTP syntax to guide LLM proof generation for very difficult lemmas.

Datasets

• LPTP nat and gcd libraries — core logic programming predicates for Peano arithmetic and gcd — publicly available with LPTP.
• LPTP proof scripts and lemma statements for irrationality of sqrt(2) — approximately a dozen lemmas developed in the study — available at https://github.com/FredMesnard/LPTP-LLM.git

Baselines vs proposed

• Automated Theorem Provers (Vampire, E) on main intermediate lemmas: success on 5/10 lemmas initially; 9/12 lemmas in the refined version.
• ATP on main irrationality theorem: failed within 20s timeout.
• LLM Claude directly proved 5/10 lemmas initially and improved to 9/12 lemmas in refined proof without hints.
• LLM Claude with human hints/provided proofs succeeded on the toughest lemma (evenpp:evenp) and full main theorem.
• ATP results whereas fast and reproducible, cannot produce natural deduction proofs usable in LPTP for proof checking.

Limitations

• LLM could not fully generate the hardest lemmas (e.g. evenpp:evenp) without human assistance or detailed hints.
• No adversarial evaluation of robustness of LLM-generated proofs to malicious or random inputs.
• Performance comparison limited to a small classical problem (√2 irrationality), no large-scale benchmark on diverse logic programs.
• The LPTP framework and syntax might be less documented and less widely used than mainstream proof assistants, limiting generalizability.
• Proof search largely manual and guided; fully automated LLM-driven theorem proving remains out of reach.
• Closed proprietary nature of the LLM (Claude Opus) limits open-source replicability.

Open questions / follow-ons

• Can the approach be scaled to more complex logic programming properties beyond classical number theory proofs?
• How well do other LLMs (e.g., GPT-4 or open models) perform in generating LPTP proofs for similar problems?
• Can tighter integration reduce human intervention, enabling fully automated LPTP/LLM theorem proving loops?
• How can proof reconstruction be improved for resolution-style proofs from ATPs to integrate them formally into LPTP?

Why it matters for bot defense

For bot-defense and CAPTCHA researchers, this study illustrates a promising paradigm for combining large language models with lightweight, formal proof checkers to verify correctness of logic programs and predicates. Analogously, CAPTCHA and bot defense systems use logical and behavioral predicates that require robust verification mechanisms. Using LLMs to generate candidate verification schemas or behavioral rules combined with strict proof checking could enable adaptive, formally-verified bot detection logic. Furthermore, the methodology of iterative feedback between an LLM and a proof checker provides a model for refining heuristic bot detection modules that must satisfy logical consistency guarantees. While the domain here is pure mathematics formalization, the principles apply broadly to logic-based verification tasks in security-sensitive environments like CAPTCHA or bot-defense logic analysis.

Cite

@article{arxiv2607_21187,
  title={ Case study: proving sqrt(2) irrational with LPTP and an LLM },
  author={ Fred Mesnard and Étienne Payet and Wim Vanhoof },
  journal={arXiv preprint arXiv:2607.21187},
  year={ 2026 },
  url={https://arxiv.org/abs/2607.21187}
}

Read the full paper

• arXiv:2607.21187 (abstract)
• arXiv:2607.21187 (PDF)