'Planeliner' by Simon Thomas
The Activities of IMKT are long-term projects which work towards the goal of providing greater access to mathematical knowledge. This will be done by employing new technology to organize and provide navigation within mathematical knowledge in ways that a traditional print library cannot aspire to.
The following four initiatives were explicitly mentioned in the first proposals for setting up an IMKT.
The goal of SFC is the formulation and communication of semantic information in a way that promotes interoperability of math.
The use of Special Functions is among the less elementary subjects that are significant in engineering and other applications of mathematics. We envisage a service that will allow the use of special functions to be even more reliable. The service will also clarify the relationships between the capabilities provided by the many existing tools.
The mathematics of a great number of special functions is so well understood that computer algebra systems, both commercial and non-commercial, offer calculation with such functions, both numerical and symbolical.
The implementations of trigonometric functions, Bessel, Legendre, Chebyshev, functions in Maple, Mathematica, Matlab, SageMath, Pari, Gap and other such systems have, to a large extent, replaced the old uses of tables and handbooks in dealing with these mathematical objects.
……….
The classic Handbook by Abramowitz and Stegun from the National Bureau of Standards has been put out in a revised edition, with an online form as the Digital Library of Mathematical Functions from NIST (National Institute of Standards and Technology). On the Web, this joined the massive online Wolfram Functions site, publicly available due to support from the commercial entity Wolfram Research, producers of Mathematica. There are also offerings from the creators of Maple, a Digital Dictionary of Mathematical Functions from INRIA in France, and other repositories of information about special functions.
This, however, does not mean that there is healthy competitive effort or that it does not matter which tools are being used. One tool might be more efficient for a particular calculation, but the mathematical facts should be the same everywhere. In truth, this is not so. There are almost as many different views of special function as there are systems treating them. They often do so without an unwitting user’s being aware of it.
There has been a sense in which it has been natural for each system—Mathematica (now the Wolfram Language), Maple, Matlab, NAG, etc. —to stick to and promote its own conventions, with little interest in comparison, or even in interoperability, with others. This is, of course, unsatisfactory in order to build the sorts of tools there should be for technology and the development of science.
……….
The GDML WG has been aware of these problems since its inception. A GDML should be able to work with mathematical knowledge in equivalent representations and to know when what was thought to be the same turns out not to be.
Two members of the WG are now on the NIST board overseeing the DLMF, and several European special function efforts have also had contact with the WG. In addition, there has been concern about special functions displayed by the OpenMath Society. The OpenMath markup is coherent at a basic level with Content markup of MathML, which was developed by the W3C (World Wide Web Consortium) and is now an ISO standard.
At the recent gatherings in Seattle (Jan 2016) and Toronto (Feb 2016), matters of concern to a GDML were worked over. Representatives of both Mathematica and Maple publicly declared their willingness to consider, in principle, working on this according their notions of specific functions. The same general support of the idea was to be heard from other parties at the OPSF13 meeting at NIST in June 2015.
NIST is suggested as a broker who is obliged by law to be neutral. One current proposal is to organize groups around NIST, working on setting down the vocabularies, definitions and conventions used to describe the well-known special functions. The groups would, in addition, record the comparisons of their various forms in such a way for tools to provide interoperability for, and integration of, the vast knowledge implicit in the various systems. We hope that an IMKT legal entity can provide a way to finesse social issues so as to get to the science and eventually provide the desired public service.
The concern of FABstracts is the (logical) formalization of mathematics that is computable.
We wish to develop a collection of formal abstracts (FABstracts), consisting of carefully captured assertions of theorems and the underlying definitions, to be recorded in a formal framework. To begin a pilot system, the proof assistant Lean is the natural framework chosen by the FABstracts Project, under the leadership of Tom Hales and Jeremy Avigad.
A full formalization of usable mathematics is something we imagine. However, we are not yet clear what can be formalized, what “fully” means outside a specific context, and there is no general agreed framework in which to formalize.
Tom Hales suggested beginning with a much smaller practical pilot project. Hales is well-known for his proof of the Kepler Sphere Packing Conjecture and related results, and then for mounting a successful 25-year FTE project to make his proofs formally machine-checkable after some felt they were beyond human understanding. HOL Light might have been a natural framework to begin in, since that carried Hales’s convincing Flyspeck project mentioned above. One good area of mathematics with which to start was thought to be geometry, since it makes different semantic demands than analysis or algebra.
At this time, writing these formal abstracts starting from extant mathematical literature is a task for educated humans – perhaps leading to automation as the process becomes better understood. An initial project would undertake the transcription of the abstracts of a selection of geometrical literature into a proof assistant’s formalism.
Once that is done, there will be an unusually well-marked up and authoritative corpus of mathematical knowledge that can be publicly displayed. Perhaps more importantly, its mathematical knowledge data can be used for experiment in providing innovative interfaces into it.
This will be a well-formulated collection of theorems and definitions that should ultimately be supported by full proofs. In the cases of Flyspeck, or of Gonthier’s analyses of the Four Color Theorem and the Feit-Thompson Theorem, a major final result had to be supported by finding proof patterns and reformulations that allowed a final complete verification. This will probably lead to a different style of corpus. In addition, this sort of effort is one that should lead to more crowd-sourcing with a wider net of volunteers, extending the starting efforts once we have found a clear way to approach the task.
There are by now overlapping pieces of mathematics, such as basic pieces of Euclidean geometry and some fundamental lemmas and theorems of analysis, that have had to be formalized in more than one system. The main systems where there is real overlap are HOL Light, Coq and Mizar.
What has not been done is to make careful comparisons of the formulations of, for example, the Jordan Curve Theorem, or the Fundamental Theorem of Calculus in the various contexts. We need to see in what sense they are really the same and in what they may differ. This is not just a matter of the way the proofs proceed, but may be about subtleties in the semantics resulting from different foundational bases.
Harrison from HOL Light, Wiedijk who has worked with more than one system, Urban from Mizar and others have expressed interest in exploring the ways these systems are the same and differ. As a practical result, the search for applicable results may be extended to a federated search over the different library collections of already formalized material with clarity over what is returned.
There are several sorts of document analysis that are possible, and these have not been applied to the mathematical corpus. Its writing is not truly linear, and it involves a large sign vocabulary. A different grammar is required by the use of formulas. There is a need for power tools for document digestion as the GDML effort ramps up, so NLP methods tried and tested elsewhere will need to be adapted to handling the mathematical corpus.
$n$-gram analysis of mathematical corpora is a relatively easy place to begin. NLP tools here are readily available for ordinary languages. Sample corpora, e.g., those of zbMATH and arXiv are readily available and their curators are interested in such ideas.
Some early experiments have been tried at zbMATH for keyword generation. Another small project was completed at ORCCA under Watt’s direction, which concentrated the $n$-grams on the mathematical formulas. It found that characteristics of different subjects could be detected. This is a much more limited approach than deep learning and needs many fewer resources. It is, however, applicable in context finding and clustering tools that can also be deployed much more easily. Other projects have also been funded by the Alfred P. Sloan Foundation using alternative statistical approaches.
