prob025: Lam's problem

proposed by Toby Walsh
tw@cs.york.ac.uk

Results

The problem has no solution. This shows that finite projective planes of order 10 do not exist.

The proof caused some controversy as it used computer brute force (2,000 hours on a Cray) and no one has been able (or is ever likely to be able) to check it by hand. Can constraint satisfaction algorithms reduce the size of this task?

Browne, M. W. "Is a Math Proof a Proof If No One Can Check It?" New York Times, Sec. 3, p. 1, col. 1, Dec. 20, 1988.

Petersen, I. "Search Yields Math Proof No One Can Check." Science News 134, 406, Dec. 24 & 31, 1988.