From: Harald Hanche-Olsen on 10 Apr 2010 09:22 + pjb(a)informatimago.com (Pascal J. Bourguignon): > Harald Hanche-Olsen <hanche(a)math.ntnu.no> writes: > >> + His kennyness <kentilton(a)gmail.com>: >> >>> Aha! jsMath!! You just changed my life. >> >> Then take a look at its successor-to-be: http://www.mathjax.org/ > > Yes, that's the problem with all these "nice" "intuitive" GUI tools: > they always have a successor, so you are always switching and learning a > new one. Eh? Did mathjax suddenly morph into an intuitive GUI tool while I wasn't looking. Strange. > Those who are not left with much time prefer to stick with efficient > stable tools, such as emacs or lisp which have been basically the same > for 30 years, so that we can concentrate on _our_ work, not on the job > of making another software enterpreneur rich or flattered. Or TeX. You hardly get any more stable than that. Come to think of it, that is what jsmath and mathjax do: They let you type TeX code and have it transformed into readable math on a web page. Mathjax is just a better implementation of what jsmath does, and both try to do for the web what TeX did for paper. I take it you don't approve of Lisp implementations that haven't been around for 20 years or more either? -- * Harald Hanche-Olsen <URL:http://www.math.ntnu.no/~hanche/> - It is undesirable to believe a proposition when there is no ground whatsoever for supposing it is true. -- Bertrand Russell
From: Xah Lee on 10 Apr 2010 10:57 On Apr 10, 5:53 am, m_mom...(a)yahoo.com (Mario S. Mommer) wrote: > p...(a)informatimago.com (Pascal J. Bourguignon) writes: > > What about if you merged LaTeX with an automatic proof checker? > > That would have to be one hell of a proof checker! It would have to > understand natural language, and know what can be "safely assumed" as > being implicit, given the audience. It has to be that way because a > maths paper written like a formal spec of something is not going far, > because of its intrinsic wetware incompatibility. The referees will > absolutely hate you for it. And then you get the "way too technical" > rejection. Which is a good thing, because if such a paper were accepted, > nobody would read it. > > In short, that automatic proof checker has to be a really damn good AI, > of the type Lisp was originally concieved to make happen. > > I mean, I'm all for such a program, but I'm a tiny bit skeptical :-) it is impractical for TeX to be merged into a proof checking language. I mean, if it happens, the result would really have nothing to do with TeX. However, the idea of combining a system that can display math formulas and proof checking, or with a so-called computer algebra system, and also as a computer language, is a common need, and has in fact been done to various degrees. Mathematica for example, is one. While, most computer algebra systems (such as Maple), or any math tools used in physical sciences, all have a math formula display system builtin to some degree (MatLab, Sage, MathCAD...) for more detail of this, see: ⢠Math Notations, Computer Languages, and the âFormâ in Formalism http://xahlee.org/cmaci/notation/index.html Xah â http://xahlee.org/ â
From: Tim Bradshaw on 10 Apr 2010 12:42 On 2010-04-10 11:10:41 +0100, Pascal J. Bourguignon said: > What about if you merged LaTeX with an automatic proof checker? Given the extreme imprecision of a lot of mathematical notation (obviously not as used by people who are very precise, but as used by physicists, say), I imagine the sheer labour of having to enter everything in a semantically precise way would kill such a thing dead.
From: Tim Bradshaw on 10 Apr 2010 12:48 On 2010-04-10 11:37:53 +0100, Pascal J. Bourguignon said: > Yes, that's the problem with all these "nice" "intuitive" GUI tools: > they always have a successor, so you are always switching and learning a > new one. While that's true (and it kind of annoys me that I might now have to get Mathjax integrated into TW), this really should not be a problem here. Both of these things ought to be able to let you write baically $...TeX...$ (or $$...displayed TeX...$ in things, so what you *type* is the same.
From: Robert Uhl on 17 Apr 2010 17:56
m_mommer(a)yahoo.com (Mario S. Mommer) writes: > > In my experience, writing directly to TeX or anything similar is asking > for trouble unless you are doing simple things. The source is not all > that readable, and the hardcopy looks too good. The result is that you > do not see the mistakes and the holes in the arguments. Taking a draft > on paper and cleaning it up by copying the non-strike-out to new a paper > draft is the only really good way to make sure you are really really > really going over every detail again. That doesn't just apply to mathematics, though--that applies to anything written. Those who know me have read or heard the following tale many, many times before, but it might be interesting to those who haven't: When I was in high school and my early years of college, I wrote papers the same way everyone else did: by typing into a word processor (whether Microsoft Word, Nisus Writer or something similar). My papers weren't _bad_, but reading them now none were particularly _good_ either. My senior year, I chose to write all my papers by hand, starting from an outline, then rewriting it fleshed out a bit, then rewriting again, and so on until I had a finished paper, all written longhand. Then I'd go home and typeset it with LaTeX. I didn't get less than an A that year. The difference was night-and-day. -- Cinder blocks: $100 Mortar: $30 A cask of amontillado: $300 The faint screams of a desperate PHB: priceless. --O. Schwarz |