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

121–130 of 171 posts

Re: New math book rescues landmark topology proof

#121

Post by srcreigh »

jcranmer wrote: post #94
srcreigh wrote: post #76

Earlier quoted context omitted.

I suspect someone could write a book (or an HN comment at least) about the popular confusion about Godel's 1st incompleteness theorem. :-) In fact we (my brother and I) agreed that it bears a striking resemblance to Turing's halting problem: They both seem to show what computers or math can't do, but in fact both theorems only reveal limitations of certain models of computers and/or math. We both have undergrad degre…

Gödel's Incompleteness Theorem and the undecidability of the halting problem can in fact be proved using each other, so there is good reason to think that there is a deeper connection. What you suggest isn't actually possible, and to explain why, it's worth stepping back a little bit. Originally, there was a program to formalize mathematics that came to be known as naïve set theory. This theory ran into a major roadb…

I am honoured to have nerd-sniped you, jcranmer. I won't respond at length as I have in some of the child threads here.

As far as I can tell in my other expositions, apparently I object to the very fact that mathematicians like to fix things and make inferences about them! I think some things, such as computation, humans, animals, etc, should be allowed to be sensitive to time and prior inputs.. and the very act of fixing now and inferencing later seems to infringe upon that right. That may be the lowest barrier of all of mathematics!

Cheers my friend, thank you for engaging.

Re: New math book rescues landmark topology proof

#122

Post by fogof »

mindcrime wrote: post #62
leephillips wrote: post #2

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.

I wonder how many other results in maths require an entire book length treatment (or multiple book length treatments)? The one that jumps out to my mind is Gödel's Incompleteness Theorem(s)[1]. I know there are at least a couple of complete books dealing exclusively with this result. [1]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

"Incompleteness ex Machina" by Sebastian Oberhoff, is a nice paper-length exposition https://arxiv.org/abs/1909.04569.

Re: New math book rescues landmark topology proof

#123

Post by srcreigh »

srcreigh wrote: post #101
geofft wrote: post #92

Earlier quoted context omitted.

How do you generate the sequence H_0, H_1, ...? Specifically, is there a Turing machine G that can generate H_0, H_1, ..., onwards, perhaps taking in some input along the way? If so, then you can construct a self-contained Turing machine Z that takes a machine M as input, which works as follows: it calls G to generate H_0, runs H_0 for a bit on M, then calls G to generate H_1, runs H_1 for a bit on M, and so forth. T…

Thanks so much! This is fun. I think, with your explanation, there's still a big handicap for the halting machine code. To illustrate.. If I were to say to you: Is the correct answer yes or no, considering that later I will reverse my answer, and enforcing that you can't later change your answer? It's like, okay, of course, with that model, you can never win. I don't think it reveals any limitation of your understand…

I mixed up some things here... If you have G(G,M) which at each point gives you [0|1]:G', it's interesting to think of what happens if you define M = "if G(G,M)[0]: print G' = G(G,M)[1] then loop"... does G'(G',M) always produce a contradiction?

Re: New math book rescues landmark topology proof

#124

Post by 3PS »

jacobolus wrote: post #33
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.

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.

It's not out of the question for research-level math to be formalized in proof assistants. Most notably, a landmark paper by Peter Scholze (a Fields medalist) was, at his request, formalized in Lean. Or at least, the important part was formalized in about 6 months. See [1] for the post where Scholze asks for help in formalizing the proof and explains why he thinks it's important - in this case it was a very gnarly proof of a theorem that could hopefully be used as a black box by other mathematicians. See [2] for Scholze's thoughts after the project succeeded, 6 months later.

[1] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...

[2] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

Re: New math book rescues landmark topology proof

#125

Post by philipswood »

hermitdev wrote: post #117
leephillips wrote: post #2

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.

I hope they have a quality editor. Would hate to have a situation where they made a mistake on page 5, rendering the subsequent 495 pages worthless gibberish without a correction. (I know there's a bit from a TV show or movie like this, but I can't recall where. Maybe Good Will Hunting?) On a serious note, I'm wondering how approachable this book is to non-mathematicians. I mean, I've had more formal math education t…

