Hacker News Reader

Comment by cschmidt | Hacker News Reader

I don't know about the OP's point on the value of proof to programmers. I do optimization and machine learning, and I use all kinds of math on a regular basis. But I don't prove things, and rarely need to follow someone else's proof either. You can get a lot out of applied math without touching a proof. And if it isn't applied, then you really don't need it ;-).

I agree there is value in learning how to read math notation, so there is a valid point in there somewhere.

View on HN

An analogous case is the programmer who relies on libraries and abstraction and "knows just enough to be dangerous." Statistics and optimization mathematics in particular are vulnerable to this. If you haven't read the proofs or you cannot prove it yourself, then you truly don't understand it. I'm not claiming this is you since your post doesn't imply that.

However as an example, if someone is solving linear or non-linear programs using <insert software or library here> but hasn't bothered to thoroughly study the mathematics underlying either and is just plugging in numbers from the constraint equations they came up with, then I would not want that person doing any sensitivity analysis. There would just be no way to be confident that they are interpreting the results correctly.

I've benefited from lots of theoretical classes, and you're absolutely right that you need to understand the theory of what you're doing. For example, I took a lovely class from Prof. John Hooker (at CMU) that derived Linear Programming duality as a natural consequence of Farkas' Lemma, rather than just mechanically grinding through LP tableau. I certainly followed the proofs discussed in many classes.

However, I can honestly say I got that understanding without doing hardly any proofs of my own. Graph theory was the only class where I "did proofs", and I didn't find it my favorite. (Later I did algorithmic graph theory and network flows - and that was fantastic, with no proofs.)

I guess my point is just that an engineer can understand and use a lot of pretty advanced math without spending much effort learning about proof techniques. That certainly wouldn't be how I'd spend my time. (Of course, if you enjoy doing that then knock yourself out.)

Just because you don't explicitly write it down doesn't mean you didn't prove something. For optimization, you have to prove to yourself that the new code behaves equivalently to the old code. Anytime you use algebra you're doing a small proof to show that two expressions should be treated equivalently. Writing a proof down is the very last step, the hard part is thinking it through.

I do derivations all the time. I just do a series of algebraic transformations, starting from what I have, and getting to what I need. Some might say that I'm doing a proof. But I never use proof by contradiction, contrapositive, induction, or proper proof techniques.

Doing a derivation like that is sometimes called a proof by "chaining if and only ifs", though that's far from a standard name taught to students. It's basic, but most certainly a required method of proof to come up with convenient formulas.

You are restricted by the set of tools you already have right?

I can't believe how many times a great advancement in theory in different field comes from pure math advancement (or applying pure mathematical results). Say in economics, if Nash didn't apply topology, how would one ever know Nash equilibrium exists. Stable matching, compressed sensing and others also comes to mind.

I have a hypothesis that any field would benefit if we introduce some pure mathematicians to them.

To be completely honest, the more common case is that the mathematicians follow behind physicists and engineers to verify that their applications are theoretically sound. But yes, great breakthroughs do come from pure theory.

I think that theorems are just like libraries you can pull in for your purposes, and the proofs are the unit tests that you can dive into if needed ;) !

In the sense of http://en.wikipedia.org/wiki/Curry–Howard_correspondence, the theorems are the type signatures of the API, and the proofs are the implementations!

Reply on news.ycombinator.com