ICIS Foundations Group  [Foundations FrontPage] [TitleIndex] [WordIndex]

Research/MathWiki

MathWiki

What?

Who?

The core project group is the Foundations Group at RU Nijmegen, however the project welcomes collaboration from anybody anywhere. The current contributors are:

People at RU:

People outside RU:

Background to the Research

We believe that formal (computer understandable and verifiable) mathematics has many advantages and is inevitable in the long term. Formal mathematics is not only important because it allows unmatched precision in checking the validity of (sometimes extremely long and complex) important ideas and designs. It is also important as a field providing uniquely deep understanding between computers and humans, allowing them to cooperate on semantic level in a number of novel strong ways that cannot be found in other areas.

There can obviously be various ideas about how formal mathematical wikis should look and what kind of functionality they should provide. For example, they could be just tools for collaborative web-based editing and development of existing formal libraries, or they could also provide a number of functions helping with formalization and understanding of formal mathematical texts and libraries. The wikis could target the existing systems and developers of formal libraries, or they could focus more on making formalization accessible to outsiders. Ideally, our efforts should lead to a platform and tools that make (collaborative) formalization much easier and smoother than it is today for everybody interested, and that allow development of large re-usable formal repositories analogous to the informal Wikipedia and Planetmath repositories.

The Basis

A starting point for the project are existing formal systems with large libraries, and the tools available for them. The current group's expertise is mainly in the Coq and Mizar systems. However the issues we are solving are to a large extent system-independent and we hope to make our techniques available for other major formal systems like Isabelle , HOL , HOL Light , and others. Our manpower is however limited, so anybody interested in collaboration is welcome.

The Tasks

Our focus so far has been on the following (high-level) tasks:

The Results

Our current prototypes/systems/proposals and software developed so far are:

Publications


2013-06-07 12:15