On 10/3/09, markus schnalke <mei...@marmaro.de> wrote: >> otoh it would be nice if maths had a plain text representation with a >> proper formal language, well defined scoping rules, semantics.. and if >> one came up with a new construct he would define it inside the >> language > > Reminds me much of `eqn', which AFAIK provides all of this. >
no, i was thinking about a bit different thing there in eqn one cannot define axioms which later could be used for formula correctness verification eqn is good for typesetting formulas, but it's not good as mathematical notation for the digital age. it is important to be able to express the semantic meaning behind the symbols. a good language would make the processing of the formulas possible (static analysis to catch errors, search for certain constructs/patterns, evaluate formulas, describe proofs in a verifiable way, render formulas nicely..) coq, isabelle, mizar, metamath, acl2, agda.. is closer what i was thinking
