[Axiom-developer] mizar

[root]

My name is Tim Daly. I'm the lead developer on the Axiom project.

Axiom is a free, open source, general purpose computer algebra system
similar to Mathematica and Maple. It was originally developed at IBM
Research starting in 1973. It was later sold to NAG (Numerical Algorithms
Group). Axiom was a commercial product until 2001 when it was withdrawn
from the market and released as free software under the Modified BSD license.
The current home page is:
http://savannah.nongnu.org/projects/axiom

Axiom consists of many hundreds of algorithms, many of which are 
implementations of research level mathematics. Many of these algorithms
cannot be understood without reading the associated research papers.
Currently the research papers are in libraries, journals, or proceedings.

We have been discussing ways of combining the research with the executable
code. Knuth has recommended a style called "literate programming" which
combines TeX files with special tags that embed the source code. This
would allow us to keep the research paper with the implementation code.
Dr Carlo Traverso is looking at developing a specialized journal in
computational mathematics that would accept articles written as literate
programs.

As computers begin to have a larger impact on mathemtatics there will
be a subset of mathematics, which I call computational mathematics,
which can only be performed by computer. We need to develop formal
ways of handling the mathematics and its associated computational
aspects. In particular, we need to develop machinery (similar to
your Mizar syntax) that allows the computer to access and manipulate
the mathematics as well as the algorithms.

I've been looking at your Journal of Formalized Mathematics. It appears
that we have areas where our goals overlap. For instance, in the paper
"Introduction to Turing Machines" there is a description of turing machines
which can easily be reduced to executable code. I notice, however, that
it does not include the code. Traverso's Journal would extend the article
with such code.

If you have any interest in considering cooperative efforts (such as
extending the Mizar syntax to allow executable code) please let me know.

Tim Daly
address@hidden
address@hidden