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

Reply via email to