Pith. sign in

REVIEW 2 major objections 5 minor 25 references

The paper shows that a large language model, guided by a proof checker for Prolog, can complete a formal proof that the square root of 2 is irrational.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

A general-purpose LLM and the LPTP proof checker jointly produced a machine-checked proof that sqrt(2) is irrational, with the checker localizing every wrong step.

T0 review reviewed 2026-08-01 challenge →

load-bearing objection Honest, proof-checked case study of LLM+LPTP for sqrt(2); core proof is solid, but Section 5's bridge from the LPTP theorem to the Prolog query is unshown and should be tightened before acceptance. the 2 major comments →

arxiv 2607.21187 v1 pith:UJPEG42H submitted 2026-07-23 cs.LO cs.AIcs.SC

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

Fred Mesnard , \'Etienne Payet , Wim Vanhoof This is my paper
classification cs.LO cs.AIcs.SC MSC 03B3568N17
keywords formal verificationlogic programmingtheorem provinglarge language modelsproof checkingirrationality of square root of 2Prolognatural deduction
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This case study aims to establish a division of labour for formal proof: an off-the-shelf large language model proposes proof steps, a proof checker for logic programs accepts or rejects them, and a human supplies the high-level proof skeleton. The authors try to show that this loop terminates in a complete, machine-checked proof that the square root of 2 is irrational — that no two coprime natural numbers p and q satisfy p^2 = 2q^2. This matters because the corresponding Prolog query has an infinite search space, so no resolution-based engine can ever return the negative answer by exploration; only a proof can. The paper reports that the checker rejected every incorrect derivation, that the model proved most auxiliary lemmas on its own, and that the human only had to structure the two main results and give one hint.

Core claim

The central claim is that the combination of a human proof skeleton, an LLM generating candidate proofs for auxiliary lemmas, and a proof checker for pure logic programs yields a complete and verified proof of the irrationality of sqrt(2). The proof follows the classical argument: assume coprime p,q with p^2 = 2q^2; from p^2 even infer p even; write p=2r; derive 2r^2=q^2; infer q even; then 2 divides both p and q, contradicting coprimality. In the formalisation, the theorem is stated as: for all natural p,q, if nat(p), nat(q), and coprime(p,q), then not square(p)=2*square(q). The LLM successfully proved most auxiliary lemmas directly; the human provided the structure for the two main results

What carries the argument

The central object is the inductive extension of a logic program: for each user predicate, Clark's completion is augmented with success, failure, and termination predicates, fixed-point equivalences, and an induction schema along the predicate's recursive structure. Goals are lifted to first-order formulas by three operators that express whether a goal succeeds, fails, or terminates; the resulting theory is consistent and sound with respect to the operational semantics. The proof checker's practical feature is that it validates a natural-deduction proof step by step and can report the first invalid step in a failed proof attempt — this error localization is what makes the LLM feedback loop t

Load-bearing premise

The conclusion rests on the soundness of the proof checker's logical theory (Clark completion plus induction axioms) and of the imported natural-number and gcd lemmas; if either contains a flaw, an accepted proof file would not actually establish irrationality.

What would settle it

