The problem
Every Robbins algebra — a set with an associative, commutative binary operation satisfying \(\lnot(\lnot(x \lor y) \lor \lnot(x \lor \lnot y)) = x\) — is a Boolean algebra. (Resolved 1996 by machine.)
The Robbins conjecture
historicuniversal-algebra automated-reasoning
History & significance
Huntington (1933) axiomatized Boolean algebra; Robbins conjectured the same follows from a weaker single axiom with commutativity and associativity. Human provers chipped for sixty years — Winker (1992) found a conditional criterion that reduced the problem to finding one proof, but no human found it. In 1996 McCune's equational prover EQP, running for days, produced the missing proof: fourteen equations no human had seen. The first landmark theorem proved by a machine with no human guidance in the search.
Connected problems
- related The Four Colour Theorem
- related The Boolean Pythagorean Triples Problem
References
- primaryRead the primary source →
- sourceRobbins conjecture
The resolution (computer-assisted proof)
McCune (1996) let the automated prover EQP search from Winker's condition; after days of CPU time it returned a fourteen-step equational proof that every Robbins algebra is Boolean. No human directed the search — the machine found a proof humans had missed for sixty years.
Verified by curator — see the API for full claim provenance.