Case study: solving P-99 with LPTP and an LLM | Fred Mesnard et al. | ResearchPod

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

Alex: Welcome to another episode of ResearchPod. Today we are looking at a recent study that explores how we can bridge the gap between AI-generated code and formal mathematical certainty.

Sam: So the core problem is that AI often writes code that looks correct but might fail in subtle ways?

Alex: Exactly. Think about how a student might write an essay that sounds convincing but gets the facts wrong. AI code can do something similar — it produces programs that appear to work, but contain hidden logical errors that only show up later. The researchers call this "vibe-coding," where the AI is essentially writing by feel rather than by proof. The paper proposes a shift to what they call "vericoding," where the AI generates not just the code, but also a machine-checkable argument — a formal proof — that the code is logically sound.

Sam: So it's not enough for the code to pass a few tests. The AI has to demonstrate, step by step, why the code is correct?

Alex: Right. And to make sure those proofs aren't just made up, they run everything through an independent checking tool called a Logic Program Theorem Prover, or LPTP. Think of it like a strict exam board. The AI is the student, submitting both its answer and its working. The LPTP checks every line of that working against hard logical rules. If anything doesn't hold up, the whole submission is rejected, and the AI has to try again.

Sam: So the AI can't just produce a plausible-sounding proof and move on. It has to keep revising until the proof actually passes the checker?

Alex: Precisely. That feedback loop is the key mechanism. The LPTP acts as a referee that rejects invalid logic, which forces the AI to genuinely refine its reasoning rather than guess. The code and the proof have to align perfectly before the system accepts them.

Sam: And they tested this on a specific set of programming problems?

Alex: Yes — a well-known collection called the P-99 exercises, which are standard challenges used to measure how well someone, or something, understands a programming language called Prolog. They worked through the first thirty-three of those exercises using this verify-and-revise loop, generating over eleven thousand lines of proof code in the process.

Sam: Eleven thousand lines just for the proofs. That gives you a sense of how much additional work formal verification actually requires. But I'm curious — how does the system handle something as basic as numbers? You can't just use regular arithmetic if everything has to be logically airtight.

Alex: That's a good question, and it gets at something genuinely interesting. Ordinary numbers carry a lot of assumptions that are hard to prove from first principles. So the researchers use a system called Peano notation, which builds numbers up from scratch using pure logic. Zero is just zero. The number one is "the successor of zero." Two is "the successor of the successor of zero," and so on. It looks unusual written out, but it means every number is defined as a precise chain of logical steps, with no ambiguity anywhere.

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

Fred Mesnard, Thierry Marianne, Étienne Payet, Wim Vanhoof

Jul 23, 2026·3:47·arxiv·Original Paper

P-99 (Ninety-Nine Prolog Problems)LLM (Large Language Model)LPTP (Logic Program Theorem Prover)VericodingVibe-codingLPTP

Listen

4 min

Briefing

Research Approach

This study explores the intersection of "vibe-coding"—generating code from informal natural language specifications—and "vericoding," which involves ensuring that generated code meets formal reliability guarantees. The researchers tasked Claude (Opus 4.6) with solving the first 33 exercises of the classic P-99 Prolog problem set. For each problem, the model was required to produce the Prolog implementation, a test file, and formal proofs for properties including type preservation, groundness, termination, uniqueness, and existence.

Methodology and Verification

The authors established a rigorous workflow where Claude was provided with specific instructions via a CLAUDE.md file and a reference guide for LPTP. Because the goal was formal verification, the model was restricted to a pure subset of Prolog (e.g., no cuts, no built-ins) to ensure compatibility with the LPTP theorem prover. The researchers manually audited every output, re-running tests and proof-checking the generated lemmas. For complex functional properties, the authors provided natural language guidance to help the model formulate the necessary logical statements.

Findings and Results

Claude successfully generated 58 logic procedures and over 500 tests. Notably, the model proved 257 lemmas, totaling approximately 11,800 lines of proof. The generated code often differed from common online solutions because the model adhered to the strict "pure Prolog" constraints requested. The study also highlights an ongoing effort to integrate the Model Context Protocol (MCP) to allow LLMs to interact directly with LPTP, potentially reducing the need for manual prompt engineering and token-heavy documentation.

Why It Matters

This work demonstrates that LLMs can serve as effective assistants for formal verification, not just code generation. By combining the generative capabilities of LLMs with the rigorous checking of automated theorem provers, researchers can bridge the gap between informal requirements and formally verified software, even for complex tasks like prime factorization.

Key Terms and Definitions

Vibe-coding — The practice of generating code from informal natural language specifications without immediate formal verification.
Vericoding — A development approach where generated code is accompanied by formal proofs of reliability and correctness.
LPTP — A Logic Program Theorem Prover used to formally verify properties of Prolog programs, such as termination and functional correctness.
Peano notation — A method of representing natural numbers using a successor function (e.g., 2 is s(s(0))).
Model Context Protocol (MCP) — A standard protocol that allows AI agents to interact with external tools and data sources, such as theorem provers, in a structured way.

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.

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