Bridging the gap between the human mathematical language and unambiguous computer representations

This project will improve capabilities for converting between the common mathematical language (CML), the mixture of natural language text and symbolic formulas of human-written mathematics, and unambiguous computer representations of mathematics suitable for use in computer systems for mathematics (CSMs). Existing CSMs generally treat the textual portion of mathematics as uninterpreted blobs of data. Computer proof assistants (e.g., Isabelle) have the potential to represent the semantic content of CML texts, but are hard to learn, have input languages that are quite distant from CML, and have generally committed to technical choices (in logics, types, and foundations) that can conflict with the choices made by a CML text. This project aims to bridge the gap between CML texts and the input languages of proof assistants by developing (1) software and methodology for parsing and disambiguating CML, (2) unambiguous representations for recording the results of this parsing and disambiguation, and (3) connections between these representations and proof assistants. Research will investigate questions of how best to resolve ambiguity and determine bindings, what discourse representation formalism or logic is most suitable, how best to handle implicit information, and a number of other issues. The work will build on recent progress in grammars for CML, types for CML, dynamic parsing, discourse representation logics, controlled natural languages (CNLs) for CML, and machine learning for searching CML. We will develop new techniques for using partial proving for disambiguation and new representations for disambiguated CML. Many of the pieces are already available and a PhD-sized work package has good potential to overcome obstacles and put them together. The expected results have the potential to make many CSMs more accessible and could enhance the production and use of mathematics in many ways.