130 citations · 228 across the 17 of their papers we have counts for
5 papers · 1 filter
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
Jesse Alama, Lionel Mamane, Josef Urban
Two methods for extracting detailed formal dependencies from the Coq and Mizar system are presented and compared. The methods are used for dependency extraction from two large math…
Licensing the Mizar Mathematical Library
Jesse Alama, Michael Kohlhase, Adam Naumowicz +3
The Mizar Mathematical Library (MML) is a large corpus of formalised mathematical knowledge. It has been constructed over the course of many years by a large number of authors and…
Large Formal Wikis: Issues and Solutions
Jesse Alama, Kasper Brink, Lionel Mamane +1
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…
mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library
Jesse Alama
The Mizar Mathematical Library (MML) is a rich database of formalized mathematical proofs (see http://mizar.org). Owing to its large size (it contains more than 1100 "articles" sum…
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
Josef Urban, Jesse Alama, Piotr Rudnicki +1
Formal mathematics has so far not taken full advantage of ideas from collaborative tools such as wikis and distributed version control systems (DVCS). We argue that the field could…