Earlier quoted context omitted.
Is it possible to even check such a proof programmatically? Do we have that kind of technology? Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?
There is a language called lean which is popular among mathematicians. Here is an article: https://www.quantamagazine.org/building-the-mathematical-lib... A more recent article as well: https://www.quantamagazine.org/lean-computer-program-confirm...
New math book rescues landmark topology proof
91–100 of 171 posts
Re: New math book rescues landmark topology proof
#92Earlier quoted context omitted.
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 co…
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. This is a single Turing machine which does not need external modification. Internally, it works by having an inner Turing machine that it modifies. But Z itself doesn't change.
Then you can define M = "if Z(M): loop", call Z(M), and get your contradiction back.
If no, then you've built a more-powerful-than-a-Turing-machine machine of some sort.
Re: New math book rescues landmark topology proof
#93Earlier 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 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
#94Earlier 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…
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 roadblock when Russell proposed a paradox: does the set of all sets that do not contain themselves contain itself? The solution to this, as found in modern set theory, is to very carefully construct sets in such a way that no set can contain itself in the first place, and so the very question isn't expressible in the logic of modern set theory.
The underlying point of both Gödel and Turing is, as you say, constructing a similar statement akin to "this statement is false." But more specifically, what they actually did was to show that, once you meet some relatively low barriers, it is impossible to make a system that omits that construct. In effect, what is done is to encode (respectively) proofs and programs into integers, and then using this encoding, shows that you can always create a self-reference that blows up. Yes, if you change the encoding, it requires a potentially different number to create the self-reference, but the point is that so long as there is a bijection to the natural numbers, then the problematic self-reference must exist.
And, as you may be able to reflect upon, everything we as humans can write or speak can be reduced to a finite-length string of a finite-symbol alphabet, so everything we create must be bijectable with the natural numbers if infinite.
Re: New math book rescues landmark topology proof
#95Earlier 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…
> Would the proof completely fall apart if the algorithm could update itself to handle the new information? The only thing stopping it is that in the formulation of the problem, the algorithm is assumed to not be able to change with new information (ie it's not an "online" algorithm). Simple put the halting problem means that you cannot make a program (a static piece of code) that can determine in a finite amount of…
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?
I realized it may not be entirely possible to build an actual machine which hosts endlessly growing code. There are probably laws of physics which put some type of limit on how big things we build can get.
Re: New math book rescues landmark topology proof
#96Earlier 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...
Re: New math book rescues landmark topology proof
#97Earlier quoted context omitted.
> Would the proof completely fall apart if the algorithm could update itself to handle the new information? The only thing stopping it is that in the formulation of the problem, the algorithm is assumed to not be able to change with new information (ie it's not an "online" algorithm). Simple put the halting problem means that you cannot make a program (a static piece of code) that can determine in a finite amount of…
> The halting problem means that you cannot make a program (a static piece of code) that can determine in a finite amount of time if another program halts operating on some input. 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? I realized it may not be ent…
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).
> I realized it may not be entirely possible to build an actual machine which hosts endlessly growing code. There are probably laws of physics which put some type of limit on how big things we build can get.
So long as you have enough memory, even an Intel 8086 would be able to compute arbitrarily large programs. It could just emulate a universal Turing machine.
Re: New math book rescues landmark topology proof
#98I 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…
Re: New math book rescues landmark topology proof
#99Earlier 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…
"There is no proof for the statement with Godel-number g".
What I'm struggling with is trying to understand if self-reference can be formally represented by some symbol. Can it?
Godel's proof seems to rely on a trick that allows a formal system to talk about itself but is that possible? There would need to be a symbol for that and thus a symbol that refers to itself?
A picture of a pipe is not a pipe. Similarly a representation of a proof is not a proof, is it?. Not saying I believe I'm right and Godel wrong, but it just feel strange to me that a formal system could ever "prove" anything about itself.
What does it mean that something is "true"? That it can be proven?
Re: New math book rescues landmark topology proof
#100I do find it amazing that mathematicians seem to have almost infinite time to work on problems, and so much freedom to choose what they're working on. How great that a big group of people can collectively decide to spend years creating a book like this.