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

arXiv: https://arxiv.org/abs/2607.21196 · HTML: https://mlsanity.com/paper/2607.21196/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 27 references that are in the map.
- First posted on arXiv 23 Jul 2026.

## Builds on (most cited first, 11 of 11)

- [Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity](https://mlsanity.com/paper/2507.09089/) (2025)
- [Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI](https://mlsanity.com/paper/2505.19443/) (2025)
- [Agentic Software Engineering: Foundational Pillars and a Research Roadmap](https://mlsanity.com/paper/2509.06216/) (2025)
- [Vibe Coding in Practice: Motivations, Challenges, and a Future Outlook -- a Grey Literature Review](https://mlsanity.com/paper/2510.00328/) (2025)
- [Vibe coding: programming through conversation with artificial intelligence](https://mlsanity.com/paper/2506.23253/) (2025)
- [AI Agentic Programming: A Survey of Techniques, Challenges, and Opportunities](https://mlsanity.com/paper/2508.11126/) (2025)
- [Is Vibe Coding Safe? Benchmarking Vulnerability of Agent-Generated Code in Real-World Tasks](https://mlsanity.com/paper/2512.03262/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [AI IDEs or Autonomous Agents? Measuring the Impact of Coding Agents on Software Development](https://mlsanity.com/paper/2601.13597/) (2026)
- [VibeContract: The Missing Quality Assurance Piece in Vibe Coding](https://mlsanity.com/paper/2603.15691/) (2026)

## Abstract (arXiv)

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.