MIT教员制作vdash

Mgccl

vdash是MIT的教员Cameron Freer制作的一个网站. 现在还没有启动.
主要意义就是创造一个一切基于形式化数学的wiki. 每一个定理都被一步一步的形式化证出来.
其中只有正确的语句才能够被发布.
这样网站的存在可以将所有的证明联系起来

可以看一下他在讲解这个事情的录像.
http://www.youtube.com/watch?v=ZDI7L4Ya9Ms

虽然这样的事情不是首次,但是希望这个可以成功,因为上次失败的案例是在1995年(根本都没有开始 )的QED Project.
类似的最为相像的系统就是Mizar System. 可惜是给专业数学家搞得东西,大众很难搞...
不过最为知名的应该是Metamath Proof Explorer,但是只有几个人在搞创作,其他人不能帮忙.
我将我的能力做点事吧. 只有做大了才有用. 网站出来了慢慢往上添...
不过我在想..如果用的是wiki形式做...想要做成真正的证明数据库就不容易了.

无心人

很好很强大

呵呵
做这个很困难