An automatic mathematical assistant - a vision
Arnold Neumaier, Vienna
February 27, 2009
http://www.mat.univie.ac.at/~neum/FMathL/vision.txt
This file is part of the FMathL web site at
http://www.mat.univie.ac.at/~neum/FMathL.html
This is an outline of a very ambitions long term project.
The long term vision is to create an automatic mathematical assistant,
that is able to perform at the level of a good undergraduate student
of mathematics, both with respect to mathematical background knowledge
and with respect to capability of understanding ordinary mathematical
language and the ability to solve standard exercises. Moreover, the
assistant should be efficient in supporting the mathematical modeling
of large-scale real life applications.
This would enable mathematicians using this system
- to check their own work for correctness,
- to improve the quality of their presentations,
- to decrease the time needed for routine work in the preparation
of publications,
- to quickly and reliably remind them of work done
- to produce multiple language versions of their manuscripts
- and ultimately to quickly disseminate fully checked results to
other users of the system.
Thus such a system will have a high value for every mathematician.
It would also enable visually impaired people to use the system and
its mathematical contents.
It is planned to create the system in such a way that these benefits
will begin to be available long before the full capability of the
system is reached, thus making it attractive to mathematicians to
use it and to contribute to its completion.
A successful automatic mathematical assistant requires the creation of
a database system for storing mathematical theory that
- contains a formal representation of the mathematical theory at the
undergraduate level; at least naive set theory, linear algebra,
real analysis, basic algebra, and basic numerical analysis;
- ... and much more theory as the system grows;
- allows the systematic storage and retrieval of mathematical concepts
propositions, and proofs;
- is fairly independent of notational styles, input language, and
underlying mathematical or logical foundation;
- allows conceptual and structural search;
- a standardize transfer language for communicating database contents
between different database instances and to standard formats like
MathML,
- has a versioning and backup/restore system for safe upgrading, etc.
- contains external links for background information, authorities for
reference, further explanation.
- get automatic upgrades from an official web site.
It also requires algorithms for
- reading and interpreting mathematical text specified in a LaTeX-like
fashion (which is as close to natural mathematical language as
possible),
- displaying contents in natural mathematical language, if possible in
different styles and/or languages,
- restructuring mathematical contents according to specific goals,
- comparing different sections of mathematical contents with respect
to structural similarity and common information,
- verifying the semantical meaningfulness of mathematical contents,
- verifying the logical correctness of proofs given the validity of
auxiliary results used,
- pointing out gaps and errors in proofs,
- finding counterexamples of, from a human point of view, obviously
wrong statements,
- automatic calculation of routine computations,
- hierarchical arrangement of mathematical material in way
comprehensible by humans,
- meaningful handling of mathematically similar fragments of
theories,
- automatic recognition and formation of special cases and
generalizations,
- heuristic evaluation of the quality of mathematical contents
w.r.t. given goals
- heuristic decision making for how to reach assigned goals
It also requires an analysis and efficient formalization of the social
process by which a student acquires the capabilities
- to read and understand mathematical contents,
- to verify proofs, arguments given in a book or by a lecturer,
- to guess from context the meaning of ambiguous formulations, and to
check whether the guessed interpretation is consistent with the
context,
- to ask sensible questions clarifying items that are not
well understood or seemingly ambiguous,
- to relate mathematical contents to one's own understanding, and
to classify the material accordingly,
- to recognize the need to learn more about a concept, and to find
out where the required information can be found,
- to respond sensibly to statements commenting on current performance,
- to answer questions regarding its understanding and knowledge of
mathematical theory,
- to formulate meaningful plans for proceeding in a more complex
task,
- to assess the quality of an argument or proof and to suggest
sensible improvements,
- to adapt to its partners in communication by selecting an
appropriate level of detail or overview,
- to recognize particular styles of presenting mathematics,
- to recognize the existence of hidden assumptions, assumed
terminology and notation, etc.,
- to recognize and use preferred but not binding notational
conventions,
- to integrate notation, concepts, algorithms, or proof methods seen
repeatedly or formally described into its knowledge base,
- to recognize minor glitches in spelling or sloppiness in notation or
handling degenerate cases,
- to recognize that variations of the same statemnt say essentially
the same thing, or to be able to say how they differ
It also requires a flexible and easy to use human-machine interface,
in particular
- a TeXmacs like editor for creating mathematical contents, for
editing mathematical manuscripts for publications,
- a batch mode for the automatic interpretation of mathematical
textbooks, and their incorporation into the database,
- a facility to easily inspect and edit the database,
- graph based techniques to understand the interdependence of the
contents of selected parts of the database,
- a dialogue system for communication with the user; both the system
and the user must be able to ask and respond to questions by the
other side,
- web based interaction tools to allow remote users to contribute to
the growth and quality of the database contents,
- automatic synchronization tools between different instances of the
database.
To guarantee the highest possible level of reliability, all
mathematical units of content are assigned signatures containing
information about what is assumed to be able to trust the statement.
(A signature may say, e.g., ``from Bourbaki's Elements'',
``imported from PlanetMath'', ``verified by the proof assistant HOL
light on the basis of ZFC'', ``by an approximate Matlab calculation'',
``based on the Riemann hypothesis'', or ``unverified claim by
user xyz''.)
There must be a trust propagation and verification system that
recognizes on which assumptions a given assertion is based and, given
definition of what is trusted, points out all the untrusted links in
existing verifications together with their signatures. This enables
users to specify or even to experiment with the amount of trust they
are prepared to put in various sources of information and deduction
systems.
Users interested in increasing the quality of the system can also
discover theories with important gaps on certain trust levels, and
work towards closing these gaps.