Hacker News Reader

Comment by TelmoMenezes | Hacker News Reader

> 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.

View on HN

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.

>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.

> 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