Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

New math book rescues landmark topology proof

quantamagazine.org

Post reply on HN
Print view View original

31–40 of 171 posts

Re: New math book rescues landmark topology proof

#31

Post by lostmsu »

roywiggins wrote: post #25
lostmsu wrote: post #11

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? P.S. Reviews are still needed to check novelty etc.

> Why don't serious math journals require programmatically checked proofs for all publications Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer th…

This sounds like a very dangerous attitude, considering that making any tiny mistake will cause you to be able to prove any statement. Of all people mathematicians should understand that.

Re: New math book rescues landmark topology proof

#32

Post by lostmsu »

turminal wrote: post #21
lostmsu wrote: post #11

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? P.S. Reviews are still needed to check novelty etc.

Because programmatically checked proofs don't work the way you think they do. And even programatically checked proofs are still programs. And programs still need code review.

I understand that you might need a code review for the proof to look nice, but the point of a checked proof is that you don't need a separate code review for correctness. If it checks (sans internal checker issues) - it is correct.

Re: New math book rescues landmark topology proof

#33

Post by jacobolus »

lostmsu wrote: post #29
jacobolus wrote: post #19

Earlier quoted context omitted.

> Why don't serious math journals require programmatically checked proofs ... Because that would take 2+ orders of magnitude more work, and nobody has the time/attention budget for it. This is sort of like asking: why did you single person write this 10-page short story instead of making a Hollywood-style feature film?

Would it though? Are proof checkers much more complicated than LaTeX? If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.

Maybe half (?) of the basic undergraduate math curriculum has been formally verified, after decades of effort by large numbers of researchers. The proof under discussion here is significantly more complicated than anything that has ever been formally verified, as far as I understand. Disclaimer: I don’t know much about formal verification of mathematics, only what I have read from time to time on the internet.

Re: New math book rescues landmark topology proof

#34

Post by lostmsu »

qsort wrote: post #20
lostmsu wrote: post #11

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? P.S. Reviews are still needed to check novelty etc.

For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve. Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.

There are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.

Re: New math book rescues landmark topology proof

#35

Post by klyrs »

lostmsu wrote: post #11

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? P.S. Reviews are still needed to check novelty etc.

> ...what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts?

I kinda feel like this question answers itself. On the other hand, I can't imagine this quagmire lasting another century, but the machine-assisted proof ecosystem hasn't reached adolescence yet.

Re: New math book rescues landmark topology proof

#36

Post by roywiggins »

lostmsu wrote: post #31
roywiggins wrote: post #25

Earlier quoted context omitted.

> Why don't serious math journals require programmatically checked proofs for all publications Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer th…

This sounds like a very dangerous attitude, considering that making any tiny mistake will cause you to be able to prove any statement. Of all people mathematicians should understand that.

Empirically, proofs with bugs get ironed out into proofs with less bugs, and the results almost always end up standing. Why mathematical proof seems to be as good as it is at avoiding proving false statements is a matter of contention, but practically speaking it works. There's very little incentive to computer check proofs because, as a practical matter, mathematics is not plagued with false "theorems."

Computing, on the other hand, is plagued with broken programs, and formal methods are still a very specialized area, even though the potential benefits are much greater in computing than mathematics.

Re: New math book rescues landmark topology proof

#37

Post by lostmsu »

nerdponx wrote: post #16
lostmsu wrote: post #11

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? P.S. Reviews are still needed to check novelty etc.

Is it possible to even check such a proof programmatically? Do we have that kind of technology? Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?

> Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?

The point of the checked proof is that your final theorem is almost definitely correct (you did not make mistakes in your deductions, unless the proof checker has a serious bug) if you can convince computer it derives from your axioms.

You can convince humans without your proof being correct thought, because they might not spot an error.

Re: New math book rescues landmark topology proof

#38

Post by klyrs »

lostmsu wrote: post #29
jacobolus wrote: post #19

Earlier quoted context omitted.

> Why don't serious math journals require programmatically checked proofs ... Because that would take 2+ orders of magnitude more work, and nobody has the time/attention budget for it. This is sort of like asking: why did you single person write this 10-page short story instead of making a Hollywood-style feature film?

Would it though? Are proof checkers much more complicated than LaTeX? If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.

> Are proof checkers much more complicated than LaTeX?

In terms of lines of code, no. In terms of the learning curve, yes -- latex does a very good job of getting out of the way and letting a mathematician just write in English, where proof assistants require rigid structure that doesn't remotely resemble how (most) mathematicians think. In terms of runtime, oh my god, get out of town.

Re: New math book rescues landmark topology proof

#39

Post by phaedrus »

The part I find most interesting is that (as I understand the article), Freedman's proof relies on a meta-proof that details not worked out in the base proof could be ignored:

"But there were places where he couldn’t quite complete the picture — as if he were creating a portrait and there were some aspects of his subject’s face he couldn’t see. His last move, then, was to prove that those gaps in his picture — the places he couldn’t see — didn’t matter from the standpoint of the type of equivalence he was after. That is, the gaps in the picture could not possibly prevent the Casson handle from being homeomorphic to the disc, no matter what they contained."

Re: New math book rescues landmark topology proof

#40

Post by mahogany »

roywiggins wrote: post #28
hxksleo wrote: post #3

I'd be interested in whether proofs like these will be formalized in proof assistants that can be checked with computer code, so that it removes doubt of error. It's something in math I'd like to see become more prevalent.

The problem is, once you have a proof that everyone agrees is correct, what's the incentive to painstakingly translate it into something a computer also agrees is correct? Yes, you might turn up some "bugs" in the proof, but proof bugs can almost always be ironed out. It's a very rare proof that is accepted and then falls apart later. If proofs were as "buggy" as computer programs- falling apart all the time- then th…

I agree that it's rare that a proof is accepted and falls apart later, but it does happen occasionally.

Somewhat famously, Voevodsky turned his attention to mathematical foundations, including proof assistants, at least in part because he was spooked that a part in one of his big papers was later shown to be incorrect. (Interestingly, someone much less known pointed this out in a preprint but it was, from my memory, largely ignored for some time -- who's going to believe a nobody versus a Fields Medalist?) There's a talk that Voevodsky gives at (I think) IAS, where he mentions this.

---

Edit: okay, here are the slides: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio...

The whole talk is interesting, but slides 8-13 talk about the topic at hand. In particular:

> This story got me scared. Starting from 1993 multiple groups of mathematicians studied the “Cohomological Theory” paper at seminars and used it in their work and none of them noticed the mistake.

> And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.

...

> It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.

Post reply on HN