Generating Lean 4 and SWI Prolog code with Grok 4.5
13 hours ago
- Grok 4.5 generated SWI Prolog code that enumerated all solutions for placing 5 white and 3 black queens on a 5x5 board without opposite-color attacks.
- The puzzle is a Martin Gardner variation of the n-queens problem; there are eight solutions, related by rotation and reflection.
- Grok 4.5 also produced working Lean 4 code after three attempts, outperforming the author's previous experiences with Claude.
- The article includes the full Prolog (with clpfd) and Lean 4 code, plus a hand-crafted Prolog solution for comparison.