RJF's point is the one that has been on my mind as I try to come up to speed on this discussion. TeX formulae are written to generate some graphical effect; their algebraic structure is some combination of accident and good style, not anything that the language forces on the author. You can't expect to extract much more information than is there in the first place.
I have a dream of being able to write math in LaTeX and have "the system" "just know" what I'm talking about, kind of like what was envisioned for things like Isabelle/HOL and Proof General, but actually usable.* A model of computation in which symbols accumulate properties by assumption, proof, and calculation and any unproved assertion creates a proof obligation and gets flagged like a spelling error. I don't expect to be able to do it without adding some syntactic sugar, though. * - I haven't looked at these interactive proof assistants (or their descendants) in about six years, they are probably better now than they were then. I am looking forward to playing with PyKE on top of Sage, for planning large-scale computations first, but the idea of using it for proving stuff is on my mind too. I haven't seen much about logic in Sage yet, but I haven't spent much time looking yet either. -- To post to this group, send an email to sage-devel@googlegroups.com To unsubscribe from this group, send an email to sage-devel+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org
