Pith. sign in

REVIEW

Large Formal Wikis: Issues and Solutions

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1107.3209 v1 pith:J637DVY4 submitted 2011-07-16 cs.DL

Jesse Alama , Kasper Brink , Lionel Mamane , Josef Urban This is my paper
classification cs.DL
keywords formallargewikicornissueslibrariesmathematicalwikis
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

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.

Discussion (0). Sign in to comment.

Pith tools