Papers With

← All papers
First page of Greedy queens and the golden ratio

Greedy queens and the golden ratio

Boon Suan Ho

math.CO Sep 25, 2026 · v2
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
The authors provide a Lean formalization of the greedy queens result alongside the code for the finite state-graph verification.
Abstract
Place a queen in each successive column of an infinite $\mathbb{N}\times\mathbb{N}$ chessboard, always choosing the lowest row such that no two queens may attack one another. We prove that the row $q_n$ occupied by the queen in the $n$th column satisfies $q_n=nφ+O(1)$ or $q_n=n/φ+O(1)$, where $φ=(1+\sqrt5)/2$ is the golden ratio.
Problem

Greedy queens place a queen in each column of an infinite N×N board at the lowest non-attacked row. Dekking, Shallit, and Sloane conjectured that the queen positions stay within bounded distance of the lines y=xφ and y=x/φ.

Approach

The k-th upper queen is shown to lie on the k-th upper diagonal, and the conjecture is reduced to a bounded diagonal discrepancy |d_j−j|≤4 for lower queens. The process is modelled by finite local states (records) that are shown to determine each greedy step. A computer check confirms that the reachable states form a finite graph satisfying the required bounds, and induction extends this to all columns. Code and a Lean formalization are released.

Results

For upper queens, |q_n−nφ|<5/φ. For lower queens, |q_n−n/φ|<4+5/φ, which proves the conjecture. Sharper explicit bounds are also given, along with an O(N)-time, O(log N)-memory generator that uses under 2 MiB for ten billion queens.

Figure 8. The distance from each queen to its line, for 1\leq n\leq 10^{6} : the density of the points (n,q_{n}-n\phi) for upper queens (top) and (n,q_{n}-n/\phi) for lower queens (bottom), with a histogram of the distances on the right. Shaded: the bounds of Theorem 1 . Solid: the bounds of Theorem 2 . Dashed: Knuth’s observed ranges, in 0 -indexed coordinates.