Instrument the proof checker to accept a deliberately false statement (for example, s(0)=0) by exploiting a bug in its rules or in a library lemma; if such an acceptance is possible, the checker's verdict on the sqrt(2) file no longer certifies irrationality. Conversely, an independent re-check of the final proof file against a different verified kernel would corroborate the result.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Every lemma whose proof the checker accepts can be added to the shared library without threatening consistency, so verified results accumulate across sessions.
  • The negative answer to the infinite-search Prolog query is established once and for all; no runtime search over N×N is needed.
  • The demonstrated 'LLM proposes, checker judges' loop is a template for other Prolog verification tasks, as long as a checker with error localization is available.
  • First-order automated theorem provers proved several lemmas too, but their resolution proofs are not directly convertible to the checker's natural-deduction format, so the checker remains the final gate.
  • The burden on the human is reduced to high-level proof structuring and occasional hints, not low-level arithmetic details.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • A natural next step, not tested here, is to let the LLM generate the main proof skeleton as well; this case study's need for a human-specified skeleton marks the current boundary.
  • The error-localization behaviour of the checker could itself be a subject of study: comparing how different LLMs respond to 'first incorrect step' feedback versus whole-proof rejection could guide tool design.
  • Because the proof library accumulates only checked lemmas, the approach could in principle grow a large verified corpus of Prolog program properties without a human re-checking each step — provided the checker's own soundness is independently established.
  • ATPs that solved the easy lemmas were still not enough for the final theorem, so a practical pipeline might use an ATP as a fast filter to label which lemmas are true before asking the LLM for natural-deduction proofs.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper reports a case study in which the authors use the LPTP proof checker together with Claude (Anthropic's LLM) to construct a machine-checked proof of the irrationality of sqrt(2). They formalize a standard proof in LPTP, identify a set of auxiliary lemmas, and iteratively ask Claude to produce LPTP proofs, feeding LPTP's error reports back. Most lemmas are proved by Claude directly or after a few iterations; the main theorem and one difficult lemma required human-provided proof skeletons. The paper also compares with automated theorem provers (Vampire, E) and describes an attempt to prove in LPTP that the motivating Prolog query cannot succeed. The final proof is claimed to be fully checked by LPTP, and the artifact is available on GitHub.

Significance. If the artifact is complete, the paper convincingly demonstrates that an off-the-shelf LLM can be integrated with a lightweight proof checker for logic programs, and that LPTP's error localization makes the feedback loop effective. The explicit accounting of human vs LLM effort and the use of an external checker are strengths. The comparison with ATPs is a useful baseline. However, the paper's main claim of a 'complete formal proof' is established only for the mathematical theorem; the operational query-level claim in Section 5 is not backed by sufficient detail. The paper is a valuable empirical contribution to the LLM-assisted theorem proving literature, but the presentation needs to fill an important gap.

major comments (2)
  1. [Section 5 (Back to Prolog)] The paper claims that 'Claude is able to generate three bridging lemmas and to prove that sqrt2_is_rational can not succeed by contradiction,' but the statements of these lemmas and their LPTP proofs are not given. Since the motivating query in Section 1 contains the operational gcd predicate defined with Prolog's if-then-else (->), while Section 2 defines LPTP's goal language without ->, the reader cannot determine whether the LPTP proof applies to the same gcd predicate as in the query. The equivalence between coprime(P,Q) and gcd(P,Q,s(0)) is asserted but not formally demonstrated. This is a load-bearing step for the claim that the answer to the query is 'no' and that the formal proof covers the operational query. Please include the bridging lemmas (and ideally their proofs) and clarify the relationship between the operational and logical definitions of gcd.
  2. [Sections 3-4 (formalization)] The paper freely uses the function symbols * and square and the predicate times/3 without specifying how they are defined in LPTP. For instance, lemma npq:nnppqq is stated as ∀n,p,q (n = p * q → square(n) = square(p) * square(q)) with no nat antecedents, although square is defined only for arguments satisfying nat. Similarly, the main theorem's conclusion uses the term s(s(0)) * square(q). The reader needs to know whether * is a defined function symbol or an abbreviation for the times predicate, and under what conditions the lemmas are proved. Since the paper's contribution is a machine-checked proof, precise statements of the formal definitions are necessary to make the results reproducible and to rule out that the lemmas rely on unintended properties of partially defined functions.
minor comments (5)
  1. [Throughout] Minor language issues: 'we take profit of this exercise' should be 'we take advantage'; 'The theoretical basis and specification language is purely first-order logic' should use 'are'.
  2. [Section 5] It would be useful to state which parts of the final proof were produced by Opus 4.6 as opposed to Opus 4.5, and whether any earlier proofs had to be rechecked after the model switch.
  3. [Tables 1 and 2] Please specify the ATPs (Vampire/E) and the axiom set used; currently the reader must consult reference [13] to interpret the ATP column.
  4. [Figures 1 and 2] The dependency graphs are hard to read in the printed version; consider larger fonts or a different layout.
  5. [Section 4] The prompts to Claude (for example, 'Donne-moi une preuve LPTP de :') are given in French; an English translation would help international readers, or a note that the language of interaction is not important.

Circularity Check

0 steps flagged

No circularity: the LPTP proof-checked derivation is self-contained; self-citations are peripheral and the Section 5 bridge gap is a formalization caveat, not a circular step.

full rationale

The derivation chain is: (1) state auxiliary lemmas, admitted temporarily via `by gap`; (2) have Claude generate proofs; (3) have LPTP reject incorrect steps and accept the final proofs; (4) combine them into `sqrt2:irrational`. Each step is checked by an external proof checker (LPTP) against Stärk's IND(P) theory, so the conclusion is not assumed as an input. The lemma set is genuinely auxiliary: `sqr2:4`, `twotimes:even`, `even:twotimes`, `even:div2`, etc., none is a restatement of the theorem, and `evenpp:evenp` is given a separate case-split hint and proof. The only author self-citations [12,13] support the ATP column, which records experiments with Vampire/E; these results are not used to justify the LPTP proof and are not load-bearing. The remaining caveats—trusting LPTP's soundness and its nat/gcd libraries, and Section 5's unshown bridge from pure `coprime`/`gcd` to the operational `->`-based `gcd` in the query—are external-tooling and proof-detail gaps, not cases where a result is equivalent to its own input by construction. Thus no significant circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The paper's result rests on trusting LPTP's soundness, on the correctness of the imported nat/gcd libraries, and on the adequacy of the Herbrand-term encoding of natural numbers. There are no fitted parameters and no invented entities.

axioms (3)
  • domain assumption LPTP's inductive extension IND(P) — Clark's completion plus the nine axiom schemas including induction — is sound for the ISO-Prolog operational semantics used.
    Section 2 describes the axioms and cites Stärk [20] for correctness; the paper does not re-verify the checker.
  • domain assumption The imported LPTP nat/gcd library lemmas (e.g., times:existence, times:uniqueness, gcd properties) are correct.
    Used without proof in Section 3 for square:existence, square:uniqueness, and in the main proof skeleton.
  • domain assumption The encoding of natural numbers as Herbrand terms 0, s(0), ... with nat/plus/times is an adequate formalization of the arithmetic claim that sqrt(2) is irrational.
    Sections 1-3 assume this correspondence; LPTP checks the formal statement, not the informal mathematical claim.

reviewed 2026-08-01 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Case study: proving sqrt(2) irrational with LPTP and an LLM." pith.science (2026). https://pith.science/paper/UJPEG42H

@misc{pith2026260721187,
  author       = {Pith},
  title        = {Pith review of: Case study: proving sqrt(2) irrational with LPTP and an LLM},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UJPEG42H}},
  note         = {Machine review of arXiv:2607.21187}
}
Share X Bluesky LinkedIn Reddit HN
read the original 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.

