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.
isabelle-dev mailing list