Pith. sign in

REVIEW 3 major objections 5 minor 27 references

Case study: solving P-99 with LPTP and an LLM

T0 review · 3 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

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

Pith's one-line read A large language model, prompted on informal English, produced machine-checked Prolog solutions to the first 33 P-99 exercises.

desk verdict Honest, reproducible case study of an LLM driving LPTP with machine-checked proofs, but the 'just by prompting' claim needs the human hints written into it. read the letter →

arxiv 2607.21196 v1 pith:JBYCLLTW submitted 2026-07-23 cs.LO cs.AI

Fred Mesnard , Thierry Marianne , Étienne Payet , Wim Vanhoof This is my paper · ORCID
classification cs.LOcs.AI MSC 68N1768V15
keywords P-99Prologproblemslogicprogramminglargelanguagemodelsformalverificationtheoremprovingprimefactorizationvericoding
verification ladder T0 review T1 audit T2 compute T3 formal

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 paper reports on an experiment in which a large language model was prompted with the informal English specifications of the first thirty-three Ninety-Nine Prolog Problems. The model generated Prolog code, runtime tests, and formal property statements with proofs; a logic program theorem prover machine-checked every proof. The authors claim they 'solved' each exercise in the sense that the code passes tests and the proofs certify types, groundness, termination, existence, uniqueness, and—where requested—functional correctness. Across the exercises the model wrote 58 logic procedures, 508 tests, 257 lemmas, and about 11,800 proof lines. If the claim holds, it shows a practical workflow in which an LLM produces code plus reliability guarantees that a human can check automatically, though for functional correctness the authors note they nearly always supplied hints about the logical statements to prove.

What carries the argument

The load-bearing mechanism is a proof checker for pure Prolog programs (with negation as failure, equality on finite trees, and Peano naturals). The workflow is: represent each generated Prolog program as a ground, variable-free clause file; have the model write property statements in the checker's formal language; let the checker certify each derivation; and accumulate reusable lemmas and proof techniques across exercises. The model's ability to reuse lemmas from earlier problems (e.g., the primality facts from exercise 31 inside the factorization proof of exercise 35) is what lets the proof effort compound, turning a large proof burden into 257 lemmas that amortize over 33 exercises.

What would settle it

Re-run the P35 experiment using only the standard instructions and prompt, with no human-supplied hints for the functional-correctness properties (existence, uniqueness, product, ordering, all-prime). If a fresh model cannot produce certified proofs of all those properties, then the claim that these exercises were solved 'just by prompting' fails under the paper's own definition of solved.

Watch

Extended reading notes

Core claim

The authors' central claim is that the first third of the P-99 exercises can be solved—code, tests, and formal proofs—by prompting a large language model, provided every proof is checked by a sound proof system for pure Prolog. The model produced 58 logic procedures and 508 tests, then 257 lemmas totalling about 11,800 lines of machine-checked proof. For the most demanding exercise, prime factorization, the resulting properties form a logic-programming proof of the prime factorization theorem: the generated factor list exists for every positive integer, is unique, is in ascending order, consists only of primes, and its product equals the number being factored. The authors are careful to note

Load-bearing premise

The proof checker certifies the formal statements the model writes, not their correspondence to the English exercise; if any statement encodes a subtly wrong definition of the intended property, the machine-checked 'solution' may not actually solve the problem as stated.

Editorial extensions

