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

41–50 of 171 posts

Re: New math book rescues landmark topology proof

#41

Post by lostmsu »

klyrs wrote: post #38
lostmsu wrote: post #29

Earlier quoted context omitted.

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.

> In terms of runtime, oh my god, get out of town.

I think you're mixing two different things here. Runtime is large for proof assistants, e.g. programs that can actually generate pieces of proof for you. Specifically the generation part. Verification of a complete proof were all the steps are provided like you would do in a paper should not, AFAIU, take a long time.

Re: New math book rescues landmark topology proof

#42

Post by spekcular »

auntienomen wrote: post #7
spekcular wrote: post #4

This has been a long time coming. There is an infamous MathOverflow thread about the proof (also linked in the article), with the following comment summarizing the state of affairs ~10 years ago: > There is no other evidence. In fact there is absolutely no evidence what so ever. I have never met a mathematician who could convince me that he or she understood Freedman`s proof. I attempted to read that monstrosity of a…

That comment on incentives is funny, but I'm not sure it captures the situation here: The mathematicians who wrote The Disc Embedding Theorem have been quite successful. All are on the tenure ladder (or tenured already) and publishing novel research in a field they revitalized. I can see how sinking time into this is risky, but that's generally true of choosing a field of research. I think the authors deserve credit…

I agree, actually. I think a book published by a major academic press is a plus for any tenure/promotion committee. Further, this is definitely not just "expository" work; as the article notes, they had a bunch of gaps/errors to fix. I expect the importance of those contributions would be reflected in strong recommendation letters for promotion.

Re: New math book rescues landmark topology proof

#43

Post by [deleted] »

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.

[deleted]

Re: New math book rescues landmark topology proof

#44

Post by lostmsu »

roywiggins wrote: post #36
lostmsu wrote: post #31

Earlier quoted context omitted.

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,…

> mathematics is not plagued with false "theorems."

But you don't know that.

There certainly were precedents: https://mathoverflow.net/questions/291158/proofs-shown-to-be...

Re: New math book rescues landmark topology proof

#45

Post by roywiggins »

webmaven wrote: post #30
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…

> A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe into a computer system. I guess the question is which of "convincing a human" or "convincing a computer" is considered…

Right, but the ordinary methods of doing mathematics seem to be so good that the vast effort required to encode proofs well enough for a computer to check vastly dwarfs the benefit, at least for now.

There's obviously been a lot of work done on proof assistants and maybe it will become easy and natural to formulate most proofs in a way a computer can check, but it's not anywhere close to that yet. The book explicating the proof discussed in the article is already 500 pages long, translating that into something a computer could check just isn't at all feasible yet.

Re: New math book rescues landmark topology proof

#46

Post by OGWhales »

spekcular wrote: post #4

This has been a long time coming. There is an infamous MathOverflow thread about the proof (also linked in the article), with the following comment summarizing the state of affairs ~10 years ago: > There is no other evidence. In fact there is absolutely no evidence what so ever. I have never met a mathematician who could convince me that he or she understood Freedman`s proof. I attempted to read that monstrosity of a…

> (also linked in the article)

Would never have seen that without your telling me. It was well hidden until you moused over it

Re: New math book rescues landmark topology proof

#47

Post by roywiggins »

lostmsu wrote: post #44
roywiggins wrote: post #36

Earlier quoted context omitted.

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,…

> mathematics is not plagued with false "theorems." But you don't know that. There certainly were precedents: https://mathoverflow.net/questions/291158/proofs-shown-to-be...

The answer given there by Manuel Eberl is more or less what I was trying to get at (and he is far more knowledgeable about it than I am). Lots of mathematicians find that the existing level of rigor in the field is enough.

Obviously the people who like proof assistants disagree, and they may be right. It could be that modern theorems are just too complicated to be adequately evaluated by unassisted humans. But mathematicians have been getting along just fine without them for a long time, so "why aren't we requiring computer-checked proofs of everything" has a very straightforward answer: mathematicians writ large aren't convinced of the benefit yet.

Re: New math book rescues landmark topology proof

#48

Post by doublerabbit »

I really wish I could get math to stick. I just finished my National 5 maths (rough equivalent of a US High School Diploma) night-class today and all I ever seem to understand is how, but not why. I'm the one asking "why is that that." And today was recapping on trinomial, simplifying fractions. Simple I expect to anyone with a mathematical mind, but to me, it's just an insane implosion which leaves me exhausted. I have notes, but even still.

What is the secret behind it? How do people get so good with Maths? Is it truly study,study & study? .. I hadn't even herd of the terminology of co-efficient until today. Let alone something like this.

Re: New math book rescues landmark topology proof

#50

Post by dodobirdlord »

phaedrus wrote: post #39

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 pl…

A common approach to proving a broad claim when there’s no straightforward proof is to figure out all of the entities that have the potential to produce a counterexample, break them up into a finite list of categories, and go through category by category proving, often with very different approaches depending on the category, that each category cannot contain a counterexample.

A major theorem proved in this style was the classification of finite simple groups. Not only was it done in this style, it frequently serves as a major component in other proofs of this style, since theorems about other kinds of groups can sometimes be re-expressed as claims about finite simple groups, and then checked category by category.

https://en.m.wikipedia.org/wiki/Classification_of_finite_sim...

EDIT: This is also part of why sometimes the first proof of a theorem will be very long, but someone will later use the insight of the first proof to produce a much shorter proof. The first proof will basically be a proof that the general claim breaks down into a (possibly very long) list of separately probable lemmas, followed by a proof of each of the lemmas. These may not overlap very much, leading to proofs that are very long and take a lot of background to understand. Once the result is known to be true, it may be worth the effort for the original author or someone else to refactor the “proved it can’t be disproved” proof into a much shorter direct proof.

Post reply on HN