I have to get back to my current side project, about which more in a bit. But a definite possible future side project is:
Isabelle (http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html)would be another interesting candidate for the back end of such Wiki.It allows to write proofs that are much closer to how a regular mathematical proof looks like (as compared to the Metamath language). Also, it has a built-in theorem prover which allows to write proofs in larger steps, so it is not as tedious as with Metamath (still much more time consuming that in romantic math though). The http://www.nongnu.org/isarmathlib/IsarMathLib/document.pdfdocument shows how such proofs can look like.
Post a Comment