Hacker News Reader

Comment by darkxanthos | Hacker News Reader

I like how the author mentions having an executable mathematical language might be helpful. Math is a non-standard non-machine-executable programming language which means it's inherently buggy. On top of that, now I need to interpret the "code" while I'm learning and it can be pretty dense.

Much like in programming, I'm sure expert mathematicians may not see why it's so painful, but wait until a more robust language/system is developed for the hobbyist. It will be extremely disruptive.

View on HN

What? Due to the Curry-Howard Correspondence, mathematical proofs are in fact very precisely executable: http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...

There may be lots of room to improve the "UI" of math [0] but I don't see how you could desire more power or verifiability than what modern mathematical proof systems offer.

[0] http://worrydream.com/KillMath/

Only proofs in 'constructive' logic. There's a lot of proofs that aren't executable. Most importantly proofs by contradiction.

See: http://en.wikipedia.org/wiki/Intuitionistic_logic

In practical terms, however, this isn't a huge hurdle and comes with the nice advantage that you always have a program.

BTW. I'm kinda sure you know this already, but I think it is important to mention.

Thanks for the Haskell proof-book link. I'll check it out sometime.

Hmm, I don't understand the problem. There is a philosophical question there, of course, but as long as you assume something like the law of excluded middle, you can easily set up a proof system allowing you to execute proofs by contradiction. This is a common strategy in Coq, for instance.

Maybe I'm not understanding your point, though. I also don't think this chain of conversation is the sense that darkxanthos meant, either :)

The idea is that the Curry-Howard isomorphism allows you to "play" with constructive mathematics easily. For example, consider the fact that the composition of two functions f and g is continuous if each function is continuous. Suppose f : X -> Y and g : Y -> Z. Then, in pseudo-Haskell syntax, we could say

  continuousf  : Open set in Y -> Open set in X
  continuousg  : Open set in Z -> Open set in Y
  continuousgf : Open set in Z -> Open set in X
  continuousgf = continuousf . continuousg

The idea is that the fact that f is continuous means that we can produce open sets in X given open sets in Y. Now, consider the fundamental theorem of algebra over complex numbers. This says that any polynomial with complex coefficients with degree greater than 0 has at least one complex root. We'd like to have a function

  fta : Polynomial P of degree >0 over C -> (Point x in C, proof that P(x)=0)

which would compute this root. But the thing is, the standard proof (e.g., by Louiville's Theorem) of the FTA is not constructive. The proof is by contradiction: Suppose there were no root. Then we violate some principle of complex analysis that we know is true (Louiville's Thm, or Maximum Modulus Principle, for example). Thus there must be a root.

But this doesn't tell us at all how to compute the root! So instead we need a constructive proof of the FTA in order to produce a root.

So, the idea is that you can't "play" with non-constructive mathematics in programming as you can with constructive mathematics. Our standard FTA proof would look like

  fta : Polynomial P of degree >0 over C -> Exists x. P(x)=0.

But the type of the object that this function produces isn't very fun to play with. We have no idea what the root is!

I think this is unfair: you're comparing a trivial observation to a nontrivial theorem, and complaining why the complicated thing isn't as easy to play with as the trivial thing.

The Curry-Howard isomorphism really doesn't add anything to the conversation that wasn't already there. Mathematicians already know what it means for a proof to be constructive or not constructive, and they know it's easier to work with constructive proofs.

Besides, we already know that there is no general way to compute roots of arbitrary polynomials using elementary arithmetic. What you really want is a procedure to find a description of such an x (to arbitrary accuracy, disregarding efficiency), and these are a dime a dozen.

> Mathematicians already know what it means for a proof to be constructive or not constructive, and they know it's easier to work with constructive proofs.

It is often more easy to prove that some object exists (by contradiction) than to construct such an object.

For example: by applying Zorn's lemma it is easy to prove that any vector space has a Hamel basis. But it is often non-trivial to construct such a basis.

> Math is a non-standard non-machine-executable programming language which means it's inherently buggy.

I don't understand what you mean by non-standard. I can't think of any language more standard than mathematics.

Mathematical theorems are formally proven. That is a higher form of knowledge than empirical validation (running programs against tests). Another case of empirical validation is scientific experimentation. It validates theories by increasing our assessment of their plausibility, but never up to 100%. Mathematical proofs are the only completely objective form of knowledge. Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems.

>I don't understand what you mean by non-standard.

Symbols in advanced math tend to be very poorly defined and contextual. Imagine programming if every function had a two-letter name and the list of which packages to import was left out half the time.

This is covered in the article.

Proofs formatted for automatic solvers show that they can be standardized. Now think about the tiny percentage of proofs that are in this form.

> Proofs formatted for automatic solvers show that they can be standardized. Now think about the tiny percentage of proofs that are in this form.

Just as important, though, is the number of proofs that anyone would want to read in that form. I can't think of anyone who has ever claimed that reading formally verified proofs aids understanding...

Right, the current methods are probably awful for reading. It's a proof of concept more than anything, when it comes to using standard terminology.

Mathematical theorems are formally proven.

It's formal compared to colloquial english, but completely vague compared to computer programs.

There are automatic theorem provers, but it isn't Godel's undecidability theorem that limits them. It's the difficulty of formally writing down our proofs in machine readable format that limits them for practical purposes.

Mathematical proofs are completely precise, that is to say, not vague in the least. They are, however, in an extremely high-level language; it's left to the reader to expand the notation enough to convince themselves of the validity.

(And, of course, there can be bugs - that is, mistakes - but there is no ambiguity.)

So the underlying ideas are precise, but they're expressed in imprecise language? That's true of all communication.

When I ask my wife for "that thing by the door," I know exactly what I mean, but she has a to do a lot of work to decode it.

> Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems

Human mathematicians are equally limited by Gödel.

Reply on news.ycombinator.com