TL;DR for operators The strongest result in this case study is not that an AI system wrote working Prolog. Across 33 targeted exercises, Claude generated 508 runtime tests alongside 257 lemmas and roughly 11,800 lines of proof, with the authors manually inspecting the generated files and an independent theorem prover checking the proofs. ...
A requirement can survive three meetings, two approvals, and a legal review while still meaning different things to everyone who reads it. That is not usually because anyone is careless. Natural language is simply very good at sounding settled before its meaning is settled. Words such as “after,” “until,” “immediately,” and “within” feel precise in conversation. In software requirements, they can quietly conceal incompatible assumptions about timing, cancellation, and acceptable system behavior. ...