Ghilbert home

Welcome to Ghilbert.

You are not currently logged in. If you have an account, please login! If you don't, see the mailing list for an invitation to create one.

Ghilbert is an interchange format for verification of formal proofs. It is closely related to Metamath, but has a stronger definition mechanism, a modular structure for proofs, and other changes. This site is a community repository of proofs, and also contains a web app for interactively editing proofs.

If you are new to proofs using verifiers in the metamath family, there's an introduction at (although the details of that verifier are not quite the same as ghilbert's).

If you have any questions, please ask on the mailing list at

Here are some popular destinations:

Under development is a new /workspace for editing all the content in the repository, with menus and tabs much like an IDE, and geared toward a more natural git-like workflow. It's possible to play with this even without an account, although saving does require one.

To edit the content on this site, you might want to consider creating an account. There's an account creation page, but to be most effective, you need an invite code. Feel free to contact Raph for one.

More links: