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

151–160 of 171 posts

Re: New math book rescues landmark topology proof

#151

Post by conistonwater »

est31 wrote: post #132
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…

This is more due to the inability of promotion committees to capture the usefulness of scientific work than due to the uselessness of this for science. Sure, if you have nothing else to show for yourself, it might be bad for your career. But I feel like people who work in academia already forego many career opportunities. That being said, you still need to put food onto the table. But posterity will remember you. Tod…

It's worth noting that the consensus in the MathOverflow thread seems to have been that it was a complete waste of time to spend any further time on that paper and the proof. That's the opinion that they reached based on the general issues with the proof itself, and not any promotion committee decisions: specifically the fact that multiple mathematicians tried to read the paper in detail, in seminars, to understand it, and reported that they failed. That would certainly do it!

I don't have an opinion myself on whether it was a mistake to spend more time on it, but you can clearly see professional mathematicians deciding not to work on something "important" for the legitimate reason that they thought it was unsalvageable. If that's correct, then a promotion committee should penalize people for doing it anyway.

Re: New math book rescues landmark topology proof

#152

Post by kevinventullo »

PartiallyTyped wrote: post #148
kevinventullo wrote: post #67

Earlier quoted context omitted.

As a former mathematician, I would say the stacked layers get a lot messier closer to the cutting edge.

May I ask why former? Defining better abstractions is part of the process that got us so far. Even in ML, we are starting to define some very good abstractions for Neural Networks through the perspective of symmetries and geometry.

The academic job market is brutal compared to tech, especially the “two-body problem”: https://slate.com/human-interest/2013/10/academia-s-confound...

I completely agree we should be defining better abstractions! I more meant it gets a lot harder to do so near the cutting edge.

Re: New math book rescues landmark topology proof

#153

Post by mindcrime »

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

It's a bit late to add this, but I realize that I wasn't entirely clear above. When I say "results in maths (that) require an entire book length treatment" I don't mean a proof that is inherently book length. I mean, a proof that justifies (one or more) book length "downstream" treatments that explain, clarify, expand, etc., the base proof.

Going back to Gödel's Incompleteness Theorem(s) for example... yes, the original proof is not that long, but for whatever reason, people have felt compelled to write entire books on the topic, after Gödel, to say more about the proofs. That kind of thing is more what I was thinking of, FWIW.

Re: New math book rescues landmark topology proof

#154

Post by gjm11 »

leephillips wrote: post #77
gjm11 wrote: post #73

Earlier quoted context omitted.

Just for fun, an example of an application of partial fraction decomposition that doesn't involve taking integrals. Consider the Fibonacci numbers 0, 1, 1, 2, 3, 5, 8, ... (with the convention that 0 and 1 are the 0th and 1st). Here's one way to get an explicit formula for them. First, we package them up into what's called a "generating function": 0 x^0 + 1 x^1 + 1 x^2 + 2 x^3 + 3 x^4 + 5 x^5 + ... or, more concisely…

Very nice. This is similar to Donald Knuth’s treatment in §1.2.8 of v.I of The Art of Computer Programming (Fundamental Algorithms).

Yup. I don't think the similarity is because I'm copying Knuth (I certainly wasn't deliberately doing so); this is a very well known argument and there isn't all that much scope for presenting it very differently.

(Oddly, I think the presentation in the later Concrete Mathematics is worse than in TAOCP; they're trying to make it more approachable but I think just make it a bit more roundabout.)

Re: New math book rescues landmark topology proof

#155

Post by leephillips »

gjm11 wrote: post #154
leephillips wrote: post #77

Earlier quoted context omitted.

Very nice. This is similar to Donald Knuth’s treatment in §1.2.8 of v.I of The Art of Computer Programming (Fundamental Algorithms).

Yup. I don't think the similarity is because I'm copying Knuth (I certainly wasn't deliberately doing so); this is a very well known argument and there isn't all that much scope for presenting it very differently. (Oddly, I think the presentation in the later Concrete Mathematics is worse than in TAOCP; they're trying to make it more approachable but I think just make it a bit more roundabout.)

Oh, absolutely, I realize that. It’s just that I learned this from Knuth so I recognized the derivation, and I thought you’d like to see it, but I see you already know about it.

Re: New math book rescues landmark topology proof

#156

Post by srcreigh »

unanswered wrote: post #129
srcreigh wrote: post #119

Earlier quoted context omitted.

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

Thanks, I read the proof [1] again a lot more carefully last night, and really failed to formalize my point.

I tried to reason about it in different ways. Such as, for case 1, considering Z(Z) halts. I don't think it's unreasonable to say that H(Z,Z) could in fact return true. It could read the code for Z, determine that Z(Z) will loop since H(Z,Z) would return false, return true, and then Z(Z) would halt since H(Z,Z) returned true. No immediate contradiction.

Problem is that doesn't completely eliminate the contradiction, it just introduces another one. Even if Z(Z) halts and H(Z,Z) returns false, you could argue backwards and say that the only way for Z(Z) to halt is if H(Z,Z) returns true, but H(Z,Z) can't return two different results.

Part of me still doesn't like the negator program. Too many contradictions. Apparently there are constructive proofs for the halting problem too, which I don't understand yet, so the rabbit hole continues.

Thanks again for engaging.

[1]: https://www.comp.nus.edu.sg/~cs5234/FAQ/halt.html

Re: New math book rescues landmark topology proof

#157

Post by PartiallyTyped »

kevinventullo wrote: post #152
PartiallyTyped wrote: post #148

Earlier quoted context omitted.

May I ask why former? Defining better abstractions is part of the process that got us so far. Even in ML, we are starting to define some very good abstractions for Neural Networks through the perspective of symmetries and geometry.

The academic job market is brutal compared to tech, especially the “two-body problem”: https://slate.com/human-interest/2013/10/academia-s-confound... I completely agree we should be defining better abstractions! I more meant it gets a lot harder to do so near the cutting edge.

I meant that it takes time to figure out the correct ones, modern algebra is the outcome of nearly 300 years of 'modern' mathematics!

It's unfortunate that such issues exist! But considering the issues within academia, you are most likely in a better situation now that otherwise with respect to free time and salary.

Re: New math book rescues landmark topology proof

#158

Post by rossjudson »

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.

Hurray for obsession, because without it humanity would be forever skirting around the dark corners of our understanding.

Re: New math book rescues landmark topology proof

#159

Post by lostmsu »

deadbeef57 wrote: post #150
lostmsu wrote: post #32

Earlier quoted context omitted.

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.

You still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.

Thanks for pointing that out. This is still magnitudes less things to manually check for correctness than an entire proof.

Re: New math book rescues landmark topology proof

#160

Post by jacobolus »

3PS wrote: post #124
jacobolus wrote: post #33

Earlier quoted context omitted.

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

This is great work.

But to be clear: a community effort by 20+ people, after 6 months of work, managed to make progress toward proving a theorem, including proving some of the trickiest technical parts. As I said before, this is like 2 orders of magnitude more effort than the original plain-language (slightly sloppy/underspecified) proof.

Scholze:

> I cannot read the proofs at all — they are analogous to referring to theorems only via their LaTeX labels, together with a specification of the variables to which it gets applied; plus the names of some random proof finding routines.

Post reply on HN