Rationale: To increase accessibility of the Mizar corpus of thousands of mathematical proofs, theorems and definitions.

Although the Mizar corpus is publicly available, the proof checker is proprietary and Mizar notation is complex. Converting the entire Mizar corpus to a standard and open set-theoretic notation would have great value to automated theorem proving, artificial intelligence research and other areas of mathematics, computer science and software engineering.

We are recruiting volunteers! Please contact any project owner or comment on the wiki to inquire how you might contribute.