Computer Proof of the Robbins Conjecture
Below, you'll find links to a Mathematica notebook of mine which explains in detail (and, in relatively easy-to-visualize, 2-dimensional mathematical notation) how the EQP proof of the Robbins conjecture works. This was the first EQP proof of the conjecture that all Robbins Algebras are Boolean, discovered by Bill McCune, et al at Argonne in October, 1996.
I presented this paper at the 1997 Mathematica Developer Conference. The paper has also been published in Mathematica in Education and Research (Winter 1998, Volume 7, No. 1). This project has also been featured on Wolfram Research's "Mathematica Demos", and "MathSource" pages.
For the full story on the computer solution of the Robbins Problem, including a brief outline of the history of this pesky little problem, see Bill McCune's "Robbins Algebras are Boolean" page. For those of you who don't have Mathematica, you can download Wolfram's free Mathematica Player. Or, you can download an the Adobe Acrobat PDF (which requires Adobe Acrobat Reader) version of the notebook instead. Of course, with the PDF version, you'll only be able to view/print the notebook; you won't be able to interact with it.