Robbins Conjecture

In the 1930s, Edward Huntington gave a tidy set of axioms for Boolean algebra — the algebra of AND, OR and NOT that underlies all of logic and digital circuits. Then Herbert Robbins suggested replacing one of those axioms with a different, shorter equation and asked: do you still get exactly Boolean algebra?

The whole Robbins conjecture is captured by a single line. A Robbins algebra has an operation + (think OR) and a negation $n$ (think NOT) obeying associativity, commutativity, and one curious law:

n(n(a + b) + n(a + n(b))) = a

The question: is every algebra satisfying this also a Boolean algebra? It looks like it should be easy. It was not. The problem stayed open for roughly 60 years, defeating Robbins, Huntington, and even Alfred Tarski, who popularized it.

An automated theorem prover doesn't reason in words — it rewrites equations. Given a pile of known identities, it repeatedly replaces a piece of a term with something equal to it, hunting for a chain that ends at the goal. Below is a tiny rewriting engine: pick a rule, click where it applies, and watch the term change.

<p class="hint">{{hint}}</p>
<div class="term-box">
  <div class="label">{{label_current}}</div>
  <div id="term" class="term"></div>
</div>
<div class="term-box goal">
  <div class="label">{{label_target}}</div>
  <div id="target" class="term"></div>
</div>
<div class="rules" id="rules"></div>
<div class="status" id="status">{{status_initial}}</div>
<div class="btns">
  <button id="reset" type="button" class="ghost">{{btn_restart}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.term-box { background: #f3f6f9; border: 1px solid #d6e0e8; border-radius: 8px;
            padding: .5rem .7rem; margin: .4rem 0; }
.term-box.goal { background: #eef7ef; border-color: #cbe6cf; }
.label { font-size: .7rem; letter-spacing: .04em; text-transform: uppercase; color: #6b7b8a; margin-bottom: .25rem; }
.term { font: 700 18px ui-monospace, monospace; color: #1d3557; word-break: break-all; line-height: 1.5; }
.tok { padding: 1px 0; border-radius: 4px; }
.hot { background: #ffe08a; cursor: pointer; outline: 1px solid #e0b53c; }
.hot:hover { background: #ffd24d; }
.rules { display: flex; flex-direction: column; gap: .35rem; margin: .6rem 0; }
.rule { text-align: left; font: 600 13px ui-monospace, monospace; padding: .4rem .6rem;
        border: 1px solid #1d3557; background: #fff; color: #1d3557; border-radius: 8px; cursor: pointer; }
.rule.sel { background: #1d3557; color: #fff; }
.status { font-size: 1rem; font-weight: 600; margin: .5rem 0; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Try to drive the starting term to the target. Each click is one rewrite step — exactly the kind of move EQP made millions of times. Checking that a single step is valid is trivial; finding the right sequence among an exploding tree of choices is the hard part. That search is precisely what a machine does well and what stumped humans for decades. See how the same combinatorial blow-up appears in SAT.

What kind of problem is "is every Robbins algebra Boolean"?

• It is a theorem, and it is now proven. In 1996, William McCune ran his automated theorem prover EQP (a relative of Otter) at Argonne National Laboratory. After about 8 days of search it produced a proof; the published result appeared in 1997. So the status is solved — answer: yes, every Robbins algebra is a Boolean algebra.
• Verifying is easy, finding is hard. A finished proof is a short chain of rewrite steps anyone can check by hand. Discovering that chain meant searching an enormous tree of equational consequences — the part no human managed in 60 years.
• The general problem is undecidable. Deciding whether an arbitrary equation follows from a set of equational axioms (the word problem for equational theories) is in general undecidable — there is no algorithm that always halts with the right answer. Provers like EQP succeed on particular problems, not on all of them.
• Why it mattered. This was a famous open conjecture closed not by new human insight but by a machine search, complete with a proof a person could later read and verify.

The Robbins story sits at the boundary between what is decidable and what is not — the same boundary explored by the halting problem.

"Search a space of equal transformations for one that reaches a goal" is the engine behind a huge slice of modern formal methods:

• Formal verification: proving a chip or protocol never reaches a bad state is a giant theorem-proving task, often solved by the same rewriting and search ideas.
• Proof assistants: tools like Coq, Lean and Isabelle let humans and machines build checkable proofs together; automated provers fill in routine steps.
• Program correctness: showing two programs are equivalent, or that code meets a spec, reduces to deciding equalities — exactly what equational provers attack.
• Mathematics by machine: the Robbins result was an early, headline proof that computers can settle real open problems, not just crunch numbers.

Learn how a prover cracked Robbins and you've met automated reasoning — the same machinery behind program equivalence and modern verification.

The Robbins conjecture is a small miracle of a problem: one short equation, an obvious-sounding question, and 60 years of human failure — closed at last in 1996 by EQP, a program that simply rewrote equations until the answer fell out. Every Robbins algebra really is a Boolean algebra.

The proof a person can read; the search that found it, almost no person could have run. That split — easy to check, brutally hard to discover — is the heartbeat of computer science, the same gap at the center of P vs NP. Sometimes the cleverest mathematician in the room is a machine that never gets tired of trying.