A Robbins algebra is an algebra including a single binary relation satisfying associativity, commutativity, and the "Robbins axiom" $\neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = a$.

McCune's proof that Robbins algebras are synonymous with Boolean algebras is a relatively famous application of computer-assisted automated theorem proving; the output of the computer was small enough to be checked "by hand". This is on the "flip-side" of, for example, the Four-Color Theorem, wherein the output is likely not human-readable and more trust must, in a sense, be placed in the computer.

My limited understanding is that, although human-readable, the proof per se lacks intuition - it isn't clear how a human could have come up with the proof of the Robbins conjecture.