{"id":"1a83ad71-ff9a-44a0-bc45-905855712c29","arxiv_id":"2607.21196","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An LLM, helped by human hints on correctness statements, produced LPTP-verified Prolog solutions for 33 of the 99 Prolog Problems.","lead":"The authors had an LLM (Claude) generate Prolog solutions and formal proofs for the first 33 Ninety-Nine Prolog Problems, with a theorem prover (LPTP) checking the proofs. The case study shows a 'vericoding' workflow in which informal specs are turned into code and machine-checked guarantees, though humans supplied hints for the hardest correctness properties.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 'just by prompting' claim is load-bearing but overstated: key functional-correctness properties were human-hinted, so LPTP certifies statements whose correspondence to the English P-99 specifications was not machine-checked.","rationale":"The reader's weakest_assumption identifies the same load-bearing issue: the LPTP-checked property statements were not derived end-to-end by the LLM, so LPTP certifies internal validity rather than adequacy to the English P-99 specifications. I agree with this concern and add that it is explicitly supported by the paper's own admissions in Sections 1, 5, and 6.3. The LPTP proof checker is real independent evidence for the logical validity of the proofs, and the authors' manual checks add credibility; nevertheless, the central 'just by prompting' claim depends on the formal statements being the right ones, and that dependency was discharged by human hints rather than by the LLM or by LPTP. This does not invalidate the case study; it narrows the claim to 'an LLM with human-provided functional specifications can produce LPTP-checked Prolog solutions'. Since the reader already rated the paper CONDITIONAL, my analysis supports that rating without moving the verdict.","tokens_in":12288,"tokens_out":7489,"duration_ms":85564,"concrete_test":"Re-run the P01–P35 pipeline using only the base prompt ('Read CLAUDE.md, lptp-reference.md, and solve the Pxx exercise') with no additional hints about what to prove, and require Claude to autonomously generate functional-correctness properties. Then compare, against a fixed manually written list of intended functional properties for all 33 exercises, how many are (i) generated without hinting and (ii) LPTP-certified. If the count is substantially below 33, the abstract's 'just by prompting' and the implied LPTP backing of functional correctness need qualification; if the count is high, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the first 33 P-99 exercises were solved 'just by prompting an LLM', where solving includes LPTP-certified proofs of types, groundness, termination, uniqueness, existence, and sometimes functional correctness. For that claim to hold, the LPTP-certified statements must be faithful formalizations of the English exercises. The paper itself shows this was not achieved autonomously: Section 1 and Section 5 state that for functional correctness 'we almost always provided some hints to Claude', and Section 6.3 says properties 23–30 for P35 were 'explicitly asked in natural language'. Thus the hardest logical step—connecting the generated Prolog code to the informal specification—was supplied by the human authors, not derived by Claude from the P-99 problem statements. LPTP then certifies the hinted statements and their proofs, but it cannot certify that those statements mean 'last element', 'prime', or 'prime factorization' in the intended sense. Moreover, for the many exercises where no functional-correctness property was proved, LPTP contributes only generic properties (types, groundness, termination, determinism); the 'solved' verdict rests on the 508 runtime tests and the authors' manual inspection. This is a useful case study, but it does not support the unqualified 'just by prompting' claim in the abstract.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":12628,"tokens_out":8448,"duration_ms":86328,"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":[{"comment":"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.","section":"Abstract; §1; §5"},{"comment":"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'.","section":"§6.3; Table 4"},{"comment":"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).","section":"§5; Tables 2-5"}],"minor_comments":[{"comment":"Typo: 'We choose Claude' should be 'We chose Claude'.","section":"§1"},{"comment":"The CLAUDE.md example contains user-specific absolute paths (/Users/fred/...). For reproducibility, these should be relative paths or placeholders.","section":"§4"},{"comment":"There are inconsistent spellings: 'prime_ f actors' appears in the text, while the code and tables use prime_factors. Please unify.","section":"§6.3"},{"comment":"'P-99' and 'P99' are used interchangeably (e.g., 'P99/Pxx' vs 'P-99.html'); please standardize.","section":"Throughout"},{"comment":"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.","section":"§8"}],"recommendation":"major_revision","confidential_remarks":"The authors already disclose the human role in formalizing functional-correctness properties in the body of the paper; the main revision is to align the abstract and conclusions with that disclosure and to make the per-exercise evidence auditable. I do not see a fatal technical flaw in the LPTP-checked results. Please also ensure that the companion paper [13], cited as 'this volume', is available to reviewers."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nWhat you should know: this is a real case study, not vaporware. The authors had Claude drive LPTP and produce machine-checked proofs for 33 Prolog problems, including a logic-programming proof of the prime factorization theorem. The LPTP certification is strong evidence that the generated lemmas are logically valid. The paper is also refreshingly honest in the body about what the LLM could not do alone.\n\nThe genuinely new pieces: attaching the LLM-plus-proof-checker recipe to LPTP, the MCP server that exposes LPTP to LLM assistants, and the P35 artifact itself. The numbers are concrete (58 procedures, 508 tests, 257 lemmas, 11,800 proof lines), the companion repository is provided, and the authors manually re-checked every generated file. The lptp-reference.md file, self-maintained by the LLM, is a useful process artifact.\n\nThe soft spots are real but not disqualifying. The abstract's \"just by prompting\" overstates the autonomy: the body says that for functional-correctness properties \"we almost always provided some hints,\" and for P35 the key properties 23–30 were explicitly formulated by the authors in natural language. So LPTP certifies the stated theorems, but the correspondence to the English P-99 specifications rests on human judgment plus the runtime tests. That is a genuine limitation, but it is disclosed, and no verification tool fully closes the informal-to-formal gap automatically. Two smaller issues: the repository is referenced by URL only, without a commit hash, which makes the artifact less pin-able; and there are no failure counts or iteration statistics, so we cannot see how many attempts produced the 33 successes. A case study can still be useful without those, but the empirical claim would be stronger with them.\n\nWho should read this: anyone working on LLM-generated verified code, especially in logic programming. It is a solid datapoint that a legacy proof checker can be driven by an LLM with moderate human steering, and the MCP bridge is genuinely reusable. It deserves a serious referee. The main revision I would ask for is a more careful abstract—say \"with hints for functional properties\"—plus a commit hash and a sentence on the number of trials that led to the reported results.\n\nMy verdict: worth engaging; send it to review. I expect it to be cited.","headline":"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.","tokens_in":13087,"tokens_out":2597,"would_cite":true,"duration_ms":29336,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68N17","68V15"],"pacs":[],"model":"deepseek-v4-flash","headline":"A large language model, prompted on informal English, produced machine-checked Prolog solutions to the first 33 P-99 exercises.","keywords":["P-99 Prolog problems","logic programming","large language models","formal verification","theorem proving","prime factorization","vericoding"],"falsifier":"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.","tokens_in":12223,"feed_emoji":"🤖","tokens_out":8188,"duration_ms":74265,"temperature":0.7,"pith_summary":"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.","feed_headline":"LLM plus proof checker solves 33 Prolog exercises","feed_subtitle":"Generated code, 508 tests, and 11,800 lines of proof certifying types, termination, and uniqueness.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["LLM + proof checker pass 33 Prolog exercises","AI solves 33 Prolog problems with verified proofs","Formal proofs for LLM-generated Prolog code","33 Prolog tasks solved via LLM and LPTP"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["LLM + proof checker pass 33 Prolog exercises","AI solves 33 Prolog problems with verified proofs","Formal proofs for LLM-generated Prolog code","33 Prolog tasks solved via LLM and LPTP"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00015,"raw_usage":{"total_tokens":1034,"prompt_tokens":748,"completion_tokens":286,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":492,"completion_tokens_details":{"reasoning_tokens":221}},"tokens_in":492,"tokens_out":286,"duration_ms":3258,"temperature":1.0,"reasoning_tokens":221,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T08:10:10.677400+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}