Content deleted Content added
Modif. |
Modif. |
||
Line 50:
== Other works connected to metamath ==
Using the design ideas implemented in Metamath, Raph Levien has realized what must be regarded as the smallest proof checker in the world. Called Ghilbert<ref>{{cite web | author=Levien | title=Presentation of Ghilbert | work=Asteroid Meta Wiki | url=http://planetx.cc.vt.edu/AsteroidMeta/Ghilbert}}</ref>, this software is only 500 lines of python long. Now Levien would like to realize a system where several people could collaborate together and his work is emphasizing modularity and connection between small theories. Using as well Metamath design principles, Juha Arpiainen has realized his own proof checker called Bourbaki (in common-lisp) and Marnix Klooster has coded a proof checker in Haskell (called Hmm).▼
▲Using the design ideas implemented in Metamath, Raph Levien has realized what must be regarded as the smallest proof checker in the world. Called Ghilbert, this software is only 500 lines of python long. Now Levien would like to realize a system where several people could collaborate together and his work is emphasizing modularity and connection between small theories. Using as well Metamath design principles, Juha Arpiainen has realized his own proof checker called Bourbaki (in common-lisp) and Marnix Klooster has coded a proof checker in Haskell (called Hmm).
The philosophy of Mel O'cat being absolutely existentialist, he has found the bottom-up process of entering proofs in Metamath absolutely inhuman and he designed a system (called mmj2) where proofs can be entered in both directions. There is also a project to add a graphical user interface to Metamath called mmide.
| |||