Live data from Hacker News

New math book rescues landmark topology proof

quantamagazine.org

51–60 of 171 posts

Re: New math book rescues landmark topology proof

#51

So who gets credit for proving it? Freedman, the original author from 1981; or the authors of this book? If Freedman's proof has so many gaps, should it be considered more of a proof outline, or a motivation for believing a conjecture, and the current book be considered the actual proof? Or does Freedman get the glory? In that case, there's not much incentive for people to do what these book authors did. Which I supp…

According to a sister comment, the paper contains a meta-proof that shows that many of the gaps do not matter in showing the equivalence.[0] I don't know if this is true or not, I'm just connecting the discussions.

[0] https://news.ycombinator.com/item?id=28473319

Re: New math book rescues landmark topology proof

#52

Earlier quoted context omitted.

> Math is the most formal science there is. Can you prove that?

Formality is technically the degree of mathiness applied to a domain, since formal logic and any other framework of formalization decomposes to mathematics. So... it's a tautology. Math is the most mathy math. Biology or psychology are less mathy maths. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Having provablility holes in the formal system doesn't imply the existence of other systems that could…

But if you only have maps and no territory, can you still be said to be doing cartography? :)

Re: New math book rescues landmark topology proof

#53
post #41
post #38

Earlier quoted context omitted.

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

Fair point. I'm coming from the perspective that mathematicians don't like to fill in pesky details that experts in their respective fields can figure out in an hour or ten.

Re: New math book rescues landmark topology proof

#54
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…

There's plenty of incentive to do that actually, since a translation of a proof that had not been formalized before yields a much clearer proof than anything a human could write on her own. This is doubly true when some "bugs" are found and "ironed out" in the process - even seemingly trivial bugs can trip up the reader and obscure interesting sr structure. In fact, a truly novel formalization is pretty much publishable work in and of itself. The problem is not incentives; it's more of a lack of willingness to work in an area that's very fragmented still and makes it way too hard to reuse existing results.

Re: New math book rescues landmark topology proof

#55

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

High school math does not look much like research math.

High school math is highly concerned with teaching 'algorithms' that compute answers, like long multiplication, long division, the quadratic formula, completing the square, synetic division, u-sub integration, ...

Most mathematicians don't work with calculating things. Rather, they're more interested in _generally_ characterizing how objects behave (and _proving_ that that characterization is actually correct)

For example, the definition of "continuous" you learn in pre-calc is probably something like: if you compute a function's limit, you get the same thing as computing the function.

The topologist's definition is that the function's inverse map preserves openness.

These are basically unrecognizable as being the same thing, but in fact they are. And the second doesn't actually reference calculation or even anything identifiable as numbers!

I believe this is a significant cause of not understanding "why" despite understanding "how". As an example, I remember in pre-calculus we spent at least an entire unit on partial-fraction-decomposition. Partial fraction decomposition is a strange algebraic manipulation that is basically only important to integrating rational functions -- something you don't do until at least a year later, and which doing by hand is basically pointless because computers are better at it than humans.

They also require very different kinds of intuition. Building intuition is hard, but important for people studying math. Working through many different examples and problems and applications can help you build intuition.

But I don't really have any advice for how to make math stick better, but just want to share that the mathematics you learn in high school is not representative of the entire field.

If you ever want to get a taste of "higher math" without having lots of prereqs, point-set topology and group theory are two (very different!) fields that are also fairly accessible.

Re: New math book rescues landmark topology proof

#56

So who gets credit for proving it? Freedman, the original author from 1981; or the authors of this book? If Freedman's proof has so many gaps, should it be considered more of a proof outline, or a motivation for believing a conjecture, and the current book be considered the actual proof? Or does Freedman get the glory? In that case, there's not much incentive for people to do what these book authors did. Which I supp…

Well, thank God lots of scientists (mathematicians in this case) understand that transmission of knowledge is as important (or more so) as novelty. And that is their incentive.

This distinction has been called an "open exposition problem", versus an "open research problem".

Once Freedman's proof was accepted, it was no longer an open research problem; on the publication of this book, it will (hopefully) no longer be an open exposition problem.

The phrase was coined by Timothy Chow in his paper A Beginner's Guide To Forcing [0];

> "All mathematicians are familiar with the concept of an open research problem. I propose the less familiar concept of an open exposition problem. Solving an open exposition problem means explaining a mathematical subject in a way that renders it totally perspicuous. Every step should be motivated and clear; ideally, students should feel that they could have arrived at the results themselves."

[0] https://arxiv.org/abs/0712.1320

Re: New math book rescues landmark topology proof

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

(Meta but I don't think the parent comment deserved to be downvoted. Maybe it's arguably wrong but it prompted replies that increased my understanding of the practice of maths.)

Re: New math book rescues landmark topology proof

#58

If I understand this article, it’s about a 500-page book that is devoted to one proof of one theorem in topology. I find that amazing. And cheers to Quantum Magazine for regularly publishing popularizations of research mathematics. I know many, at times, take issue with their simplifications and framing, but they’re trying, where almost no one else with their reach covers these areas at all.

It's amazing how math can require so much work for what appears to be a single result, but I spend an entire semester proving a single mathematical theorem and to do that I had to work through an entire textbook, so I don't think it's that unusual.

Re: New math book rescues landmark topology proof

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

Getting a proof, even in one that is amenable to computer verification into a form where you can actually verify it is a monumental task, like it can easily take multiple experts multiple years. Adding to this problem the intersection of mathematicians who understand computer aided verification and who understand a particular piece of research mathematics is often empty, and even if there are a handful of people who…

> I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods.

Right, because that's not how it works. Errors aren't discovered after the proof has been translated into machine language because that is the only step of the verification. As soon as the code is written, the proof is verified. Necessarily, then, any error discovery has to happen before that.

Post reply on HN