[thaumasiotes]

The art museum visitor would be unambiguously correct in the case of De Morgan's laws. Rolle's Theorem depends on some fairly tricky setup work.

But for an even more obvious theorem that was actually difficult to prove (Rolle's theorem isn't), see https://en.wikipedia.org/wiki/Jordan_curve_theorem

("Any path which begins in the interior of a closed curve, and ends in the exterior of the same curve, must cross the curve at some point.")

[yesenadam]

From that link:

"The first formal proof of the Jordan curve theorem was created by Hales in the HOL Light system, in January 2005, and contained about 60,000 lines. Another rigorous 6,500-line formal proof was produced in 2005 by an international team of mathematicians using the Mizar system. Both the Mizar and the HOL Light proof rely on libraries of previously proved theorems, so these two sizes are not comparable."