On 2012-07-12, Hans Aberg <[email protected]> wrote: > On 12 Jul 2012, at 12:33, Julian Bradfield wrote: >> In practice, no working mathematician is going to use the mathematical >> alphanumerical symbols to write maths in (La)TeX, because it's .. >> the Unicode mathematical symbol model does not match how one uses >> mathematical symbols. > > It is used by proof assistants such as Isabelle, and also in logic. > https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
No it isn't. Isabelle uses (essentially) TeX control sequences internally, though it writes them as \<oplus> rather than \oplus . A small number of these are mapped to Unicode code points for display and input purposes, and that small number does not include any of the mathematical alphanumerical symbols block. > If your only objective is to achieve a rendering for humans to read, TeX is > fine, but not if one wants to communicate semantic information on the > computer level. On the contrary, computers are very happy with TeX notation. There are several useful mathematical online learning sites (such as, for example, Alcumus) which use TeX syntax to interact with the students. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
