I have to get back to my current side project, about which more in a bit. But a definite possible future side project is:
- Create a "foundations of math" wiki combining MediaWiki and the Metamath proof-checking engine.
04 April 2006
To do
Subscribe to:
Post Comments (Atom)
1 comment:
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.pdf
document shows how such proofs can look like.
Post a Comment