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. What the record does not claim: the content of the 1997 paper in the Journal of Automated Reasoning, whose preprint links are dead and whose journal is paywalled; or the year of Robbins's conjecture itself, which the page gives only as shortly after 1933.