It has been known since the 1850's (or even much earlier) that 5 queens could be placed on an 8*8 chessboard so that every square on the board lies in the same row, column, or diagonal as at least one of the queens. It was also "known" that this could not be done with 4 queens. But I have not been able to obtain or track down any rigorous mathematical proof of this that could be (or could have been) carried out in a reasonable time by a human being with pencil and paper. There are altogether 635376 ways of placing 4 queens on an 8*8 chessboard. Does anyone know of a combinatorial algorithm, exploiting the symmetries of the chessboard, which would reduce the number of cases to be considered to the hundreds (or, at most, the low thousands.)? This is, of course, a trivial problem for modern computers, which have many times since verified that 5 queens are needed.

The problem of finding the minimum number of queens needed to cover an nbyn board is the queens domination problem. According to http://ajc.maths.uq.edu.au/pdf/15/ocrajcv15p145.pdf , "Although there is currently no mathematical proof that these values [the known minimum numbers of queens] are correct, they have been verified by computer." According to http://www.combinatorics.org/Volume_8/PDF/v8i1r29.pdf , "...current knowledge that [among other things, the queens domination number for an 8by8 board is greater than 4], comes from exhaustive search." 


The number of fundamental arrangements one needs to check to prove there is no solution with 4 queens is about $\frac{1}{8}{64 \choose 4}\sim 10^5$ as Mark Meckes noted in his comment. This number can be greatly reduced if we choose to inspect the space of solutions with $5$ queens. Clearly, every hypothetical $4$ queens' solution generates a family of $5$ queens' solutions (just place the $5$th queen at any of the $60$ remaining free squares). Now, there are only $638$ fundamental arrangements with $5$ queens. All $4860$ solutions can be obtained from the fundamental arrangements by rotation and reflection. This was reportedly first calculated `by hand' by A.M. Yaglom and I.M. Yaglom (check out "Across the Board: The Mathematics of Chessboard Problems" by John J. Watkins). It seems to be a pretty feasible task to check that one cannot remove a queen in any of those arrangements and still get a dominating arrangement. 


I also wonder whether the formation came before or after 1990, because that is when Spencer came up with the lower bound for n=11. I know firsthand that formations can be searched for by hand for say, up to n=20 with reasonable results (note that is much different than actual proof that the formation is minimal, for if we find the formation we've only found an upper bound). So it's quite possible that someone found the formation first, and then Spencer might have been the first to observe it. Of course it's also possible that Spencer's bound came first. I found Dr Chatham's comment interesting enough to vote it up, although seeing as how I'm stuck at one reputation, I can't. 