If this is right

  • Informal natural-language programming tasks can be turned into machine-certified code by an LLM plus a proof checker, with human effort concentrated on stating intent.
  • Every proof the checker rejects is a hallucination caught; the model can iterate until the derivation is certified, so the final artifact carries a machine-checkable guarantee.
  • The P35 result demonstrates that such workflows can produce nontrivial mathematical proofs—here, the prime factorization theorem—inside a logic programming framework.
  • The reproducible layout and tutorial file mean other developers can run the same pipeline on the remaining 55 exercises or on their own Prolog code.
  • Because lemmas are reused across exercises, the cost of verification decreases as a shared lemma library grows.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper qualifies 'just by prompting' with the admission that functional-correctness statements were almost always human-hinted; an honest reading is that LLMs today automate code, tests, and proof search, while humans still formalize intent. If this boundary persists, the limit of vericoding is the specification, not the proof.
  • The tool-based integration described in the last section points toward a turnkey service where any tool-using model can submit proof sketches for certification, which would test whether the human-hint bottleneck shrinks as models improve.
  • A direct experiment suggests itself: run the identical prompt on P36-P40 without human hints, and count how often the model independently formulates a correct functional-correctness statement. That would quantify how much of the 'solved' is the model versus the human steering.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper reports a case study in which the first 33 exercises of P-99 are claimed to be solved by prompting Claude (Opus 4.6) and checking the generated Prolog with LPTP. For each exercise, Claude is asked to produce pure Prolog code, a test file, and LPTP proofs of type, groundness, termination, uniqueness, existence, and sometimes functional correctness. The authors state that they manually inspected every generated file. They report 58 procedures, 508 tests, 257 lemmas, and about 11,800 proof lines. Three exercises (P01, P31, P35) are discussed in detail, and a separate MCP-based experiment for P14-P24 is described. The central claim is that this is a successful 'vibe-coding/vericoding' experiment with minimal human effort, but the paper itself discloses that functional-correctness statements were almost always supplied or hinted by the human authors.

Significance. If taken as a case study of LLM plus proof checker for logic programs, the contribution is real and useful. The LPTP-checked artifacts provide machine-checked evidence for 257 lemmas, and the P35 development is a notable verified implementation of prime factorization. The paper also demonstrates that an LLM can learn an unfamiliar proof formalism and produce large proofs, with LPTP catching errors. The aggregate 'solved by prompting' claim is, however, not fully established: the formal properties that connect the code to the English P-99 specifications were, by the authors' own account, largely human-formulated or human-hinted. LPTP certifies those statements and their proofs, not their correspondence to the informal exercises. With a qualified central claim and a complete per-exercise artifact table, this would be a valuable data point for the vericoding literature.

major comments (3)
  1. [Abstract; §1; §5] The central claim 'solved the first thirty three just by prompting an LLM' is not supported by the workflow described in the paper. Section 1 states that 'for functional correctness properties ... we almost always provided some hints to Claude to express the logical statements we were interested in', and §5 states that 'Sometimes we had to fully formulate the properties in natural language (see Section 6.3)'. For P35, properties 23-30 were 'explicitly asked in natural language'. LPTP therefore certifies statements whose semantic correspondence to the English P-99 problems was supplied by the human authors, not derived end-to-end by the LLM. The abstract and conclusions should be qualified accordingly, or the paper should provide evidence that Claude produced the formal properties from the English text without such hints.
  2. [§6.3; Table 4] The statement that the P35 results 'constitute a logic-programming-based proof of the prime factorization theorem' is stronger than what is shown. The properties in Table 4 are proved for the particular Prolog implementation prime_factors/2 and depend on the definitions of divides/2, times/3, @=</2, ordered/1, and product/2. They establish that this program computes a unique, ordered, all-prime list whose product is the input; they are not a direct LPTP formalization of the arithmetic theorem independent of the program. The text should either state the theorem as an LPTP theorem in its own right or explicitly say 'a verified implementation of the prime factorization theorem'.
  3. [§5; Tables 2-5] The paper does not provide enough per-exercise evidence to audit the claim that all first 33 exercises were solved. Only P01, P31, and P35 are shown in detail, and the MCP section covers P14-P24; the aggregate numbers (58 procedures, 508 tests, 257 lemmas, 11,800 lines) cannot be checked against the individual exercises from the text. Since 'solved' is defined by a conjunction of proved properties, a supplementary table listing each Pxx with the proved properties, whether functional correctness was included, and which properties required human hints is needed (or a clear statement that the repository is the complete auditable artifact).
