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

81–90 of 171 posts

Re: New math book rescues landmark topology proof

#81

Post by lostmsu »

adgjlsfhk1 wrote: post #68
lostmsu wrote: post #41

Earlier quoted context omitted.

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

The problem is that the way people write proofs, you don't go axiom by axiom. You might evaluate an integral in one step, or make an argument that some sequence is obviously asymptotically less than a function. Pretty much every step in a human proof requires a computer proof generation step to verify.

There might be a chicken and an egg problem. If knowledge of theoretical mathematics would be designed like a framework with good documentation what you mention would be solved by simply referring to the corresponding part of the framework.

But to get that more people would need to be involved into transcribing proofs into formal language. Ideally, everyone. This is a higher standard, and somebody needs to ask for it.

Re: New math book rescues landmark topology proof

#82

Post by EamonnMR »

srcreigh wrote: post #76
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_...

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…

I like to think of the halting problem as similar to the inability to predict the future. In order to predict the future you'd need a model of the whole universe, including the model. Once you think of it like that you realize that you can't beat halting in the classical universe.

Re: New math book rescues landmark topology proof

#83

Post by lostmsu »

andyjohnson0 wrote: post #57
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.

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

Thanks for this remark.

It is amusing to see this behavior, considering the comment is a question, to which responses seem to favor answer "no".

The only part of the comment, that is actually a statement about peer review in mathematics being as bad or even worse in terms of assessing correctness, than reviewing large code changes. And nobody argues against that.

Re: New math book rescues landmark topology proof

#84

Post by geofft »

srcreigh wrote: post #76
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_...

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…

Suppose the algorithm could update itself with new information. Then you can formulate it in one of two ways:

1. The process of updating the algorithm can, itself, be described by a Turing machine. Think of it like an emulator / debugger (since a universal Turing machine exists, i.e., you can write an evaluator for a Turing machine as a Turing machine). The outer Turing machine can run the inner one partially, realize it needs changes, update it, and then continue running it and return its output.

But then the outer Turing machine, which is self-contained, is itself subject to the halting problem, and you can construct the counterexample based on it. You've just made the machine bigger.

