EQP solves the Robbins problem
On 10 October 1996 the program EQP, built at Argonne National Laboratory, found a proof that every Robbins algebra is Boolean. The search took about eight days on an RS/6000 processor and used about 30 megabytes of memory. Herbert Robbins had posed the question shortly after 1933; neither he nor Huntington found a proof, and Tarski and his students later studied it.
Why it matters
A program solved automatically an open problem mathematicians had worked on since the 1930s and on which, the page says, there had been no significant progress since the early 1980s. The machine was no longer checking or repeating a human proof; it found its own.
The problem: whether, in the axioms for Boolean algebra E. V. Huntington gave in 1933, his equation can be replaced by Robbins's simpler one. William McCune's page on the solution was posted in October 1996; EQP resembles the laboratory's better-known Otter but has associative-commutative unification and is restricted to equational logic. The program's log: EQP 0.9 of June 1996, the job began on 2 October 1996, the contradiction was found at second 678,232. McCune's paper, submitted to the Journal of Automated Reasoning on 22 January 1997, describes how the search went. The attack that led to the solution took five weeks, from 6 September to 11 October 1996, on up to three generic UNIX workstations. About fourteen multiday searches used about five CPU-weeks in all. The successful search ran almost 8 days, derived 49,548 equations and proved that every Robbins algebra satisfies a condition Steve Winker had earlier proved sufficient by hand. The machine first took on the problem in 1979, when Winker, a student visiting Argonne, learned of it from Joel Berman. Citing a phone conversation with Robbins in October 1996, the paper says the problem did not arise from Huntington's error, as folklore has it. What the record does not claim: the year of Robbins's conjecture itself; the page gives only shortly after 1933, the paper only the 1930s. The paper was read in the author's final version of March 1997, not in the typeset journal issue.