Hacker News Reader

Comment by a3_nm | Hacker News Reader

I do not find that the article insists strongly enough on the fact that computer-aided verification of proofs is not, in any way, a threat to human creativity in mathematics.

You can just understand proof assistants as an effort to design a language for mathematical proofs, and a procedure to verify them mechanically. (Spelled out like this, it sounds a lot like Hilbert's program -- we have just understood since then that you cannot hope to have a "perfect" proof assistant.) The availability of computers means that you can actually implement the verification process and run it, but if you do not want to involve computers in the process (because you do not "trust" them, or whatever), you could always check such proofs by hand, in principle.

In a sense, a proof designed for a computer assistant is one that can be verified without any intelligence required from the reader.

View on HN

This quote sums it up pretty well:

> Voevodsky himself is careful to distinguish the various ways computers should or shouldn’t be put to use. “Lots of people don’t understand the difference between using computers for calculation, for computer-generated proofs, and for computer-assisted proofs,” he says. “The computer-generated proofs are the proofs which teach us very little. And there is a correct perception that if we go toward computer-generated proofs then we lose all the good that there is in mathematics—mathematics as a spiritual discipline, mathematics as something which helps to form a pure mind.”

The recent financial crisis shows even those who claim to understand the math, do not, let alone even being able progress on probability (hmm what are the odds all this could go wrong? Nah).

More accurately you might say that the people who understand the math are somewhat segregated from the people who make the decisions.

I keep hearing/seeing statements like this when that is not the case. Models are inherently simplifications of the real world. I don't think the problem was with the math or anybody's understanding of it but more a result of the innate complexities of the market. The people at Goldman Sachs for example maybe knew about their exposure to the mortgage backed securities but they were unaware of the exposure of all the other firms in the industry. Also, a number of people expected and made a lot of money from the crash, although nobody expected it to be as bad as it was (again nobody had an accurate gauge of the exposure), it's not a lack of intelligence that drove firms but greed they were making so much money that they considered it foolish to stop and think what would happen and based on the aftermath they really have no incentive to. They suffered for a while but the government made every effort to assist them and now a few years later the market is back to record highs until the next inevitable crash.

Reply on news.ycombinator.com