Live data from Hacker News

New math book rescues landmark topology proof

quantamagazine.org

141–150 of 171 posts

Re: New math book rescues landmark topology proof

#141
post #139
post #72

Earlier quoted context omitted.

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

For those interested: Assume a formal language that can model the natural numbers. Consider the set of all provable statements. This is countable because it’s a subset of the list of strings of a finite number of characters, which is countable. Consider the statement “Statement N is false”. This is both a valid statement and cannot appear in the list. Godel proved significantly more than that, but that’s the basic re…

Since these 3 results are so similar are they a subset of a more general concept?

Re: New math book rescues landmark topology proof

#142

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…

Your comment made me break down and finally make an HN account. I think I may have the perfect answer for you. Your comments remind me so much of myself, when I was in 7th grade and we just learned that 0.999... would exactly equal 1. Not almost, but exactly. I know that I asked my math teacher tricky questions, and left really unsatisfied, because "obviously it's not true", probably my teacher does not understand infinity. I kind of forgot about it, and it only really clicked a couple years later once I learned about series and limits, because I finally gained an intuition for working with infinity.

A very important notion about infinity that the terms "For any arbitrary large N" and "For Infinity" are not the same thing.

I actually think that the cause of the confusion is similar. Maybe your mental model of computation includes an "arbitrarily large N" where you actually need an "infinitely large N".

Note that the halting problem (and a whole bunch of other interesting undecidable problems) is actually "semi-decidable". This means we are guaranteed to get an answer to the question, but only if the answer is actually "yes". (Before you ask: Taking the inverse of a problem does not preserve semi-decidability, so no trickiness here.)

We need some intermediate results here. I am not going to prove them for brevity (and because I will probably be unable to produce them right now), so you'll have to trust me for them. Sorry!

A Turing machine P which gets input i produces output P(i). We can construct a machine P_i which ignores its input, but instead always produces P(i) for any i. We can also construct for any P an encoding Enc(P) (the "source code" so to say, actually a Gödel numbering) which encodes the turing machine. We can also show that there is a universal turing machine U which for any Enc(P) will produce the same outputs as P for all possible inputs i. We can also construct a special limited universal turing machine U_j which halts after at most j steps.

So how does semi-decidability work in practice: Let us simulate a turing machine P on U_1. If it halts, we return 1, if it does not halt after 1 step, we return 0. This turing machine will solve the halting problem for all turing machines that halt after 1 step. We can then look at U_2, U_3 and so on, and those machines will always solve the halting problem for a strict superset of the others. So we know that the number of turing machines which do not have a solution by our ever increasing set of halting problem deciders will get smaller and smaller.

The halting problem now says: Even if all machines of {U_j : j is natural number} run in parallel, we will always have Turing machines P for which we will not get an answer. The halting problem also tells us that there will never be a U_infinity, which would then give us the answer.

If you don't like the self-referential proof, you can check out the diagonalization proof, which is more rigorous.

Now you have given examples of for example humans adapting to additional input. We know for a fact that humans in their lifetime can only perform a finite number of computational operations, and parse a finite number of input arguments. If I was a physicist I could probably cite some theorem of thermodynamics to give you an upper bound on that number, which is probably astronomically huge but finite. The same applies for the computing power of the universe. Huge, but finite.

This is all the halting problem says: We can solve a lot of problems by brute force, but never all of them. We can also solve all problems approximately by just giving an arbitrary (but fixed) answer after we get bored with our long-running turing machine.

The halting problem is important because for all we know and care, and infinite computer cannot physically exist, as the universe itself is finite. For example, the halting problem can be solved by a theoretical computer which speeds up by factor 2 on every step. And probably also something like a machine which has an exact encoding for every real number, which cannot exist in the universe as we currently understand it, for similar reasons. https://en.wikipedia.org/wiki/Hypercomputation

It's not that we cannot think of those models, it is just that they are completely useless and uninteresting as they get too powerful, but also impossible to build. You could approximate them, but the approximation is useless, as the approximation will again be a convoluted turing machine.

Re: New math book rescues landmark topology proof

#143

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 is pretty common for some pure mathematics papers to be pretty much book length anyway these days, say 80 pages or more.

Re: New math book rescues landmark topology proof

#144
post #133

Earlier quoted context omitted.

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…

It's peppa pig episode where mommy pig writes a book and george overflows the buffer of her computer by scoring very high in the chicken game

It gets better:

it is used in at least one but do I think two or possibly more later episodes.

The one that pops into my mind is the one where the kids dress up as something from their favourite book and the Elephant kid dresses up as the very long number from Mummy Pigs book.

For some reason even while I'd much prefer silence, Peppa Pig doesn't annoy me as much as certain other kids tv shows. Maybe it is the lack of lessons to learn, that everyone messes upnor something like that?

Re: New math book rescues landmark topology proof

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

There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised into the system so that a theorem can even be stated, let alone its proof checked. Coming up with useful (and correct) formalisms of these objects, objects that mathematicians use constantly every day, are entire research projects of their own.

There are some excellent talks by Kevin Buzzard about this, and where he sees it going in the future from a mathematician’s perspective. We’re getting there but progress is slow, and a large part of why it’s slow is that modern mathematics is fantastically complicated.

Re: New math book rescues landmark topology proof

#146
post #72

Earlier quoted context omitted.

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 :)

Speaking of ABC, some years ago HN was all abuzz with inter-universal Teichmuller theory, did that fizzle out or what?

Re: New math book rescues landmark topology proof

#147
post #139

Earlier quoted context omitted.

For those interested: Assume a formal language that can model the natural numbers. Consider the set of all provable statements. This is countable because it’s a subset of the list of strings of a finite number of characters, which is countable. Consider the statement “Statement N is false”. This is both a valid statement and cannot appear in the list. Godel proved significantly more than that, but that’s the basic re…

Since these 3 results are so similar are they a subset of a more general concept?

[deleted]

Re: New math book rescues landmark topology proof

#148

Earlier quoted context omitted.

I am not a mathematician, though I do very applied math (ML), I took a course this semester that is intended for Pure Math MSc, called Advanced Vector spaces, having only done some linear algebra and calculus at the undergraduate level, some abstract algebra and some geometric algebra. I am consistently in awe of how well mathematicians have stacked layers of abstraction one on top of the other, and how many differen…

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.

Re: New math book rescues landmark topology proof

#149

Earlier quoted context omitted.

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

"apparently I object to the very fact that mathematicians like to fix things and make inferences about them": that's not really what's going on: time can be present in mathematics (e.g. defining a sequence iteratively) and the like.

What you do have to fix is the definition of things: your reasoning is very shaky, and once you would start formalizing things you will find you cannot "defeat" the Halting problem or incompleteness theorem.

Re: New math book rescues landmark topology proof

#150
post #32

Earlier quoted context omitted.

Because programmatically checked proofs don't work the way you think they do. And even programatically checked proofs are still programs. And programs still need code review.

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.
Post reply on HN