Ghilbert is an interchange format for formal proofs. As an interchange format, all that is needed to get started creating proofs is a verifier and a text editor. Yet, the promise of a simple, well-defined interchange format, rather than a complex highly-integrated system, is that there may eventually be an entire ecosystem consisting of various tools for automating the theorem proving process, searching and browsing proof repositories, integrations with other theorem-proving environments, and providing a rigorous basis for computer algebra systems and programming languages.

The design of Ghilbert is very closely based on Metamath. It adds a safe definition mechanism as well as a module system. There are a number of other changes, including the use of Lisp-like S-expressions to represent terms, and replacing the "distinct variable conditions" of Metamath with a more traditional technique of expressing free variables explicitly in the metalogic.

Even though the base Ghilbert format uses S-expressions, more sophisticated tools will present mathematical expressions using traditional mathematical layout.

Ghilbert is at present mostly vaporware, but a lot of the components have been prototyped to various degrees of completeness. Right now, the main focus is on creating a web app for collaborative proof development, interactively verifying proofs-in-progress in the browser. A roough prototype exists as an AppEngine app.

The nominal place for new discussions about Ghilbert is the Google group. Historically, discussion of Ghilbert has been fragmented in a number of places, including a PlanetMath wiki, the Metamath Google group, and other places.

Some active discussions here, especially coordination with the related JHilbert project: http://www.wikiproofs.de/

[obviously this site is still very much a stub - if you're interested in working on it yourself, contact Raph Levien, who will be happy to give write-access]

How to use the prototype

The prototype is now live, and, while crude, usable enough to start proving theorems. Here's a screenshot:

The batch verifier is at http://ghilbert.googlecode.com/. Basically just get the source, go into the ghilbert directory, and run "python verify.py peano/peano_thms.gh". A reasonable but clunky way to develop proofs is to add the proof to the bottom of the gh file and run the batch verifier.

If you prove a good peano theorem, the current way to save it is to commit to the svn repository. Ask for access, or just send it to me and I'll add it.

The web app is now live at http://ghilbert-test.appspot.com/. As of now, usability is terrible, but interactive proving with basic math typesetting does work. Use a Webkit-based browser, eg Chrome or Safari for best results. Here's a quick way to get a feel for it. Navigate to http://ghilbert-test.appspot.com/edit/nn0nlt0, then type the following:

thm (nn0nlt0 () ()
  (-. (< A (0)))
    1nle0 (1) A addge02t
    (1) (+ A (1)) (0) letr mpan
  A (0) nnltp1let mtbir

The top pane is the editor window, and should work more or less as expected (note: mouse clicking to move the cursor is not yet implemented; cut and paste use ctrl- keys even on a mac, and the clipboard is only within the editor ). The bottom pane, if everything is working, should display the proof status as you type. When you're done, it should display "¬A<0", the theorem being proved.

If you prove a good theorem in the web app, press ctrl-S to save. Then you can access it by looking at http://ghilbert-test.appspot.com/recent. My current methodology is to copy it from that display into peano_thms.gh, test with the batch verifier, and then submit using svn. There is not yet server-side checking of proofs.

A few simple theorems that can be easily proved are: letri3t, boundedal. Versions of these proofs in an older draft of Ghilbert are available at http://levien.com/garden/ghilbert/pax/pred-thms.gh.

Subpages (1): Related systems