minor comments (5)
  1. [§1] Typo: 'We choose Claude' should be 'We chose Claude'.
  2. [§4] The CLAUDE.md example contains user-specific absolute paths (/Users/fred/...). For reproducibility, these should be relative paths or placeholders.
  3. [§6.3] There are inconsistent spellings: 'prime_ f actors' appears in the text, while the code and tables use prime_factors. Please unify.
  4. [Throughout] 'P-99' and 'P99' are used interchangeably (e.g., 'P99/Pxx' vs 'P-99.html'); please standardize.
  5. [§8] The related-work discussion is broad but would benefit from a sentence positioning this case study relative to the vericoding benchmarks cited ([4], [26]), since the present workflow does not provide a formal specification upfront.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: LPTP is an external proof checker, the proved properties are not fitted predictions, and the authors' self-citations are background tooling rather than load-bearing premises.

full rationale

The paper's derivation chain is not circular. The central claim is that Claude generated Prolog code, tests, and LPTP proof scripts, which were then machine-checked by LPTP, an external theorem prover whose foundations are cited to independent work by Stärk. The LPTP-certified properties are statements about the generated programs (types, groundness, termination, uniqueness, existence, and functional correctness), and they are not derived from the proof text; they are independently stated and then verified. The human hints used for some functional-correctness properties (e.g., Section 5: 'For functional properties, we had to give hints to Claude'; Section 6.3: 'properties 23 to 30 that we explicitly asked in natural language') weaken the 'just by prompting' claim and the correspondence between natural-language specifications and formal statements, but that is a soundness/specification-adequacy limitation, not a circular reduction. Self-citations in the paper are limited to companion/background work on LPTP and related verification tools; none is invoked as an unverified uniqueness theorem or as an ansatz that smuggles in the result. The P35 'prime factorization theorem' is a genuine theorem proved against the generated code and independently stated properties, not a renaming of an input. Therefore no step reduces, by construction or by citation, to its own inputs.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

This is an empirical case study, not a fitted model, so there are no free parameters or invented entities. The core assumed inputs are: trust in LPTP as a proof checker, adequacy of the human-guided formal specifications, and reliability of the authors' manual verification narrative.

assumptions (3)
  • domain assumption LPTP is a sound proof checker for the target pure-Prolog fragment.
    All 'solved' claims rest on proof acceptance by LPTP; soundness is cited to Stärk [21] but not re-verified here.
  • ad hoc to paper The formalized properties capture the intended English problem statements.
    Humans supplied hints and natural-language formalizations for functional correctness; if the encoding is off, verified proofs do not imply the exercise is solved.
  • domain assumption The self-reported experiment descriptions (counts, timings, tests run, manual checks) are accurate.
    The paper does not include complete reproducibility logs; confidence in the narrative depends on the authors' manual checks and the linked repository.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Case study: solving P-99 with LPTP and an LLM." pith.science (2026). https://pith.science/paper/JBYCLLTW

