Generating Lean 4 and SWI Prolog code with Grok 4.5

(832) 422-8646

Contact

I’ve written several posts about using Claude or ChatGPT to generate Prolog or Lean code to solve a chess puzzle. I didn’t think Grok would be up to the task, though I didn’t try it. I’ve heard good things about Grok 4.5, so I gave it a shot. It did great.

Here’s the problem, a variation on the n-queens problem formulated by Martin Gardner.

Can you place five white queens and three black queens on a 5 × 5 board so that no queen of one color attacks a queen of another color?

Here’s the prompt I have Grok 4.5.

Generate SWI Prolog code to solve the following chess puzzle. On a 5 by 5 chessboard, place 5 white queens and 3 black queens so that no queen is attacking a queen of the other color. Have the code enumerate all solutions.

The code ran correctly, giving all eight solutions.

I then asked Grok

Now generate Lean 4 code to solve the same puzzle.

The code did not run on the first or second attempts but ran correctly on the third iteration. That’s better than I’ve seen before. It’s not an apples-to-apples comparison, but it has usually taken many iterations with Claude before Lean code would run.

Solutions

There are eight solutions, each being a flip or a rotation of one fundamental solution. Here’s a representative.

SWI Prolog code

:- use_module(library(clpfd)).

%% Enumerate all ways to place 5 white queens and 3 black queens<br>%% on a 5x5 board so that no queen attacks a queen of the opposite colour.<br>%% Same-colour queens are allowed to attack each other.<br>%%<br>%% Positions are numbered 1..25 in row-major order:<br>%% 1 2 3 4 5<br>%% 6 7 8 9 10<br>%% 11 12 13 14 15<br>%% 16 17 18 19 20<br>%% 21 22 23 24 25

solve :-<br>solution(Whites, Blacks),<br>print_solution(Whites, Blacks),<br>fail.<br>solve :-<br>writeln('No more solutions.').

solution(Whites, Blacks) :-<br>length(Whites, 5),<br>length(Blacks, 3),<br>append(Whites, Blacks, All),<br>All ins 1..25,<br>all_distinct(All),<br>% canonical order so each set of positions is generated once<br>Whites = [W1,W2,W3,W4,W5],<br>W1 # write('W ')<br>; memberchk(Pos, Blacks) -> write('B ')<br>; write('. ')<br>)),<br>nl )),<br>nl.

Lean 4 code

-- Lean 4 solution for the 5×5 black-and-white queens puzzle.<br>-- 5 white queens + 3 black queens; no opposite-colour attacks.

def absDiff (a b : Nat) : Nat :=<br>if a ≥ b then a - b else b - a

def attacks (p q : Nat × Nat) : Bool :=<br>p.1 == q.1 || p.2 == q.2 || absDiff p.1 q.1 == absDiff p.2 q.2

/-- All 25 squares (0-based, row-major). -/<br>def allPositions : List (Nat × Nat) :=<br>(List.range 5).flatMap fun r =><br>(List.range 5).map fun c => (r, c)

/-- Combinations of length exactly `k` (order-preserving). -/<br>def combinations {α : Type} : Nat → List α → List (List α)<br>| 0, _ => [[]]<br>| _, [] => []<br>| k + 1, x::ys =><br>(combinations k ys).map (fun zs => x :: zs) ++<br>combinations (k + 1) ys

def isAttackedBy (pos : Nat × Nat) (queens : List (Nat × Nat)) : Bool :=<br>queens.any (fun q => attacks q pos)

/-- Every solution as a pair (white squares, black squares). -/<br>def solve : List (List (Nat × Nat) × List (Nat × Nat)) :=<br>(combinations 3 allPositions).foldl (fun acc blacks =><br>let forbidden := allPositions.filter fun p =><br>blacks.contains p || isAttackedBy p blacks<br>let available := allPositions.filter fun p =><br>!(forbidden.contains p)<br>acc ++ (combinations 5 available).map fun whites => (whites, blacks)<br>) []

/-- Pretty-print one board. -/<br>def printBoard (whites blacks : List (Nat × Nat)) : IO Unit := do<br>for r in List.range 5 do<br>let mut row := ""<br>for c in List.range 5 do<br>let p := (r, c)<br>row := row ++<br>(if whites.contains p then "W "<br>else if blacks.contains p then "B "<br>else ". ")<br>IO.println row<br>IO.println ""

/-- Enumerate and display every solution. -/<br>def main : IO Unit := do<br>let sols := solve<br>IO.println s!"Found {sols.length} solutions.\n"<br>for p in (List.range sols.length).zip sols do<br>let i := p.1<br>let (whites, blacks) := p.2<br>IO.println s!"Solution {i + 1}:"<br>printBoard whites blacks

#eval main

One thought on &ldquo;Solving a chess puzzle with Grok 4.5&rdquo;

Lewis Baxter

20 July 2026 at 14:55

For your amusement here is a hand-crafted Prolog program.

solve( [ WQ1,WQ2,WQ3,WQ4,WQ5, BQ1,BQ2,BQ3 ] ) :-

bagof( (I,J), ( between(1,5,I), between(1,5,J) ), B0 ),

select(WQ1,B0,B1),

select(WQ2,B1,B2), WQ2 @> WQ1,

select(WQ3,B2,B3), WQ3 @> WQ2,

select(WQ4,B3,B4), WQ4 @> WQ3,

select(WQ5,B4,B5), WQ5 @> WQ4,

select(BQ1,B5,B6),

select(BQ2,B6,B7), BQ2 @> BQ1,

select(BQ3,B7,_ ), BQ3 @> BQ2,

forall( ( member( (BI,BJ), [BQ1,BQ2,BQ3] ),

member( (WI,WJ), [WQ1,WQ2,WQ3,WQ4,WQ5] ) ),

( WI =\= BI , WJ =\= BJ, abs(WI-BI) =\= abs(WJ-BJ) ) ). % safe

Leave a Reply<br>Your email address will not be published. Required fields are marked *<br>Comment *<br>Name *

Email *

Website

Search for:

John D. Cook, PhD

My colleagues and I have decades of consulting experience helping companies solve complex problems involving data privacy, applied math, and statistics.

Let’s talk. We look forward to exploring the opportunity to help your company too.