[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] notes on isabelle vs. mizar



Hi guys,

Josef Urban wrote:
ASCII editors are not good tools for
presenting or authoring mathematics, formalized or
not.

I would agree with presenting, authoring is a different matter. The Mizar team even went from nonASCII-allowed to ASCII-only couple of years ago for purely practical reasons, and people got used very quickly to "in" instead of the \epsilon character.
Josef, Slawomir is right. For authoring mathematics: still a blackboard or sheet of paper rule:)))

Of course, ASCII editors for writing less-formal (or as you prefer non-formal) mathematics in LaTeX are the most popular. This is the one and only way to do this since this is what journals accept. Even if some crazy guy uses tools like ScientificWorkPlace, he ends up correcting the source using notepad in order to meet the journal requirements (I really know some of these guys).

I think that this might change over time, e.g. with good Unicode tools (in this sense XSymbol is still ASCII, which is good).

But then someone has to create a special keyboard for writing maths;) These things would be great. So far auctex mode in emacs has to do the trick for me.

Bartek