2. The process of updating the algorithm cannot be described by a Turing machine. Perhaps it involves some sort of higher form of intelligence which itself cannot be represented as a Turing machine (so, if you want to say "a human updates it," you're working on the assumption that the human brain cannot be implemented/emulated - however slowly - on a Turing machine, and the decisions of how to update the algorithm require this supra-Turing computational power).

But then, as before, the actual machine is this combination of the extra intelligence and the Turing machine. You've made some stronger non-Turing machine to solve the problem, and the statement "No Turing machine can determine whether any arbitrary Turing machine halts" still holds true. You've introduced a new class of machines with additional power over Turing machines. And the halting problem now applies to these machines when evaluating whether a machine of their own class halts, even though they can determine whether simpler machines halt. Your human-Turing mechas can solve the halting problem for Turing machines, but they cannot solve it for other human-Turing mechas. See https://en.wikipedia.org/wiki/Turing_jump

In fact, this model, applied to Gödel's theorem, was explored in Turing's own Ph.D. thesis: https://en.wikipedia.org/wiki/Systems_of_Logic_Based_on_Ordi...

Re: New math book rescues landmark topology proof

#85

Post by iainmerrick »

CamperBob2 wrote: post #79
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_...

The most recent case similar to this one is Mochizuki's work on the ABC conjecture, which has still not reached the point where it's accepted by the majority of the community due to its complexity. There are lots of parallels between Mochizuki and Freedman. They both had to break a lot of new ground, and they both had trouble communicating their results to enough people to become part of the official canon of mathema…

I believe the latest news on Mochizuki’s work is that Peter Scholze and Jakob Stix identified a fatal flaw, and Mochizuki has not convincingly rebutted it. See e.g. the first item here: https://www.math.columbia.edu/~woit/wordpress/?p=12429

Both the claimed proof and the disproof have now been published in journals, and neither has been retracted! That’s a rather unusual situation to say the least. But I think people in the field generally agree that the proof is flawed and unfixable.

Re: New math book rescues landmark topology proof

#86

Post by jcranmer »

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

The classification of finite simple groups [1] is apparently ~11-12 books long (when it's finished). Yes, several books for a single theorem.

[1] https://en.wikipedia.org/wiki/Classification_of_finite_simpl...

Re: New math book rescues landmark topology proof

#87

Post by [deleted] »

iainmerrick wrote: post #85
CamperBob2 wrote: post #79

Earlier quoted context omitted.

The most recent case similar to this one is Mochizuki's work on the ABC conjecture, which has still not reached the point where it's accepted by the majority of the community due to its complexity. There are lots of parallels between Mochizuki and Freedman. They both had to break a lot of new ground, and they both had trouble communicating their results to enough people to become part of the official canon of mathema…

I believe the latest news on Mochizuki’s work is that Peter Scholze and Jakob Stix identified a fatal flaw, and Mochizuki has not convincingly rebutted it. See e.g. the first item here: https://www.math.columbia.edu/~woit/wordpress/?p=12429 Both the claimed proof and the disproof have now been published in journals, and neither has been retracted! That’s a rather unusual situation to say the least. But I think people…

[deleted]

Re: New math book rescues landmark topology proof

#88

Post by CamperBob2 »

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.

The slides that mahogany linked to [1] may give you some insight into this question. They're pretty interesting.

[1] https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio...

Re: New math book rescues landmark topology proof

#89

Post by srcreigh »

geofft wrote: post #84
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…

Suppose the algorithm could update itself with new information. Then you can formulate it in one of two ways: 1. The process of updating the algorithm can, itself, be described by a Turing machine. Think of it like an emulator / debugger (since a universal Turing machine exists, i.e., you can write an evaluator for a Turing machine as a Turing machine). The outer Turing machine can run the inner one partially, realiz…

Thanks for response! I will definitely read about Turing jumps :)

I'm not sure I understand your 1. Reading the Halting problem undecidability proof, it goes like this:

Suppose machine H can solve the halting problem. We construct special machine M which calls H(M), and negates the output. Then when we run H(M), it halts if M doesn't halt, and doesn't halt if M halts, hence M doesn't exist.

On the other hand, if H could self-modify, we would have a sequence H_0,H_1,... of machines based on its modifications. Ie, M is written with H_i, but later we're calling H_j(M). No guarantee that our negation still works.

Re: New math book rescues landmark topology proof

#90

Post by ntlang »

iainmerrick wrote: post #85
CamperBob2 wrote: post #79

Earlier quoted context omitted.

The most recent case similar to this one is Mochizuki's work on the ABC conjecture, which has still not reached the point where it's accepted by the majority of the community due to its complexity. There are lots of parallels between Mochizuki and Freedman. They both had to break a lot of new ground, and they both had trouble communicating their results to enough people to become part of the official canon of mathema…

I believe the latest news on Mochizuki’s work is that Peter Scholze and Jakob Stix identified a fatal flaw, and Mochizuki has not convincingly rebutted it. See e.g. the first item here: https://www.math.columbia.edu/~woit/wordpress/?p=12429 Both the claimed proof and the disproof have now been published in journals, and neither has been retracted! That’s a rather unusual situation to say the least. But I think people…

Experts have been skeptical for quite some time. You can see discussion on the exact point Scholze (PS) brings up in the following blog post (the post and many comments are by prominent number theorists)

https://www.galoisrepresentations.com/2017/12/17/the-abc-con...

One quote from the post I find worth repeating:

> This post is not about making epistemological claims about the truth or otherwise of Mochizuki’s arguments. To take an extreme example, if Mochizuki had carved his argument on slate in Linear A and then dropped it into the Mariana Trench, then there would be little doubt that asking about the veracity of the argument would be beside the point. The reality, however, is that this description is not so far from the truth.

Post reply on HN