options if Latex is the basis

Latex is the representation of Math that everyone can agree is common across domains. There is also consensus that Latex is inadequate for formal math.

Brainstorming possible methods of leveraging Latex,

• Having authors use semantic markup (e.g., sTeX) when creating documents.
• After documents have been created, perform bulk analysis (arXiv corpus) to extract semantics. After separating text from math in a given document, tasks are to (identify article text as theorems or claims or lemma) and (identify parts of expressions in math Latex using either a grammar or machine learning).
• After author has written document but before they share it, the author uses software to categorize sections of text and identify parts of expressions. (This requires an addition to existing workflows, creation of novel software, and reliance on novel grammars or ML algorithms.)
• Instead of authoring Latex in a text editor or GUI or OverLeaf, author the content in a CAS (e.g., Sage) and generate the .tex from the CAS. Here the CAS is serving as a Latex editor, constraining what's allowed by or required from an author. While CAS software can generate Latex output, using a CAS as a Latex editor isn't standard. 

dynamically build latex parser grammar based on symbols used in the Physics Derivation Graph

I've been using the Sympy Latex parser. After encountering a wide variety of issues, I realized a new strategy is needed.

The previous mindset was "make modifications to the ANTLR grammar as we encounter novel issues in Latex." That approach would constant process of catching up with whatever is in the Physics Derivation Graph.

Here is a different method that takes advantage of the information available in the Physics Derivation Graph to inform the ANTLR grammar.

The Physics Derivation Graph has a list of symbols in its database. We could leverage that list of symbols and build an ANTLR grammar specification that is based on the Physics Derivation Graph list of symbols.

The process would be

1. get list of symbols from Physics Derivation Graph
2. add those symbols into the ANTLR grammar
3. when Sympy parses Latex, use the modified grammar specification
4. when new symbols are added to the Physics Derivation Graph, go to step 1

from Latex to Abstract Syntax Tree

In the latest revision to the Physics Derivation Graph, the tuple (unique expression identifier, latex expression) has been replaced with (unique expression identifier, latex expression, abstract syntax tree). This is similar to the split between "presentation MathML" and "content MathML." This distinction requires a translation between a (visually pleasing and easy to input representation) and (a mathematically meaningful representation).

Latex will be input by the user for the PDG; the user will not need to supply the AST as input. To validate a step, the AST is needed. This presents a few challenges:

• Is the input valid tex?
• Is the valid tex a mathematical expression?
• Is the valid mathematical expression consistent with the step? 

A step in a derivation is defined as the application of a single inference rule with one or more expressions as input, feed, or output.

There are a few options for parsing mathematical tex: 

• write a custom parser 
• use an existing parser, e.g. MathJax