The existing proof involved exhaustive checking of thousands of possibilities and ran to 300 pages. The Flyspeck project used formal verification to certify it.