On 12 Jul 2012, at 16:06, Julian Bradfield wrote:
> 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.
Yes, I posted before here some example of people using it.
> 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.
Latest version requires STIXFonts to be installed. Some other proof assistants
use it.
>> 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.
TeX formulas are just for rendering. For example, if you want to have
superscript to the left, you have to write ${}^x y$.
Hans
