has On Apr 10, 5:53 am, m_mom...@yahoo.com (Mario S. Mommer) wrote:
> p...@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