Initiatives

The following four initiatives were explicitly mentioned in the first proposals for setting up an IMKT.

SFC—Special Function Concordance

The world that uses mathematics employs many techniques that are considered well known and completely trusted in their use in technology and for general reasoning. The most basic are arithmetic and elementary algebra. Among the less elementary subjects that are significant in engineering and other applications of mathematics probably the most common is the use of Special Functions. We envisage a service that will allow the use of special functions to be even more reliable, and will clarify the relationships between the capabilities provided by the many existing tools that offer access to knowledge about them and numerical and symbolic implementations of special functions and their properties.

FABstracts

The idea is to develop a collection of formal abstracts (FABstracts) consisting of carefully captured assertions of theorems and the underlying definitions recorded in a formal framework. The proof assistant Lean is the natural framework chosen by the FABstracts Project under the leadership of Tom Hales and Jeremy Avigad to start a pilot system.


 

Formal harmony

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, say, the Jordan Curve Theorem, or the Fundamental Theorem of Calculus in the various contexts. We need to see in what sense they really are the same and in what they really 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.

Document analysis

There are several sorts of document analysis that are possible and have not been applied to the mathematical corpus which has its own special features. Mathematics is arguably a natural language of a globally distributed people (those with enough training in mathematics to do science and engineering) but not a typical one. For a start, its writing is not truly linear and involves a large sign vocabulary and there is a different grammar 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.