Ghilbert is a formal proof checker, heavily inspired by Metamath. This repo contains a new implementation in progress, written Rust, as well as an older prototype, written in Python.
This quick start translates the propositional calculus fragment from Metamath into Ghilbert format and checks it.
Check out a copy of set.mm.
cd mm_xlat cargo run -- script ../../set.mm/set.mm /tmp/out.gh cd .. cargo run -- /tmp/out.gh
This will spew a lot of diagnostics, and also generate an HTML file for
each proof in the
gen directory. Note that to view these files
you probably want a simple server like
python -m SimpleHTTPServer 8000
rather than using
features load further files using XMLHttpRequest.
content/general are under
Creative Commons Share Alike 3.0.
All other proofs are under Creative Commons CC0 Public Domain
Many of the proofs are derived in some form from Metamath's set.mm, which
is also under CC0.
The main author is Raph Levien, with contributions from many others. (TODO: improve contributor attributions)
Contributions are welcome, just send a pull request!