Paper deep dive
Case study: proving sqrt(2) irrational with LPTP and an LLM
Fred Mesnard, Étienne Payet, Wim Vanhoof
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 7/24/2026, 2:45:47 AM
Summary
This paper presents a case study on proving the irrationality of the square root of 2 using the Logic Program Theorem Prover (LPTP) in conjunction with a Large Language Model (LLM). The authors formalize the proof in LPTP, which uses a specification language based on first-order logic and natural deduction. They interact with an LLM (specifically Claude Opus 4.5) to generate and verify lemmas required for the main proof. The process involves a feedback loop where the LLM generates proofs, LPTP checks them, and errors are fed back to the LLM for correction. The study demonstrates that LLMs can effectively assist in constructing formal proofs within a Logic Programming context, although some lemmas required human hints or direct proof generation.
Entities (12)
Relation Signals (8)
Wim Vanhoof → affiliatedwith → Université de Namur
confidence 95% · Wim Vanhoof Université de Namur, Belgium
Fred Mesnard → affiliatedwith → Université de La Réunion
confidence 95% · Fred MesnardÉtienne Payet LIM, université de La Réunion, France
Étienne Payet → affiliatedwith → Université de La Réunion
confidence 95% · Fred MesnardÉtienne Payet LIM, université de La Réunion, France
sqrt2:irrational → provenby → LPTP and LLM
confidence 95% · We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.
Claude Opus 4.5 → usedfor → Proof Generation
confidence 92% · We choose Claude from Anthropic and do the experiment with Opus 4.5... to construct proofs validated with the LPTP proof checker.
LPTP → createdby → Robert Stärk
confidence 90% · We rely on the LPTP (Logic Program Theorem Prover) system written by Robert Stärk
LPTP → validates → Claude Opus 4.5 Proofs
confidence 90% · We feed its proof to the LPTP proof checker, and on failure forward to Claude the firstincorrect derivation stepreported by LPTP.
evenpp:evenp → requiredhintfor → Claude Opus 4.5
confidence 85% · Claude failed to find a proof or even go in the right direction. So we derived the main steps by hand and then asked Claude to prove all auxiliary lemmas stated in natural language.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2607.21187v1
- Canonical: https://arxiv.org/abs/2607.21187v1
Trouble viewing inline? Open PDF directly →
Full Text
38,886 characters extracted from source content.
Expand or collapse full text
W. Faber, L. Giordano, R. Rocha, V. Santos Costa (Eds.): 42nd International Conference on Logic Programming (ICLP 2026) EPTCS 450, 2026, p. 67–80, doi:10.4204/EPTCS.450.5 © F. Mesnard, É. Payet, W. Vanhoof This work is licensed under the Creative Commons Attribution License. Case study: proving √ 2irrational with LPTP and an LLM Fred MesnardÉtienne Payet LIM, université de La Réunion, France frederic.mesnard,etienne.payet@univ-reunion.fr Wim Vanhoof Université de Namur, Belgium wim.vanhoof@unamur.be 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 lan- guage 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. 1 Introduction Consider the following pure Prolog program. Natural numbers are represented as terms built from the constant 0 and the function symbols/1. We borrow the predicatesnat/1,plus/3,times/3,gcd/3, andgcd_leq/3from the LPTP (Logic Program Theorem Prover, [20]) librariesnatandgcdto facilitate the future use of already proven properties. even(0). odd(s(0)). even(s(s(X))) :- even(X). odd(s(s(X))) :- odd(X). nat(0). leq(0,X). nat(s(X)) :- nat(X). leq(s(X),s(Y)) :- leq(X,Y). plus(0,Y,Y). times(0,Y,0). plus(s(X),Y,s(Z)) :- plus(X,Y,Z). times(s(X),Y,Z) :- times(X,Y,P), plus(P,Y,Z). gcd(X,Y,D) :- gcd_leq(X,Y,D) :- ( leq(X,Y) -> gcd_leq(X,Y,D) ( X = 0 -> D = Y ; gcd_leq(Y,X,D)). ; plus(X,Z,Y), gcd(X,Z,D)). Question:can we find two coprime natural numberspandqsuch that p q = √ 2,i.e.,p 2 =2q 2 ? (Two natural numberspandqarecoprimeif and only if their greatest common divisor is 1.) This ques- tion corresponds to the following Prolog query, designed so that backtracking generates a fair exploration ofN×N, whereNdenotes the set of natural numbers: ?- nat(S),plus(P,Q,S),gcd(P,Q,s(0)),times(P,P,P2),times(Q,Q,Q2),plus(Q2,Q2,P2). The answer to the question isno. This fact is known since at least the 6th century BC. But since the search space of the above query is infinite, we won’t get a negative answer fromanyresolution-based logic programming (LP) engine, Prolog included. However we can prove this fact by other means, still 68Case study: proving √ 2irrational with LPTP and an LLM within an LP context. For instance, we can prove √ 2 is not rational using the LPTP system. We take profit of this exercise to evaluate the help we may get from an LLM (Large Language Model). Recent research has shown that LLMs can be made increasingly effective at automated theorem proving by integrating them with formal provers and proof checkers (see,e.g., [11, 17]). To the best of our knowledge, no such integration has been attempted for LPTP. Yet, LPTP is an interesting formalism and tool as it uses Prolog as representation language, and the associated prover constitutes a rather lightweight and easily manipulable process. The theoretical basis and specification language is purely first-order logic, which is well-known and largely automatable. On the other hand, less documentation and examples might be available in comparison with other provers (such as Rocq, Lean and Isabelle), which might make it more difficult for an LLM to appropriate the formalism. The paper is organized as follows. Section 2 recalls the basics of LPTP. Section 3 presents a usual proof of the irrationality of √ 2 and a formalization of its skeleton. Section 4 and 5 explain how we interact with the LLM to get a complete proof. Section 6 reviews some related work, and Section 7 concludes. 2 A quick summary of LPTP The reader already familiar with LPTP can safely skip this section. LetPbe a pure logic program where negative literals may appear in the body of clauses (also callednormal programin [10]). For sake of conciseness, we do not consider built-in predicates (see [20] for a full treatment) other than the equality =/2. We start withL, the first-order language associated toP. ThegoalsofLare: G,H::=true|fail|s=t|A|\+G|(G,H)|(G;H)|somex G wheresandtare two terms,xis a variable andAis an atomic goal. The goals ofLhave the operational semantics specified by ISO-Prolog [7] assuming the occurs check. ˆ Lis the specification language of LPTP. For each user-defined predicate symbolR, ˆ Ldoes not includeR, but instead it contains three predicate symbolsR s ,R f ,R t of the same arity asR, which respec- tively express success, failure and termination ofR. ˆ Lalso contains a unary constraint for groundness gr, expressing that its argument is ground. Theformulasof ˆ Lare: φ,ψ::=⊤|⊥|s=t|R( #» t)|¬φ|φ∧ψ|φ∨ψ|φ→ψ|∀xφ|∃xφ where #» tis a sequence ofnterms andRdenotes an-ary predicate symbol of ˆ L. The semantics of ˆ Lis the first-order predicate calculus of classical logic. For any of the user-defined logic proceduresRin a logic programP,D P R ( #» x)denotes its Clark’s if-and-only-ifcompleted definition, c.f. [2, 10]. For defining the declarative semantics of logic programs, Stärk uses three syntactic operatorsS,F andTwhich map goals ofLinto ˆ L-formulas. Intuitively,SGmeansGsucceeds (any breadth-first evaluation ofGsucceeds),FGmeansGfails (the ISO-Prolog evaluation stops without any answer), and TGmeansGterminates (the ISO-Prolog evaluation produces a finite number of answers then stops). Moreover, termination implies a safe use of negation. The definition of the operators follows: SR( #» t):=R s ( #» t)Strue:=⊤Sfail:=⊥S(s=t):= (s=t) S\+G:=FGS(G,H):=SG∧SHS(G;H):=SG∨SHS(somex G):=∃xSG FR( #» t):=R f ( #» t)Ftrue:=⊥Ffail:=⊤F(s=t):=¬(s=t) F\+G:=SGF(G,H):=FG∨FHF(G;H):=FG∧FHF(somex G):=∀xFG F. Mesnard, É. Payet, W. Vanhoof69 TR( #» t):=R t ( #» t)Ttrue:=⊤ Tfail:=⊤T(s=t):=⊤ T\+G:=TG∧gr(G)T(G,H):=TG∧(FG∨TH) T(G;H):=TG∧THT(somex G):=∀xTG With LPTP, we prove properties of a logic programPw.r.t. itsinductive extensionIND(P) which includes Clark’s completion [2] and induction along the definition of the predicates. Stärk shows that the inductive extension is always consistent and proves various correctness and completeness results w.r.t. the operational semantics of Prolog [20]. The first-order theory IND(P) (cf. [20], p. 253–254) is defined by nine axiom schemas which we describe now. We omit the fixed point axioms for builtins. Let us point out that the specification language ˆ Lof LPTP can be extended by new function and predicate symbols, which can be quite handy while formalizing properties. The first two axioms specify some properties of the trees built from the function symbols extracted from the program under consideration. The third axiom forbids infinite trees. The axioms of Clark’s equality theory 1.f(x 1 ,...,x n ) =f(y 1 ,...,y n )→x i =y i [iffisn-ary and 1≤i≤n] 2.f(x 1 ,...,x n )̸=g(y 1 ,...,y m )[ifn̸=morf̸≡g] 3.t̸=x[ifxoccurs intandt̸≡x] LPTP deals withnon-groundterms, as any ISO-Prolog processor does. LPTP offers a predefined predicategr/1 that we can consider as a constraint. This relation is useful for instance for dealing with negation as failure as LPTP only allows negation by failure forgroundgoals (see the definitionT\+G). Axioms for gr/1 4. gr(c) [ifcis a constant] 5. gr(x 1 )∧...∧gr(x m )↔gr(f(x 1 ,...,x m ))[fism-ary] LPTP considers each user-defined predicate through three points of view: failure, success and termi- nation. These three viewpoints are linked with the following axioms. Uniqueness axioms and totality axioms 6.¬(R s ( #» x)∧R f ( #» x))[ifRis a user-defined predicate] 7.R t ( #» x)→(R s ( #» x)∨R f ( #» x))[ifRis a user-defined predicate] Axiom 6 says that for any tuple of (possibly non-ground) terms, we cannot have at the same time success and failure ofR. Axiom 7 states that given termination, we have success or failure. Altogether, it means that for any tuple of terms #» x, assuming termination, eitherR( #» x)succeeds or (exclusively)R( #» x) fails. Fixed point axioms for user-defined predicatesR 8.R s ( #» x)↔SD P R ( #» x),R f ( #» x)↔FD P R ( #» x),R t ( #» x)↔TD P R ( #» x) 70Case study: proving √ 2irrational with LPTP and an LLM We recall thatD P R ( #» x)denotes the definition of the completion [2] of the user-defined procedureR( #» x) in the logic programP. In the previous section, we saw how to apply the operatorS,FandTto formulas. So for instance, the first equivalenceR s ( #» x)↔SD P R ( #» x)definesR s ( #» x). Finally, for any property of the form∀ #» x[R s ( #» x)→φ( #» x)], whereR( #» x)is a user-defined procedure andφ( #» x)an ˆ L-formula, we have an induction schema. The interactive prover LPTP is able todynam- icallygenerate an induction axiom on demand while the user interacts with it. Let us examine a simple case. It is exactly what happens using LPTP, which slightly generalizes [20]. Bydirectly recursive user- defined predicatein the box below, we forbid mutual recursive definitions. Of course, LPTP is able to handle mutually recursive properties, see [18] for some examples. A (simplified) induction schema for a user-defined predicateR LetRbe a directly recursive user-defined predicate and letφ( #» x)be an ˆ L-formula such that the length of #» xis equal to the arity ofR. Letsub(φ( #» x)/R)be the formula to be proven∀ #» x(R s ( #» x)→φ( #» x)). Letclosed(φ( #» x)/R)be the formula obtained from∀ #» x(SD P R ( #» x)→R s ( #» x))by replacing •R s ( #» x)byφ( #» x)on the right of→, • all occurrences ofR s ( #» t)appearing on the left of→byφ( #» t)∧R s ( #» t)(these are the recur- sive calls ofRinD P R , turned intoR s by the operatorS). Then the induction axiom is the following formula: 9.closed(φ( #» x)/R)→sub(φ( #» x)/R) As an illustration, consider the lemma∀x(even s (x)→odd s (s(x))), which we will use in section 4 (lemmaeven:succ:odd). We have #» x=x,R≡evenandφ(x)≡odd s (s(x))andsub(φ(x)/R)is precisely lemmaeven:succ:odd. Now forclosed(φ(x)/R), recall the clauses definingevenandodd:even(0), even(s(s(X))) :- even(X),odd(s(0))andodd(s(s(X))) :- odd(X). The Clark completion of evenisD P even (x)≡x=0∨∃y(x=s(s(y))∧even(y)), and applying the operatorSgivesSD P even (x)≡ x=0∨∃y(x=s(s(y))∧even s (y)). After the two substitutions (even s (x)⇝φ(x)on the right and even s (y)⇝φ(y)∧even s (y)on the left), we get:closed(φ(x)/even) =∀x h x=0∨∃y(x=s(s(y))∧ φ(y)∧even s (y)) →φ(x) i . Let us simplify this formula using three standard equivalences of first-order logic: (a)∀x[(A∨B)→C]≡ ∀x(A→C)∧ ∀x(B→C); (b)∀x(x=t→ψ(x))≡ψ(t)(whenx is not free int); (c)∀x[∃y P(x,y)→Q(x)]≡ ∀x∀y[P(x,y)→Q(x)](whenyis not free inQ). Ap- plying (a) splitsclosed(φ(x)/even)into two conjuncts. The first one,∀x(x=0→φ(x)), reduces to φ(0)by (b). The second one,∀x[∃y(x=s(s(y))∧φ(y)∧even s (y))→φ(x)], becomes after extrac- tion of the existential by (c) and elimination ofxby (b) (usingx=s(s(y))):∀y[φ(y)∧even s (y)→ φ(s(s(y)))]. Renamingytoxand combining withsub(φ(x)/even) =∀x(even s (x)→φ(x)), the induction axiomclosed(φ(x)/even)→sub(φ(x)/even)instantiates to: odd s (s(0))∧∀x odd s (s(x))∧even s (x)→ odd s (s(s(s(x)))) → ∀x even s (x)→odd s (s(x)) . We refer the reader to the papers of Stärk [20, 19, 18] for a complete presentation of LPTP. F. Mesnard, É. Payet, W. Vanhoof71 3 Our initial draft Let us go back to our introductory example. The informal reasoning proving the irrationality of √ 2 that we start with is the following usual proof by contradiction. Assume we have two coprime natural numberspandqsuch that p 2 =2q 2 Sop 2 is even. Hencepis even, because the square of an odd number is odd. Thus there exists a natural numberrsuch thatp=2r. By replacingpwith 2rin the main equation, we get 4r 2 =2q 2 , which gives 2r 2 =q 2 . Henceqis also even, which contradicts our assumption. We formalize the above reasoning by first introducing the logical relationsdivisor/2 (which we get from the LPTP library) andcoprime/2. We also define the logical functionsquare/1 which returns the square of its argument. Before defining a function, we must show that the associated definition (heren7→psuch thattimes(n,n,p)holds) is actually functional: for anynat(n), there exists a unique pverifyingtimes(n,n,p). So we need to prove existence and uniqueness, as done below. For proving these two properties, we rely on lemmatimes:existenceand lemmatimes:uniqueness, already proven in the LPTP librarynat. Definition[divisor/2]∀x,y(divisor(x,y)↔∃z(Snat(z)∧x∗z=y)). Definition[coprime/2]∀p,q(coprime(p,q)↔∀r(Snat(r)∧divisor(r,p)∧divisor(r,q)→r=s(0))). Lemma[square:existence]∀n(Snat(n)→∃pStimes(n,n,p)).Proof. Assumption 0 :Snat(n).Snat(n)∧Snat(n).∃zStimes(n,n,z)by Lemma times:existence [times:existence]. Thus 0 :Snat(n)→∃pStimes(n,n,p).⊔⊓ Lemma[square:uniqueness]∀n,sn,s p(Stimes(n,n,sn)∧Stimes(n,n,s p)→sn=s p).Proof. Assumption 0 :Stimes(n,n,sn)∧Stimes(n,n,s p).sn=s pby Lemma times:uniqueness [times:uniqueness]. Thus 0 :Stimes(n,n,sn)∧Stimes(n,n,s p)→sn=s p.⊔⊓ Definition[square/1]∀n,p(Snat(n)→(square(n) =p↔Stimes(n,n,p))). Now we proceed top-down, starting from the informal proof which we translate in LPTP as our main theorem. We also need auxiliary results, and we ask to the proof checker to admit them by using the LPTP tacticby gap. The proof checker validates the whole proof skeleton and produces a T E Xfile. Here is its PDF rendering. 72Case study: proving √ 2irrational with LPTP and an LLM Theorem[sqrt2:irrational]∀p,q(Snat(p)∧Snat(q)∧coprime(p,q)→ ¬square(p) =s(s(0))∗square(q)).Proof. Assumption 0 :Snat(p)∧Snat(q)∧coprime(p,q). Contra 1 :square(p) =s(s(0))∗square(q).Seven(square(p))byGAP.Seven(p)byGAP. ∃r(Snat(r)∧p=s(s(0))∗r)byGAP. Let 2 rwithSnat(r)∧p=s(s(0))∗r.square(p) =square(s(s(0)))∗square(r)byGAP. s(s(s(s(0))))∗square(r) =s(s(0))∗square(q)byGAP.s(s(0))∗square(r) =square(q) byGAP.Seven(q)byGAP. Thus 2 :Seven(q).divisor(s(s(0)),q)byGAP.divisor(s(s(0)),p)byGAP. Snat(s(s(0))).coprime(p,q).∀r(Snat(r)∧divisor(r,p)∧divisor(r,q)→r=s(0))by Definition coprime/2 [coprime/2].Snat(s(s(0)))∧divisor(s(s(0)),p)∧divisor(s(s(0)),q)→ s(s(0)) =s(0).s(s(0)) =s(0).⊥. Thus 1 :¬square(p) =s(s(0))∗square(q).¬square(p) =s(s(0))∗square(q). Thus 0 :Snat(p)∧Snat(q)∧coprime(p,q)→¬square(p) =s(s(0))∗square(q).⊔⊓ Then we refine the previous attempt. We define the properties we need for proving the main theorem bystatingthese auxiliary properties. We do not proveanyof these properties for the moment. For each proof, we just write:⊥(i.e.,false) is admitted (byGAP). As from⊥everything is true, each property holds. This pseudo proof appears for the first lemma and is omitted for the others. Lemma[nat:natsquare]∀n(Snat(n)→Snat(square(n))).Proof.⊥byGAP.⊔⊓ Lemma[twotimes:even]∀n,p(Snat(p)∧s(s(0))∗p=n→Seven(n)). Lemma[evenpp:evenp]∀p(Seven(square(p))→Seven(p)). Lemma[even:twotimes]∀n(Seven(n)→∃p(Snat(p)∧n=s(s(0))∗p)). Lemma[npq:nnppqq]∀n,p,q(n=p∗q→square(n) =square(p)∗square(q)). Lemma[sqr2:4]square(s(s(0))) =s(s(s(s(0)))). Lemma[simplify:by2]∀n,p(s(s(s(s(0))))∗n=s(s(0))∗p→s(s(0))∗n=p). Lemma[even:div2]∀n(Seven(n)→divisor(s(s(0)),n)). Assuming for the moment that these properties are true, here is the new version of the main theorem. It mimics the informal proof we started with, but with a bit more details so that there is no gap. Gaps now only appear in the lemmas. The file is proof-checked. F. Mesnard, É. Payet, W. Vanhoof73 Theorem[sqrt2:irrational]∀p,q(Snat(p)∧Snat(q)∧coprime(p,q)→ ¬square(p) =s(s(0))∗square(q)).Proof. Assumption 0 :Snat(p)∧Snat(q)∧coprime(p,q). Contra 1 :square(p) =s(s(0))∗square(q).Snat(square(q))by Lemma nat:natsquare [nat:natsquare].s(s(0))∗square(q) =square(p).Seven(square(p))by Lemma twotimes:even [twotimes:even].Seven(p)by Lemma evenpp:evenp [evenpp:evenp]. ∃r(Snat(r)∧p=s(s(0))∗r)by Lemma even:twotimes [even:twotimes]. Let 2 rwithSnat(r)∧p=s(s(0))∗r.square(p) =square(s(s(0)))∗square(r) by Lemma npq:nnppqq [npq:nnppqq].square(s(s(0))) =s(s(s(s(0)))) by Lemma sqr2:4 [sqr2:4].square(p) =s(s(s(s(0))))∗square(r). s(s(s(s(0))))∗square(r) =s(s(0))∗square(q).s(s(0))∗square(r) =square(q)by Lemma simplify:by2 [simplify:by2].Snat(square(r))by Lemma nat:natsquare [nat:natsquare]. Seven(square(q))by Lemma twotimes:even [twotimes:even]. Seven(q)by Lemma evenpp:evenp [evenpp:evenp]. Thus 2 :Seven(q).divisor(s(s(0)),q)by Lemma even:div2 [even:div2]. divisor(s(s(0)),p)by Lemma even:div2 [even:div2].Snat(s(s(0))).coprime(p,q). ∀r(Snat(r)∧divisor(r,p)∧divisor(r,q)→r=s(0))by Definition coprime/2 [coprime/2]. Snat(s(s(0)))∧divisor(s(s(0)),p)∧divisor(s(s(0)),q)→s(s(0)) =s(0).s(s(0)) =s(0).⊥. Thus 1 :¬square(p) =s(s(0))∗square(q).¬square(p) =s(s(0))∗square(q). Thus 0 :Snat(p)∧Snat(q)∧coprime(p,q)→¬square(p) =s(s(0))∗square(q).⊔⊓ For each lemma, an LPTP warning is reported:there is a gap in the proof.But our initial draft is syntactically and logically coherent. Moreover, the level of granularity seems reasonable, at least for us. We moved from the informal usual high-level proof of the beginning of this section to the LPTP equivalent of the low-level Peano axioms. Note that even the most elementary pieces (like 2 2 =4) of the above reasoning have to be proven (see Lemmasqr2:4). Let us ask for help for proving these lemmas by invoking an LLM. 4 The proof completed We choose Claude from Anthropic and do the experiment with Opus 4.5, the most powerful large lan- guage model released by Anthropic in late 2025. As this model is well known for its efficiency in programming tasks, we expect it to be able to construct proofs validated with the LPTP proof checker. We did not try any cheaper model (but we also run resolution-based automated theorem provers). All interactions used Anthropic’s default decoding settings (no temperature or sampling tuning). We per- formin-context learning,i.e., we feed the LLM with the LPTP user manual in PDF format. We also give Claude two basic LPTP libraries (Prolog code and LPTP proofs in text format), one for Peano numbers and the other one about lists. The code and library of properties for Peano numbers will be used in the proofs generated by Claude. On the other hand, the code and properties for lists will not be directly used but give many other proof examples to Claude. Our interaction follows a simple feedback loop: we submit a lemma (most often in LPTP syntax, sometimes in natural language) to Claude, feed its proof to the LPTP proof checker, and on failure forward to Claude the firstincorrect derivation stepreported by LPTP. We iterate until either LPTP accepts the proof (DP or BF in the tables below) or we estimate that Claude is not converging, in which case we provide a natural-language hint (PH) or the proof itself (PG). The human developer is 74Case study: proving √ 2irrational with LPTP and an LLM responsible for choosing the order in which lemmas are attempted and for deciding when to abandon a back-and-forth. The ability of LPTP to localize the first incorrect step is what makes this loop tractable in practice. So we start by asking the proofs of the easiest (from our point of view) lemmas, one lemma after the other. We state the lemmas formally using the LPTP syntax. The proofs of lemmasnat:natsquare (informally:nat(n)→nat(n 2 )),sqr2:4(2 2 =4),twotimes:even(n=2p→even(n)),even:twotimes (even(n)→n=2p)), andeven:div2(even(n)→2|n) are proposed by Claude and accepted by the proof checker of LPTP. For instance, our prompt for lemmasqr2:4reads: Donne-moi une preuve LPTP de : :- lemma(sqr2:4, square(s(s(0))) = s(s(s(s(0)))), f by gap). mixing a brief French instruction with the formal LPTP statement, theff by gapclause being the placeholder to be filled in. With each of its proofs, Claude summarizes in natural language the idea of the proof. For lemmasqr2:4, Claude explains that it first shows that 0, 1 and 2 are natural numbers. Then it computestimes(2,2,4)step by step: we havetimes(0,2,0),plus(2,0,2)hencetimes(1,2,2). We also haveplus(2,2,4)hencetimes(2,2,4). Finally, we getsquare(2) =4. The proofs oftwotimes:even(2p=n→even(n)) and its reciprocaleven:twotimesrely heavily on results from thenatlibrary given to Claude initially, which it uses adequately. For the lemmasimplify:by2(4n=2p→2n=p), we have to handle a few back and forths between Claude and LPTP. The proof checker detects someincorrect derivation stepsat some places in the gener- ated proof. Each time, Claude analyzes the error and proposes a new proof. Claude proposed and proved the auxiliary lemmatimes:injective:second. Finally, Claude was able to correct all the errors. We observe a similar behaviour for the lemmanpq:nnppqq(n=pq→n 2 =p 2 q 2 ). Table 1 gives our obtained results and Figure 1 shows the dependency graph of the proof. We also add a column ATP for recording the answers we get from running two automated theorem provers on the same lemmas within a 20 seconds timeout. This approach is fully described in [12] and summarized in the next section. nat:natsquare twotimes:even sqr2:4times:injective:second even:twotimes evenpp:evenp npq:nnppqq simplify:by2 even:div2 sqrt2:irrational Figure 1: Dependency graph of the lemmas of Table 1. An arrowA→BmeansAis used in the proof of B. The last remaining property,evenpp:evenp(even(p 2 )→even(p)), proved much trickier: Claude failed to find a proof or even go in the right direction. So we derived the main steps by hand and then asked Claude to prove all auxiliary lemmas stated in natural language. Finally we ask Claude to prove the lemmaevenpp:evenp(nat(p)∧even(p 2 )→even(p)) using the following hint. F. Mesnard, É. Payet, W. Vanhoof75 Lemma or theoremShorthandLLMATP nat:natsquarenat(n)→nat(square(n))DPyes twotimes:evennat(p)∧2×p=n→even(n)DPno evenpp:evenpeven(square(p))→even(p)NPno even:twotimeseven(n)→∃p:nat(p)∧n=2×pDPno npq:nnppqq n=p×q→ BFno square(n) =square(p)×square(q) sqr2:4square(2) =4DPyes times:injective:second(n+1)×p= (n+1)×q→p=qDPyes simplify:by24×n=2×p→2×n=pBFno even:div2even(n)→divisor(2,n)DPyes sqrt2:irrational nat(p)∧nat(q)∧coprime(p,q)→ PGyes ¬square(p) =2×square(q) Table 1: Summary of the obtained proof results. Shorthands for the column LLM: DP: directly proven by Claude, NP: not proven by Claude, BF: proven by Claude with back and forths, and PG: proof was given to Claude. Ayesin the ATP column means a proof was found by one of our two provers. Lemma or theoremShorthandLLMATP even:succ:oddeven(p)→odd(p+1)DPyes odd:succ:evenodd(p)→even(p+1)DPyes nat:even:disj:oddnat(p)→even(p)∨odd(p)DPyes odd:negation:evenodd(n)→even(n)failsDPyes even:typeseven(n)→nat(n)DPyes odd:typesodd(n)→nat(n)DPyes odd:plus:oddodd(m)∧odd(n)→even(m+n)DPno even:plus:oddeven(m)∧odd(n)→odd(m+n)DPyes odd:times:oddodd(m)∧odd(n)→odd(m×n)DPno odd:square:oddnat(p)∧odd(p)→odd(p 2 )DPyes evenpp:evenpnat(p)∧even(square(p))→even(p)PHyes sqrt2:irrational nat(p)∧nat(q)∧coprime(p,q)→ PGno ¬square(p) =2×square(q) Table 2: Summary of the obtained proof results for auxiliary lemmas: DP: directly proven by Claude, PH: proven by Claude with given hints, and PG: proof was given to Claude 76Case study: proving √ 2irrational with LPTP and an LLM even:succ:oddodd:succ:even even:types odd:typesodd:negation:even nat:even:disj:oddodd:plus:oddeven:plus:odd odd:times:odd odd:square:odd evenpp:evenp Figure 2: Dependency graph of the auxiliary lemmas of Table 2. An arrowA→BmeansAis used in the proof ofB. Eitherpis even or odd. Ifpis even, we are done. Otherwisepis odd sop 2 is odd, hence even(p 2 )is false. Thusnat(p)∧even(p 2 )is false and the implication is true. So in all cases, the implication is true. Claude generates the proof following our suggestion. Finally LPTP validates the whole proof file. Note that the ATPs were not able to prove the main theorem, contrary to the previous experiment. It is likely that they need more time to deal with a larger search space due to the increased number of lemmas. Table 2 presents the results and Figure 2 shows the dependency graph of the proof. 5 Back to Prolog We now have an LPTP proof that √ 2 is irrational. So on a conceptual level, we know that solving the Prolog query of Section 1 is hopeless. Within the LPTP framework, let’s take a closer look by first introducing the Prolog rule: sqrt2_is_rational :- nat(S),plus(P,Q,S),gcd(P,Q,s(0)),times(P,P,P2),times(Q,Q,Q2),plus(Q2,Q2,P2). In the meantime, Opus 4.6 is out (released early February 2026), and we switch to this new version inCode mode. We give Claude access to thefull Prolog codeof LPTP. Contrary to theChat mode, Claude is able to call the proof checker itself, and we allow this capability. We want to prove an op- erational property of our Prolog code, so we create aCLAUDE.mdfile containing the followingProblem specification: The predicate ‘sqrt2_is_rational/0’ is defined in ‘sqrt2.pl’. This file also uses predicates from the files ‘nat.pl’ and ‘gcd.pl’ present in the directory. The file ‘sqrt2_v2_no_gap.pr’ contains a valid LPTP proof that the square root of 2 is not a rational. This proof should help to prove with LPTP that the query ‘?- sqrt2_is_rational.’ does not succeed. F. Mesnard, É. Payet, W. Vanhoof77 Furthermore, we point out that a bridge is needed between the logical definition ofcoprime(p,q) used in the hypothesis of Theorem [sqrt2:irrational] and the conditiongcd(P,Q,s(0))appearing in the clause above (actually, the conditions are equivalent). Claude presents a first plan. Initially it wants to prove thatfails sqrt2_is_rational. We explain that, as termination ofsqrt2_is_rationalcan not be established, we do not have the usual dichotomy betweensuccessandfailure(Axiom 7 of Section 2). The best we can hope is a proof of¬succeeds sqrt2_is_rational(Axiom 6). As Claude has access to the Prolog code of LPTP, it does use this access to have a better understanding of the LPTP syntax and of the LPTP proof checking process. Claude is able to generate three bridging lemmas and to prove that sqrt2_is_rationalcan not succeed by contradiction. 6 Related Work There are a few Prolog verification frameworks, see,e.g., [1, 3, 5, 15] and more recently [4]. Most of them aim atpaper-and-pencilproofs and do not provide any implemented proof checker. Of course, as the most recent paper was published ten years ago, none of these papers reports any form of interaction with an LLM. A comparison of seventeen proof assistants used in formal mathematics is provided in [24] through their formalization of a proof of the irrationality of √ 2. A proof in each system is presented, highlight- ing differences in logical foundations, syntax, automation, and usability. The main goal of the book is to illustrate the diversity of formal reasoning systems and to evaluate the state of proof assistant tech- nology in the early 2000s. The included systems satisfy two criteria: they are designed, or used, for the formalization of mathematics and they are better, in at least one dimension, than all other systems in the collection. We note that LPTP is not considered. This work, published 20 years ago, does not of course report any interaction with an LLM. Recently, we showed in [13] how one can easily plug any first order logic (FOL) automated theorem prover (ATP) into LPTP. We observe that inside the LPTP interactive development environment, namely Emacs, the FOL axioms are hardwired within tactics. Going back to the FOL formalization of the operational semantics of Prolog described in [20], and translating the axioms in FOF, a human-readable syntax for FOL [21], we can apply anyoff-the-shelfFOF-compatible ATP. We applied this strategy to the whole LPTP library, and obtained a success rate of about 80% with a 20 seconds timeout, running two of the most successful ATPs. The main advantage of this approach is that we can run the freely available ATPs locally on our machines, without relying on a non-free external provider. Moreover, the experiments are easily reproducible. On the other hand, we get resolution proofs (more precisely superposition calculus proofs) which cannot be directly rewritten as natural deduction proofs as needed for LPTP. So we cannot proof-check these proofs with LPTP. We experimented the approach on our √ 2 example. The results appear in the ATP column of Tables 1 and 2 and are summarized in the conclusion. Back to our case study, we have illustrated how a formal proof checker, LPTP, can be combined with an LLM (in our experiment Claude) in order to arrive at a successful (partial) automatization of a theorem proving process. In particular, we use the LLM to generate proof steps whose correctness is subsequently checked by the proof checker. This is known as proof-step generation (e.g., [8, 16]) and contrasts somewhat with other approaches that try to generate the proof as a whole (e.g., [6, 9]). Our observations are in line with the recent literature where similar combinations of language models and proof checkers are explored using a variety of approaches. Giving a complete overview of existing and ongoing work is outside the scope of the current paper, but we can cite the following. For example, in [25] a language model (DeepSeek-Prover-V1.5) is introduced that is specifically designed and trained 78Case study: proving √ 2irrational with LPTP and an LLM for doing theorem proving in Lean 4. Being a model specifically trained on formal languages, it is in sharp contrast with other approaches using an off-the-shelf language model, including our own. In [23], the authors introduce COPRA a system that uses an off-the-shelf LLM (GPT-4) and in-context learning to let the model generate proof steps directly written in the formal language of Rocq or Lean. COPRA uses a backtracking search methodology to construct the proof in a step-by-step manner, using feedback from the proof checker to construct the prompt for the next step. Likewise, [22] also uses a general- purpose model (GPT-4) but proposes to use natural language as an intermediate language. An interactive environment (calledPétanque) provides two proof tactics that allow to convert the internal reasoning to Rocq code. In a somewhat similar way, the Hermes framework [14] couples informal reasoning by an LLM with a translator module that allows to translate this reasoning into Lean code and a prover module (such as Goëdel-Prover-V2) for verification. 7 Conclusion We report in this paper one of the very first interactions – to the best of our knowledge – between LPTP (Logic Program Theorem Prover) and an LLM. We have chosen Claude from Anthropic and did the experiment with Opus 4.5. We fed the LLM with the LPTP user manual in PDF format and two basic LPTP libraries (Prolog code and LPTP proofs in text format), one for Peano numbers and the other one about lists. We have selected a small classical problem among the proof assistant community, namely the irrationality of √ 2. This problem has been the running example of a whole book [24]. We did not find any LPTP proof of the irrationality of √ 2 on the Internet. While we had to explicitly give the proof structure of the two main results – namelysqrt2:irrational andevenpp:evenp–, the LLM was able to prove some simple properties, sometimes proposing and prov- ing new auxiliary lemmas. We stated the properties either in the LPTP language or in natural language (French in our case). Sometimes after a few back and forths between the LLM and LPTP, but sometimes directly, the lemmas generated by Claude were approved by the proof checker. Beyond the LLM, we also leveraged off-the-shelf first-order ATPs such as Vampire and E by trans- lating the LPTP axiomatization into FOF [21, 13]. They proved 5 out of 10 lemmas in the intermediate version (Section 3) and 9 out of 12 in the final, finer-grained version (Section 4). ATPs and the LLM play complementary roles: ATPs are free, local, fast and reproducible, but their resolution-based proofs cannot be easily rewritten as natural deduction and thus cannot directly enrich the LPTP library. As already implied by the literature (e.g., [11, 23]), the proof checker is the key element to eradicate LLM’s hallucinations. It allows the automatic and efficient classification of the LLM’s answers: either correct– the proof checker validates the proposed proof – orwrong– the proof checker does not validate the proposed proof and reports the firstincorrect derivation stepwithin the proposed proof –. The ability to point out the first step in the proof that is not correct is a great help for the LLM. Note also that once a proof is checked, the corresponding result can be safely added to the LPTP library, without compromising its logical consistency. This last point is crucial as the introduction of a false result in the library would allow the proof ofanystatement. The interactions between LPTP, an LLM, and an LP developer leading to a semi-LLM-generated LPTP proof of the irrationality of √ 2 is the main contribution of this work 1 . It paves the way to an AI-enhanced approach for proving LP/Prolog properties, as the relevance of LLMs will continue to grow in the future. We plan to evaluate the combination LPTP/LLM on a set of Prolog verification problems. 1 The data from the experiment are available athttps://github.com/FredMesnard/LPTP-LLM.git. F. Mesnard, É. Payet, W. Vanhoof79 References [1] K. R. Apt & E. Marchiori (1994):Reasoning about Prolog programs: from modes through types to assertions. Formal Aspects of Computing6(6), p. 743–765, doi:10.1007/BF01213601. [2] K. L. Clark (1978):Negation as Failure. In H. Gallaire & J. Minker, editors:Logic and Databases, Plenum Press, New York, p. 293–322, doi:10.1007/978-1-4684-3384-5_11. [3] Pierre Deransart (1993):Proof methods of declarative properties of definite programs.Theor. Comput. Sci. 118(2), p. 99–166, doi:10.1016/0304-3975(93)90107-5. [4] W. Drabent (2016):Correctness and Completeness of Logic Programs.ACM Trans. Comput. Log.17(3), p. 18, doi:10.1145/2898434. [5] G. Ferrand & P. Deransart (1993):Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs.J. Log. Program.17(2/3&4), p. 265–278, doi:10.1016/0743-1066(93)90033-D. [6] Emily First, Markus N. Rabe, Talia Ringer & Yuriy Brun (2023):Baldur: Whole-Proof Generation and Repair with Large Language Models. In:Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, Association for Computing Machinery, New York, NY, USA, p. 1229–1241, doi:10.1145/3611643.3616243. [7] ISO/IEC 13211-1 (1995):Information Technology – Programming Languages – Prolog – Part 1: General Core. [8] Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygó ́zd ́z, Piotr Miło ́ s, Yuhuai Wu & Mateja Jamnik (2022):Thor: wielding hammers to integrate language models and automated theorem provers. In:Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS ’22, Curran Associates Inc., Red Hook, NY, USA. [9] Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu & Guillaume Lample (2023):Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. arXiv:2210.12283. [10] J. W. Lloyd (1987):Foundations of Logic Programming. Springer-Verlag, doi:10.1007/978-3-642-83189-8. [11] Lachlan McGinness & Peter Baumgartner (2024):Automated Theorem Provers Help Improve Large Lan- guage Model Reasoning. In Nikolaj Bjørner, Marijn Heule & Andrei Voronkov, editors:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning,EPiC Series in Computing 100, EasyChair, p. 51–69, doi:10.29007/2n9m. Available at/publications/paper/vzpW. [12] Fred Mesnard, Thierry Marianne & Étienne Payet (2024):Automated Theorem Proving for Prolog Verifica- tion. In Nikolaj S. Bjørner, Marijn Heule & Andrei Voronkov, editors:LPAR 2024 Complementary Volume, Kalpa Publications in Computing18, EasyChair, p. 137–151, doi:10.29007/C25R. [13] Fred Mesnard, Thierry Marianne & Étienne Payet (2026):Automated Theorem Proving for Prolog Verifica- tion.Electronic Proceedings in Theoretical Computer Science439, p. 469–481, doi:10.4204/eptcs.439.32. [14] Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen & Farzan Farnia (2025):HER- MES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs, doi:10.48550/arXiv.2511.18760. ArXiv:2511.18760 [cs]. [15] D. Pedreschi & S. Ruggieri (1999):Verification of Logic Programs.J. Log. Program.39(1-3), p. 125–176, doi:10.1016/S0743-1066(98)10035-3. [16] Stanislas Polu & Ilya Sutskever (2020):Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393. [17] Balaji Rao, William Eiers & Carlo Lipizzi (2025):Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification. arXiv:2504.17017. [18] R. F. Stärk (1995):First-order theories for pure Prolog programs with negation.Arch. Math. Log.34(2), p. 113–144, doi:10.1007/BF01270391. 80Case study: proving √ 2irrational with LPTP and an LLM [19] R. F. Stärk (1996):Total Correctness of Logic Programs: A Formal Approach. In R. Dyckhoff, H. Herre & P. Schroeder-Heister, editors:ELP’96,LNCS1050, Springer, p. 237–254, doi:10.1007/3-540-60983-0_17. [20] Robert F. Stärk (1998):The theoretical foundations of LPTP (a logic program theorem prover).The Journal of Logic Programming36(3), p. 241–269, doi:10.1016/S0743-1066(97)10013-9. [21] G. Sutcliffe (2023):The logic languages of the TPTP world.Log. J. IGPL31(6), p. 1153–1169, doi:10.1093/JIGPAL/JZAC068. [22] Laetitia Teodorescu, Guillaume Baudart, Emilio Jesús Gallego Arias & Marc Lelarge (2024):NLIR: Nat- ural Language Intermediate Representation for Mechanized Theorem Proving. In:The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. Available athttps://openreview.net/forum?id= QzOc0tpdef. [23] Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri (2024):An In-Context Learning Agent for Formal Theorem-Proving. In:First Conference on Language Modeling. Available at https://openreview.net/forum?id=V7HRrxXUhN. [24] F. Wiedijk, editor (2006):The Seventeen Provers of the World, Foreword by Dana S. Scott.Lecture Notes in Computer Science3600, Springer, doi:10.1007/11542384. [25] Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo & Chong Ruan (2025):DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforce- ment Learning and Monte-Carlo Tree Search. In:The Thirteenth International Conference on Learning Representations. Available athttps://openreview.net/forum?id=I4YAIwrsXa.