Figures

Figures reproduced from arXiv: 2607.21187 by \'Etienne Payet, Fred Mesnard, Wim Vanhoof.

Figure 1
Figure 1. Figure 1: Dependency graph of the lemmas of Table 1. An arrow [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Dependency graph of the auxiliary lemmas of Table 2. An arrow [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

25 extracted references · 9 canonical work pages

  1. [1]

    K. R. Apt & E. Marchiori (1994): Reasoning about Prolog programs: from modes through types to assertions. Formal Aspects of Computing 6(6), pp. 743–765, doi:10.1007/BF01213601

    work page doi:10.1007/bf01213601 1994

  2. [2]

    K. L. Clark (1978): Negation as Failure. In H. Gallaire & J. Minker, editors: Logic and Databases, Plenum Press, New York, pp. 293–322, doi:10.1007/978-1-4684-3384-5_11

    doi:10.1007/978-1-4684-3384-5_11 1978

  3. [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

    work page doi:10.1016/0304-3975(93)90107-5 1993

  4. [4]

    Drabent (2016): Correctness and Completeness of Logic Programs

    W. Drabent (2016): Correctness and Completeness of Logic Programs . ACM Trans. Comput. Log. 17(3), p. 18, doi:10.1145/2898434

    work page doi:10.1145/2898434 2016

  5. [5]

    Ferrand & P

    G. Ferrand & P. Deransart (1993): Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs. J. Log. Program. 17(2/3&4), pp. 265–278, doi:10.1016/0743-1066(93)90033-D

    work page doi:10.1016/0743-1066(93)90033-d 1993

  6. [6]

    Rabe, Talia Ringer & Yuriy Brun (2023): Baldur: Whole-Proof Generation and Repair with Large Language Models

    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, d...

    arXiv 2023

  7. [7]

    ISO/IEC 13211-1 (1995): Information Technology – Programming Languages – Prolog – Part 1: General Core

    1995

  8. [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,...

    2022

  9. [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

    Pith/arXiv arXiv 2023

  10. [10]

    J. W. Lloyd (1987): Foundations of Logic Programming. Springer-Verlag, doi:10.1007/978-3-642-83189-8

    doi:10.1007/978-3-642-83189-8 1987

  11. [11]

    Lachlan McGinness & Peter Baumgartner (2024): Automated Theorem Provers Help Improve Large Lan- guage Model Reasoning. In Nikolaj Bjørner, Marijn Heule & Andrei V oronkov, editors:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning , EPiC Series in Computing 100, EasyChair, pp. 51–69, doi:10.29007/2n9m. Available...

    work page doi:10.29007/2n9m 2024

  12. [12]

    In Nikolaj S

    Fred Mesnard, Thierry Marianne & Étienne Payet (2024): Automated Theorem Proving for Prolog Verifica- tion. In Nikolaj S. Bjørner, Marijn Heule & Andrei V oronkov, editors:LPAR 2024 Complementary V olume, Kalpa Publications in Computing 18, EasyChair, pp. 137–151, doi:10.29007/C25R

    work page doi:10.29007/c25r 2024

  13. [13]

    Electronic Proceedings in Theoretical Computer Science 439, p

    Fred Mesnard, Thierry Marianne & Étienne Payet (2026): Automated Theorem Proving for Prolog Verifica- tion. Electronic Proceedings in Theoretical Computer Science 439, p. 469–481, doi:10.4204/eptcs.439.32

    doi:10.4204/eptcs.439.32 2026

  14. [14]

    ArXiv:2511.18760 [cs]

    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]

    Pith/arXiv arXiv doi:10.48550/arxiv.2511.18760 2025

  15. [15]

    Pedreschi & S

    D. Pedreschi & S. Ruggieri (1999): Verification of Logic Programs. J. Log. Program. 39(1-3), pp. 125–176, doi:10.1016/S0743-1066(98)10035-3

    work page doi:10.1016/s0743-1066(98)10035-3 1999

  16. [16]

    arXiv:2009.03393

    Stanislas Polu & Ilya Sutskever (2020): Generative Language Modeling for Automated Theorem Proving . arXiv:2009.03393

    Pith/arXiv arXiv 2020

  17. [17]

    arXiv:2504.17017

    Balaji Rao, William Eiers & Carlo Lipizzi (2025): Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification. arXiv:2504.17017

    arXiv 2025

  18. [18]

    R. F. Stärk (1995): First-order theories for pure Prolog programs with negation. Arch. Math. Log. 34(2), pp. 113–144, doi:10.1007/BF01270391. 80 Case study: proving √ 2 irrational with LPTP and an LLM

    doi:10.1007/bf01270391 1995

  19. [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, LNCS 1050, Springer, pp. 237–254, doi:10.1007/3-540-60983-0_17

    doi:10.1007/3-540-60983-0_17 1996

  20. [20]

    Stärk (1998): The theoretical foundations of LPTP (a logic program theorem prover)

    Robert F. Stärk (1998): The theoretical foundations of LPTP (a logic program theorem prover). The Journal of Logic Programming 36(3), pp. 241–269, doi:10.1016/S0743-1066(97)10013-9

    doi:10.1016/s0743-1066(97)10013-9 1998

  21. [21]

    Sutcliffe (2023): The logic languages of the TPTP world

    G. Sutcliffe (2023): The logic languages of the TPTP world . Log. J. IGPL 31(6), pp. 1153–1169, doi:10.1093/JIGPAL/JZAC068

    work page doi:10.1093/jigpal/jzac068 2023

  22. [22]

    In: The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24

    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 at https://openreview.net/forum?id= QzOc0tpdef

    2024

  23. [23]

    In: First Conference on Language Modeling

    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

    2024

  24. [24]

    Wiedijk, editor (2006): The Seventeen Provers of the World, Foreword by Dana S

    F. Wiedijk, editor (2006): The Seventeen Provers of the World, Foreword by Dana S. Scott. Lecture Notes in Computer Science 3600, Springer, doi:10.1007/11542384

    work page doi:10.1007/11542384 2006

  25. [25]

    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

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

    2025

This paper was first reviewed by deepseek-v4-flash on August 1, 2026.