一个用Claude写Prolog代码并用LPTP证明正确性的实验。有具体的数字和流程，适合对LLM+形式化验证感兴趣的人。
本研究通过提示Claude生成Prolog代码和测试，并使用LPTP进行形式化证明。Claude为前33个P-99问题生成了58个逻辑过程、508个测试和257个引理（共11800行证明）。作者手动检查了所有代码和证明，验证了类型、终止性、唯一性等性质。该实验展示了“vibe-coding/vericoding”方法用于Prolog编程的可能性。
Case study: solving P-99 with LPTP and an LLM
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.