@misc{pith2026260721196,
  author       = {Pith},
  title        = {Pith review of: Case study: solving P-99 with LPTP and an LLM},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JBYCLLTW}},
  note         = {Machine review of arXiv:2607.21196}
}
read the original abstract

Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By solved we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem Prover). Hence our approach is an experiment in vibe-coding/vericoding of P-99. It is a vibe-coding experiment because we started from informal specifications written in English and let Claude generate the Prolog code. It also fits within vericoding because the LLM proved reliability guarantees on the generated Prolog code. Claude wrote 58 logic procedures, 508 tests, 257 lemmas for a total of 11800 proof lines. We manually checked each file generated by the LLM. We checked the Prolog code, ran the tests, examined the logical statements generated by Claude and proof-checked Claude's proofs with LPTP. This paper describes this experiment and provides the main details so that it can be reproduced by the interested reader.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 8 canonical work pages

  1. [1]

    arXiv:2601.13597

    Shyam Agarwal, Hao He & Bogdan Vasilescu (2026): AI IDEs or Autonomous Agents? Measuring the Impact of Coding Agents on Software Development. arXiv:2601.13597

    arXiv 2026

  2. [2]

    Anthropic Blog

    Anthropic (2024): Introducing the Model Context Protocol. Anthropic Blog. https://www.anthropic. com/news/model-context-protocol

    2024

  3. [3]

    arXiv:2507.09089

    Joel Becker, Nate Rush, Elizabeth Barnes & David Rein (2025): Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity. arXiv:2507.09089

    arXiv 2025

  4. [4]

    CoRR abs/2509.22908, doi:10.48550/ARXIV .2509.22908

    Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan & Max Tegmark (2025): A benchmark for vericoding: formally verified program synthesis. CoRR abs/2509.22908, doi:10.48550/ARXIV .2509.22908. arXiv:2509.22908

    doi:10.48550/arxiv.2509.22908 2025

  5. [5]

    Cousot & R

    P. Cousot & R. Cousot (1977): Abstract interpretation: a unifed lattice model for static analysis of programs by construction or approximation of fixpoints . In: Proc. of the 4th Symp. on Principles of Programming Languages, ACM, pp. 238–252, doi:10.1145/512950.512973

    arXiv 1977

  6. [6]

    Cousot & R

    P. Cousot & R. Cousot (1992): Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2,3), pp. 103–179, doi:10.1016/0743-1066(92)90030-7

    work page doi:10.1016/0743-1066(92)90030-7 1992

  7. [7]

    In: Proceedings of the 48th International Conference on Software Engineering (ICSE 2026), Software Engineering in Practice (SEIP)

    Ahmed Fawzy, Amjed Tahir & Kelly Blincoe (2025): Vibe Coding in Practice: Motivations, Challenges, and a Future Outlook – a Grey Literature Review. In: Proceedings of the 48th International Conference on Software Engineering (ICSE 2026), Software Engineering in Practice (SEIP). Available at https://arxiv. org/abs/2510.00328

    arXiv 2025

  8. [8]

    Hassan, Hao Li, Dayi Lin, Bram Adams, Tse-Hsun Chen, Yutaro Kashiwa & Dong Qiu (2025): Agentic Software Engineering: Foundational Pillars and a Research Roadmap

    Ahmed E. Hassan, Hao Li, Dayi Lin, Bram Adams, Tse-Hsun Chen, Yutaro Kashiwa & Dong Qiu (2025): Agentic Software Engineering: Foundational Pillars and a Research Roadmap . CoRR abs/2509.06216. Available at https://doi.org/10.48550/arXiv.2509.06216

    arXiv doi:10.48550/arxiv.2509.06216 2025

