Solving a chess puzzle with Grok 4.5

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…