Was the movie you remember maybe "Proof"?

https://en.m.wikipedia.org/wiki/Proof_(2005_film)

PS: it had a mathematician with a band that did an imaginary number in it.

Re: New math book rescues landmark topology proof

#127

Post by fogof »

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.

As someone whose research currently consists of proving things in proof checkers, I can confirm they are more complicated than LaTeX.

At one point, I had to prove n / 15 + n / 4 + (2 * n / 3 + 1) floor or that quotient). Automatic tactics that simplify things for you help some, but it still ends up being a good 8 lines of code for such a trivial statement. When things like this can be handled fully automatically, then it will be ready for mainstream use.

It is fun to fight the proof checker though! :)

Re: New math book rescues landmark topology proof

#128

Post by throwaway81523 »

civilized wrote: post #115
throwaway81523 wrote: post #111

I had not realized the 4-dimensional case was so hard that the much more famous 3-dimensional case was "another" contender for the hardest. I had thought it was sort of like the 4 color map theorem on stereoids, where first it was proved in 5+ dimensions (Smale, 1961), then 4 dimensions (Freedman, 1982), and finally 3 (Perelman, 2006), getting harder and harder at each step.

And the proofs of this one fact are all completely different depending on the dimension. I wonder if there are any prospects of a unified proof for all dimensions.

Smale's proof for d>=5 was unified. The d=4 and d=3 cases were special and those are special dimensions for a lot of reasons. "Low-dimensional topology", i.e. d=3 or d=4, is a big subject in its own right, because of those issues. At least for now, the prospect of unifying them with higher dimensions is somewhat remote. Basically in higher dimensions, there is more space to maneuver and things don't get in each other's way as much, so many proofs become easier. As well, many things are true in high dimensions and false in low dimensions, in which case unification is obviously impossible.. See also "curse of dimensionality" about why things are different for high dimensions.

Re: New math book rescues landmark topology proof

#129

Post by unanswered »

srcreigh wrote: post #119
thethirdone wrote: post #97

Earlier quoted context omitted.

> Interesting. My first thought was, couldn't we just create programs that are designed to keep growing? Isn't that both completely possible and more powerful than the model of computing where programs are static? What does it mean to "create programs that are designed to keep growing"? If they keep going by executing a finite program (if modified by a non-static program, what created that program?) on their code and…

> What does it mean to "create programs that are designed to keep growing"? If they keep going by executing a finite program (if modified by a non-static program, what created that program?) on their code and resuming, that would not be more powerful (Turing machines can do that). To me, your question is like asking this: Do all the programs that we humans ask computers to compute come from a finite program? Is life…

Your "growing program" can (presumably, since we don't have a formal definition) be interpreted by a finite program; i.e. which can treat unlimited memory as instructions to execute. This means, in a very strict and formal sense, that it is not a more powerful model of computing. Therefore it is subject to the halting problem.

But even if it were a more powerful model, it would still be subject to an analogous halting problem. This is well-trodden ground. It is a misunderstanding to believe that the halting problem is fundamentally tied to the exact power or nature of Turing Machines.

Re: New math book rescues landmark topology proof

#130

Post by qweqwweqwe-90i »

lou1306 wrote: post #72
mindcrime wrote: post #62

Earlier quoted context omitted.

I wonder how many other results in maths require an entire book length treatment (or multiple book length treatments)? The one that jumps out to my mind is Gödel's Incompleteness Theorem(s)[1]. I know there are at least a couple of complete books dealing exclusively with this result. [1]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

Godel's theorem is actually not that complex. Sure, you may think of "Godel, Escher, Bach", but that book is stuffed with sooo much material that is only tangentially related to the theorem. Of course the consequences of that theorem are legion, and they do warrant many books worth of discussion. But the proof itself can fit in a long-ish blog post, I think. Fermat's last theorem, on the other hand...

If you could prove the ABC conjecture then Fermat's last theorem becomes much less than a page of proof :)
Post reply on HN