Show all 27 references
  1. [9]

    Manuel V . Hermenegildo, Germán Puebla, Francisco Bueno & Pedro López-García (2005): Integrated pro- gram debugging, verification, and optimization using abstract interpretation (and the Ciao system prepro- cessor). Sci. Comput. Program. 58(1-2), pp. 115–140, doi:10.1016/J.SCI...

    2005 doi

  2. [10]

    Thierry Marianne, Fred Mesnard & Étienne Payet (2025): Automated Certification of Logic Program Groundness Analysis. In Santiago Escobar & Laura Titolo, editors: Logic-Based Program Synthesis and Transformation - 35th International Symposium, LOPSTR 2025, Rende, Italy, Septemb...

    2025 doi

  3. [11]

    IEEE Access 13, pp

    Christian Meske, Tobias Hermanns, Esther V on der Weiden, Kai-Uwe Loser & Thorsten Berger (2025):Vibe Coding as a Reconfiguration of Intent Mediation in Software Development: Definition, Implications, and Research Agenda. IEEE Access 13, pp. 213242–213259. Available at https:/...

    2025

  4. [12]

    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

    2026 doi

  5. [13]

    Fred Mesnard, Étienne Payet & Wim Vanhoof (2026): Case study: proving √ 2 irrational with LPTP and an LLM. In Wolfgang Faber & Laura Giordano, editors: Proceedings of the 42nd International Conference on Logic Programming (Technical Communications), ICLP 2026 , Electronic Proc...

    2026

  6. [14]

    In: Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages , LMPL ’25, Association for Computing Machinery, New York, NY , USA, p

    Jacqueline Mitchell & Yasser Shaaban (2025): Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages , LMPL ’25, Association for Compu...

    2025

  7. [15]

    Morales, Salvador Abreu, Daniela Ferreiro & Manuel V

    José F. Morales, Salvador Abreu, Daniela Ferreiro & Manuel V . Hermenegildo (2023):Teaching Prolog with Active Logic Documents. In David Scott Warren, Verónica Dahl, Thomas Eiter, Manuel V . Hermenegildo, 222 Case study: solving P-99 with LPTP and an LLM Robert A. Kowalski & F...

    2023 doi

  8. [16]

    ACM Transactions on Programming Languages and Systems 28(2), pp

    Étienne Payet & Fred Mesnard (2006): Nontermination inference of logic programs. ACM Transactions on Programming Languages and Systems 28(2), pp. 256–289, doi:10.1145/1119479.1119481

    2006

  9. [17]

    Roumeliotis & Manoj Karkee (2025): Vibe Coding vs

    Ranjan Sapkota, Konstantinos I. Roumeliotis & Manoj Karkee (2025): Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI. arXiv:2505.19443

    2025 arXiv

  10. [18]

    In: Proceedings of the 36th Annual Conference of the Psychology of Programming Interest Group (PPIG 2025)

    Advait Sarkar & Andrew Drosos (2025): Vibe coding: programming through conversation with artificial intelligence. In: Proceedings of the 36th Annual Conference of the Psychology of Programming Interest Group (PPIG 2025). Available at https://arxiv.org/abs/2506.23253

    2025

  11. [19]

    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

    1995 doi

  12. [20]

    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

    1996 doi

  13. [21]

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

    1998 doi

  14. [22]

    In: 2nd AI for Math Workshop @ ICML 2025

    Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue & Swarat Chaudhuri (2025): CLEVER: A Curated Benchmark for Formally Verified Code Generation. In: 2nd AI for Math Workshop @ ICML 2025. Available at https://...

    2025

  15. [23]

    arXiv:2508.11126

    Huanting Wang, Jingzhi Gong, Huawei Zhang, Jie Xu & Zheng Wang (2025): AI Agentic Programming: A Survey of Techniques, Challenges, and Opportunities. arXiv:2508.11126

    2025

  16. [24]

    arXiv:2603.15691

    Song Wang (2026): VibeContract: The Missing Quality Assurance Piece in Vibe Coding. arXiv:2603.15691

    2026

  17. [25]

    https://metr.org/notes/ 2026-03-10-many-swe-bench-passing-prs-would-not-be-merged-into-main/

    Parker Whitfill, Cheryl Wu, Joel Becker & Nate Rush (2026): Many SWE-bench- Passing PRs Would Not Be Merged into Main . https://metr.org/notes/ 2026-03-10-many-swe-bench-passing-prs-would-not-be-merged-into-main/

    2026

  18. [26]

    Veeravalli, Aarti Gupta & Sanjeev Arora (2026): AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algo- rithms

    Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V . Veeravalli, Aarti Gupta & Sanjeev Arora (2026): AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algo- rithms. arXiv:2602.09464

    2026 arXiv

  19. [27]

    arXiv:2512.03262

    Songwen Zhao, Danqing Wang, Kexun Zhang, Jiaxuan Luo, Zhuo Li & Lei Li (2026): Is Vibe Coding Safe? Benchmarking Vulnerability of Agent-Generated Code in Real-World Tasks. arXiv:2512.03262

    2026

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.