I just stumbled across this http://www.fields.utoronto.ca/programs/scientific/15-16/semantic/ effort: Semantic Representation of Mathematical Knowledge Workshop.
I may be way outside my areas of competence here, but this calls to mind some of the discussions on P6. Is there value in trying to get some input to the process?
