Comment by jordigh | Hacker News Reader

Comment by jordigh | Hacker News Reader

Parent Full thread

This is not possible, at least not without a very sophisticated AI.

One thing that novices seem to not get about mathematics, especially those coming from programming languages, is that the syntax of mathematical formulae is not divorced from the natural language that surrounds it. Different authors use different symbols for the same concept or the same symbol with different meanings. That is, mathematical symbols have synonyms and homonyms, so to speak. You can read someone's "accent" when reading mathematics. The French consider 0 to be a positive number; the Americans don't. The Russians call it the Bunyakovsky inequality, most of Western Europe and America calls it the Schwarz or Cauchy-Schwarz inequality. The way they arrange their equations, the particular details of the notation, their preferred term for a particular concept, even tiny things like preferring upright or slant font for dx in an integral (and by the way, often fonts carry semantic meaning, but not in this case); all of these vary from author to author.

Mathematics is a very human activity. It is written by humans who write ambiguous things because it's meant to be read by humans who deal well with ambiguity. Reading human-written mathematics cannot be mechanised, at least, not anymore than reading a natural language can be mechanised.

Its worse than just notational differences (which probably could be solved good-enough with crowdsourcing).

The bigger problem is that there is often not a simple English description for math terms, whose meaning might involve understanding concepts that take books to explain.

For example, consider the simple sentence "Let x be an arbitrary vector". What is a vector? There is no clear answer to this question. Formally speaking a vector is simply an element of the set V where V is the underlying set for some vector space. You could try to say that V is an ordered pair of n real numbers, which is true up to isomorphism for finite dimensional vector spaces over the real numbers. But, x could also be the function f(x)=x^2, or the matrix [3, 4; 7, 1+i]. In some contexts, the translator might be able to tell from context what vector space is being worked in. But if the source is a general statement about vector spaces (even if made in support of a more concrete point), there is no way to explain it without explaining the concept of a vector space. To explain vector spaces one would need to, at a minimum, explain fields.

There is also a question of which description to use. For example, suppose we needed to define complex numbers. In some contexts, it is most natural to think of them as points on the xy-plane, which is simple enough (although does not give intuition above what multiplication means, which is arguably an essential component of the "true" meaning of complex numbers). In other contexts, it is more natural to think of them as matrices of the form [a -b; b a]. Attempting to show all the (equivelent) meanings would likely overwhelm the intended user of the service.

if this is the extent of your difficulties when reading mathematics, I don't think this article is for you...

It would certainly be possible if mathematics standardised on writing proofs in a proof assistant like Coq. Then anyone with a basic functional programming background could understand the most complex of proofs, given enough time to step through and understand all steps of the proof in the Coq IDE.

Most mathematical proofs translate quite badly to formal languages. Their formulation often relies strongly on the peculiarities of language.

Consider the "it's easy to see that" from the article. There is no translation of that into a formal language beyond either introducing the claim as an axiom, or actually providing the proof. It also means that every usage of a well known theorem needs to be explicitly mentioned.

The end result would be an incredibly verbose proofs. Moreover, the verbosity of the proof wouldn't relate very well to the complexity of the idea behind the proof. This might bloat rather simple or elegant proofs, and us mathematicians really like our elegant proofs.

Put another way, this would require writing down a lot more than the epiphany that lead to the proof.

In general, it might be nice to somehow make proofs more tree-like rather than linear. That is, show the proof from the highest level, and allow a reader to 'expand' the claims to see their proofs. Down to the 'leaves' which are considered obvious.

You would be trying to reverse a couple millenia of mathematical tradition if you wanted to convince all mathematicians to only write machine-readable mathematics. As appealing as the idea may sound to computer people, mathematicians would find it quite repugnant if they were no longer "allowed" to write mathematics in a casual style (as if it were even possible to forbid them from doing so).

That would also require re-doing all of mathematics in a constructive setting, which is a great idea as far as constructivists are concerned but it has both political and technical opposition. It's also the case that a proof in Coq doesn't have to be enlightening, especially if you discharge it with some inscrutable hammer-like custom-written pile of LTAC.

How do you deal with those problems when developing Octave? Do you stick to one 'dialect', for example? Or is it somehow a non-issue?

Exactly.

And in machine learning idiots mix lambda for hyperparameters and eigenvalues....

When you have a functional programmer in the audience...

http://aix1.uottawa.ca/~jkhoury/2006_09.jpg

Reply on news.ycombinator.com