README for Ghilbert prototype Raph Levien 26 Feb 2010 Here is a prototype of the Ghilbert implementation. You can use the batch verifier as follows: python verify.py peano/peano_thms.gh You can run the web app locally by installing the appengine SDK and running: dev_appserver.py . Then navigating to http://localhost:8080/edit/thmname Save the proof by pressing Ctrl-S, then navigating to: http://localhost:8080/recent The interactive proof tool is, at present, extremly rough. For more details, see http://ghilbert.googlecode.com/ Note: includes the minified JavaScript version of google-diff-match-patch, which is (also) under Apache 2 license. For full attribution, please see: http://code.google.com/p/google-diff-match-patch/