---
tag: X74S395RZD
kind: statement
role: theorem
name: Robbins conjecture
msc: ["06E05", "03G05", 68V15]
uses: [M3GFCVX549, 0XADJKM699]
about: [0XADJKM699]
sources:
  - url: https://en.wikipedia.org/wiki/Robbins_algebra
---

## Statement

Let $A$ be a set with a binary operation $+$ and a unary operation $n$ such that for all $x, y, z \in A$:

1. $x + y = y + x$;
2. $(x + y) + z = x + (y + z)$;
3. $n(n(x + y) + n(x + n(y))) = x$.

Such a structure is called a *Robbins algebra*, and axiom 3 is *Robbins' equation*.
Then $A$ satisfies [[Huntington's equation|M3GFCVX549]] $n(n(x) + y) + n(n(x) + n(y)) = x$, so $(A, +, n)$ is a [[Boolean algebra|0XADJKM699]] with $+$ as join and $n$ as complement.

## Remarks

Every Boolean algebra satisfies Robbins' equation, so the theorem says that the Robbins algebras are exactly the Boolean algebras.
The question was raised by Herbert Robbins in the 1930s and stayed open for about sixty years.
William McCune settled it in 1996 with the automated theorem prover EQP, which found a derivation of a condition that earlier work had shown to be sufficient.
The proof is purely equational; human-readable versions of it were written later.

## Explanations

### L1 human

Boolean algebra can be built from "or" and "not" with a few rules.
Robbins proposed a rule that looks very much like Huntington's rule, and asked whether it is just as strong.
For decades nobody could prove or refute it, until a computer program found a proof in 1996.

### L2 human

The result is a standard example of a mathematical question solved by an automated theorem prover.
It shows that the equational theory of Boolean algebras has several very short bases, and the search for the shortest single axioms for Boolean algebra builds on such results.
The proof works inside equational logic: it uses only substitution and replacement of equals by equals, starting from the three axioms.