lp15 at cam.ac.uk
Sat Oct 29 15:42:31 CEST 2016
A slight disappointment this weekend. I thought I would have a proof of the Jordan curve theorem just in time for the release. All the prerequisites seemed to be there. Sledgehammer was proving the goals one after another. Even with the last goal, it proved half and suggested two proofs for the other half. But they didn't work, and a closer look shows that this claim depends on prerequisites involving several thousand lines of HOL Light proof scripts. A bit like the EU-Canada treaty and the Wallonian Parliament.
More information about the isabelle-dev