大型正式维基：问题与解决方案
Large Formal Wikis: Issues and Solutions
摘要：
我们提出了几个步骤，大型正式的数学维基。Coq证明助手与CoRN存储库一起被添加到由\cite{DBLP:conf/aisc/UrbanARG10}中描述的通用wiki系统处理的系统池中。基于最近开发的精确跟踪数学依赖关系的方法，提出了一种用于Mizar/MML和Coq/CoRN的wiki中大型正式库的智能再验证方案。我们建议使用最先进的文件系统的功能，以允许实时克隆和沙箱的整个图书馆，也允许扩展维基到一个真正的多用户协作区。讨论了若干相关问题。
英文摘要：
We present several steps towards large formal mathematical wikis. The Coq proof assistant together with the CoRN repository are added to the pool of systems handled by the general wiki system described in \cite{DBLP:conf/aisc/UrbanARG10}. A smart re-verification scheme for the large formal libraries in the wiki is suggested for Mizar/MML and Coq/CoRN, based on recently developed precise tracking of mathematical dependencies. We propose to use features of state-of-the-art filesystems to allow real-time cloning and sandboxing of the entire libraries, allowing also to extend the wiki to a true multi-user collaborative area. A number of related issues are discussed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
