Posted on the Web February 17, 2003. Last updated on March 28, 2003 by Bob Veroff.

Here is a proof that a length 25 Sheffer equation named C6 (MOL-25A-785) implies modularity. This is a key step in proving that C6 is a short single axiom for modular ortholattices. This proof is 356 steps long! We found it using our method of proof sketches.

Here is a more comprehensive discussion.