Introduction

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 nn (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.

Rewrite the Equations

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">An automated prover proves things by <b>rewriting</b>: replace a piece of the term with something equal to it, again and again, until you reach the goal. Pick a rule below, then click a highlighted spot in the term to apply it. Reach the <b>target</b> to finish the proof.</p>
<div class="term-box">
  <div class="label">Current term</div>
  <div id="term" class="term"></div>
</div>
<div class="term-box goal">
  <div class="label">Target</div>
  <div id="target" class="term"></div>
</div>
<div class="rules" id="rules"></div>
<div class="status" id="status">Pick a rule, then click where it applies.</div>
<div class="btns">
  <button id="reset" type="button" class="ghost">Restart proof</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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// A toy equational-rewriting engine in the spirit of EQP, the prover that settled the Robbins conjecture (McCune, 1996). We work with terms built from a binary operator "+" and variables a, b, c. Each rule rewrites a matching subterm into an EQUAL subterm. A proof is a chain of such steps that turns the start term into the target. Checking one step is trivial; finding the whole chain is the hard search a machine does well.
const START  = '((a+b)+(c+a))';
const TARGET = '((b+c)+(a+a))';

// Rules as left<->right patterns over single letters. Each rule, applied to a chosen subterm, replaces it by an equal term (commutativity / associativity).
// R1 commute:   X+Y  ->  Y+X
// R2 assoc-R:  (X+Y)+Z -> X+(Y+Z)
// R3 assoc-L:   X+(Y+Z) -> (X+Y)+Z
const RULES = [
  { id:'R1', text:'R1  commutativity:  X+Y = Y+X' },
  { id:'R2', text:'R2  associativity:  (X+Y)+Z = X+(Y+Z)' },
  { id:'R3', text:'R3  associativity:  X+(Y+Z) = (X+Y)+Z' },
];

// ---- tiny parser: term = "atom" | "(" term "+" term ")" ----
function parse(s){ let i=0;
  function atom(){
    if(s[i]==='('){ i++; const l=atom(); if(s[i]!=='+') throw 'exp +'; i++; const r=atom();
      if(s[i]!==')') throw 'exp )'; i++; return {op:'+',l,r}; }
    const c=s[i++]; return {op:null,v:c};
  }
  const t=atom(); if(i!==s.length) throw 'extra'; return t;
}
function show(t){ return t.op? '('+show(t.l)+'+'+show(t.r)+')' : t.v; }

// Apply a rule at the node identified by path (list of 'l'/'r').
function applyAt(root, path, ruleId){
  function rec(node, p){
    if(p.length===0) return transform(node, ruleId);
    const d=p[0];
    const child = d==='l'? node.l : node.r;
    const nc = rec(child, p.slice(1));
    if(nc===null) return null;
    return d==='l'? {op:'+',l:nc,r:node.r} : {op:'+',l:node.l,r:nc};
  }
  return rec(root, path);
}
function transform(node, ruleId){
  if(!node || node.op!=='+') return null;
  if(ruleId==='R1') return {op:'+',l:node.r,r:node.l};               // X+Y -> Y+X
  if(ruleId==='R2'){ // (X+Y)+Z -> X+(Y+Z)
    if(node.l.op!=='+') return null;
    return {op:'+',l:node.l.l,r:{op:'+',l:node.l.r,r:node.r}};
  }
  if(ruleId==='R3'){ // X+(Y+Z) -> (X+Y)+Z
    if(node.r.op!=='+') return null;
    return {op:'+',l:{op:'+',l:node.l,r:node.r.l},r:node.r.r};
  }
  return null;
}
// Where can the selected rule fire? Returns list of paths.
function spots(root, ruleId){
  const out=[];
  (function rec(node,p){
    if(transform(node,ruleId)!==null) out.push(p.slice());
    if(node.op==='+'){ p.push('l'); rec(node.l,p); p.pop(); p.push('r'); rec(node.r,p); p.pop(); }
  })(root,[]);
  return out;
}

let cur = parse(START);
let selRule = null;

function setStatus(t,cls){ const s=document.getElementById('status'); s.textContent=t; s.className='status '+cls; }

// Render the current term, marking the subterms where the selected rule fires.
function renderTerm(){
  const el=document.getElementById('term'); el.innerHTML='';
  const hot = selRule? spots(cur, selRule.id) : [];
  const hotSet = new Set(hot.map(p=>p.join('')));
  // walk the tree, emit spans; a "+"-node gets a clickable wrapper if hot.
  function build(node, path){
    const span=document.createElement('span'); span.className='tok';
    if(node.op==='+'){
      span.appendChild(document.createTextNode('('));
      span.appendChild(build(node.l, path+'l'));
      span.appendChild(document.createTextNode('+'));
      span.appendChild(build(node.r, path+'r'));
      span.appendChild(document.createTextNode(')'));
      if(hotSet.has(path)){
        span.classList.add('hot');
        span.addEventListener('click',(e)=>{ e.stopPropagation();
          const np = applyAt(cur, path.split(''), selRule.id);
          if(np){ cur=np; afterStep(); }
        });
      }
    } else { span.textContent=node.v; }
    return span;
  }
  el.appendChild(build(cur,''));
}
function afterStep(){
  renderTerm();
  if(show(cur)===TARGET){ setStatus('✓ Reached the target — proof complete!','ok');
    console.log('Proof complete:', show(cur)); }
  else setStatus(fmt('Rewritten to %show%. Keep going.', { show: show(cur) }),'');
}
function renderRules(){
  const box=document.getElementById('rules'); box.innerHTML='';
  RULES.forEach(r=>{ const b=document.createElement('button');
    b.className='rule'+(selRule&&selRule.id===r.id?' sel':''); b.textContent=r.text;
    b.addEventListener('click',()=>{ selRule=r; renderRules(); renderTerm();
      setStatus(fmt('Rule %id% selected — click a highlighted spot.', { id: r.id }),''); });
    box.appendChild(b); });
}
document.getElementById('target').textContent = TARGET;
document.getElementById('reset').addEventListener('click',()=>{ cur=parse(START); selRule=null;
  renderRules(); renderTerm(); setStatus('Pick a rule, then click where it applies.',''); });
renderRules(); renderTerm();
Result
Console

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.

The Real Complexity

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.

Where It Matters

"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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/robbins-conjecture/Content licensed under CC BY-NC 4.0.