The project described on this page details a substantial part of a greater vision in the context of the FMathL - Formal mathematical language project described at http://arnold-neumaier.at/FMathL.html
The MathResS project will create foundations for an automatic mathematical system that combines the reliability and speed of a computer with the ability to perform at the level of a good mathematics student, with respect to mathematical knowledge and proofs, the ability to understand ordinary mathematical language and to solve standard exercises, the ability to organize mathematical information, and a searchable database of mathematical knowledge, so that it provides support for professional researchers in mathematical routine work.
To achieve this, we start with mathematics as mathematicians practise it, with their language, their editing tradition, and their informality; aiming at organizing mathematical content in computer-supported and community-supported ways, and integrating existing proof systems as they are without focusing on their development. We develop a formal model and a corresponding computer implementation of the social aspects of doing and communicating mathematics.
The MathResS project will create a multilingual, self-learnimg, easy-to-use system for the formal representation and use of mathematics on a computer that mathematicians and scientists using mathematics as a tool will like to use because it provides mathematical contents and proof services as easily as Matlab provides numerical services or Mathematica provides symbolic services, in a way that does not take undue amounts of time on their part. Moreover, the MathResS system will be efficient in supporting the mathematical modeling of real life applications involving large-scale scientific computing, by interfacing it to established problem solving environments at different levels of mathematical rigor.
These benefits will begin to be available long before the full capability of the system is reached, thus making it attractive to mathematicians to contribute to its development during and beyond the project duration by a web-based participation under a wiki-like construction.
For a detailed view of the proposed MathResS project see MathResS: A mathematical research system
Here is a project thesis going the first steps in this direction:
K. Kofler, Dynamic Generalized Parsing and Natural Mathematical Language, Ph.D. thesis, Faculty of Mathematics, University of Vienna (2017).
Here are some of related pages:
Mathematical reasoning, a bottom-up approach
An automatic mathematical assistant - a vision
What would you want from an automatic mathematical research
assistant?
Dozens of replies to some questions I had posed in various electronic
communities
Quotes on formalized mathematics and automatic mathematical assistants, collected from the Web
The FMathL mathematical framework
Arnold Neumaier (Arnold.Neumaier@univie.ac.at)