5. A hard problem solved

A few decades ago, people were looking at alternate algebraic descriptions of Boolean algebras. H. Robbins looked at these axioms, which use join and complementation alone:

(1) $x \vee y = y \vee x$ (commutativity)

(2) $(x \vee y) \vee z = x \vee (y \vee z)$ (associativity)

(3) $((x \vee y)' \vee (x \vee y')')' = x$ (a variant of $x = (x \wedge y') \vee (x \wedge y)$).

These conditions are obviously true in Boolean algebras. Robbins conjectured that they define Boolean algebras. This fact was finally proved in 1996 by a computer theorem-proving program, the first long-standing conjecture proved that way.

See http://www.mcs.anl.gov/home/mccune/ar/robbins/index.html .