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.