Generating Lean 4 and SWI Prolog code with Grok 4.515 hours agohttps://www.johndcook.com/blog/2026/07/20/grok-chess/Grok 4.5 生成了 SWI Prolog 代码，用于枚举在 5x5 棋盘上放置 5 个白皇后和 3 个黑皇后且无相反颜色攻击的所有解。这个谜题是马丁·加德纳对 n 皇后问题的一个变体；共有八个解，通过旋转和反射相互关联。Grok 4.5 在三次尝试后也生成了可运行的 Lean 4 代码，表现优于作者之前使用 Claude 的体验。文章包含了完整的 Prolog（使用 clpfd）和 Lean 4 代码，以及一个手工制作的 Prolog 解决方案以供比较。