The Mutilated Checkerboard
in Set Theory was presented at the QED meeting in Warsaw in 1995
July. It is a proof in set theory that I think an interactive prover
for heavy duty set theory should be able to accept. Besides
the html file, there is also a .dvi
file, a .pdf
file, a .ps version and a TeX version.
My 1964 memorandum A Tough Nut for Theorem Provers
has attracted some interest lately, and there is something more
about it at in the above URL.