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.