资 源 简 介
Ghilbert is an interchange format for verification of formal proofs. It is closely related to Metamath. The code tree is to include a reference verifier, a Web app for interactive and collaborative development of proofs (to run on AppEngine), and various translation tools. The Web app will store a repository of proofs.
