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 paper a number of times by myself and quite a few times with a group of other mathematicians. We never were able to finish checking all of the details. Such seminars always ended before we could make it through even half of his paper. No other expositions on the subject seem to be any better. It is truely an odd state of affairs that after all of these years no one has managed to write a clear exposition of this so called proof, and that no one seems to question the claim that there ever was a proof. I remember thinking as a young mathematician either this "proof" is sheer nonsense or someone will eventually write out a clear and detailed explanation. As of April of 2011 I have understood that the so called proof is full of errors and they can not be fixed. I mentioned this to several mathematicians during the summer of 2011 and I believe these conversations are directly linked to the dialogue seen here on math overflow.
Also on that thread, Brendan Guilfoyle raised the issue of writing a complete book-length treatment of the proof. I found the following response an interesting commentary on incentives in academia.
> Promotion committee: "What have you done in the last 5 years?"
> B.G.: "I've been writing a book about a paper published in 1982."
> Promotion committee: "How is that groundbreaking overachieving hyped research?"
> B.G.: "It is not, but I am preserving the knowledge of the elders."
> Promotion committee: "Who told you that was a good idea?"
> B.G.: "A guy on the internet, and 24 people liked his suggestion."
> Promotion committee: "We will call you, don't call us. Good bye."
That comment on incentives is funny, but I'm not sure it captures the situation here: The mathematicians who wrote The Disc Embedding Theorem have been quite successful. All are on the tenure ladder (or tenured already) and publishing novel research in a field they revitalized.
I can see how sinking time into this is risky, but that's generally true of choosing a field of research. I think the authors deserve credit for doing it well. Likewise, Peter Teichner should get a little credit for helping to create the space for them to do so.
I agree, actually. I think a book published by a major academic press is a plus for any tenure/promotion committee. Further, this is definitely not just "expository" work; as the article notes, they had a bunch of gaps/errors to fix. I expect the importance of those contributions would be reflected in strong recommendation letters for promotion.
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. Today, Bach is considered one of the most prolific musical composers of history. But back when he lived, he didn't receive that much fame. In fact, after his death, people forgot about him. And Bach lived in a time before copyright. He used existing themes by other people and rearranged them for the instruments he used. Many of those folks might have been famous back then, but now many their names are only known to historians (exceptions exist, e.g. Vivaldi).
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.
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 than your average lay person, but I've also hardly used most of it since college. I'm curious if it'd be a worthwhile read or just something that'd end up sitting on my shelf, mostly unread...
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?
As a mathematician myself, I highly doubt it would be readable for non-mathematicians. Typically reading math books is work, even for mathematicians, and not so much something you do to relax in the evening.
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.
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.
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 result. It’s basically the same as the diagonal argument of real numbers being uncountable and it’s also basically the halting problem.
The crucial trick is that you can plug in an entry as data to another "program/theorem". This is extremely interesting, because there are limited logics and limited computation models where Godel and the Halting Problem do not apply.
GEB is a book about intelligence/consciousness. The incompleteness theorem is incidental — it’s only there to illustrate the notion of self-referentiality, and I’m not sure it does a particularly good job at it.
The incompleteness theorem can be proved in a few lines given the right definitions up front. It's basically the same as the undecidability of the halting problem, which has a proof that is written as a poem: https://introcs.cs.princeton.edu/java/54computability/haltin...
There is a wonderful book by Torkel Franzén about the incompleteness theorem that is 100+ pages, but it is not purely about the proof. It's a popularization that discusses bogus ways philosophers have interpreted the theorem, and stuff like that. It is called "Gödel's Theorem: An Incomplete Guide to its Use and Abuse".
And of course the proof of the classification of finite simple groups has afaik never been published all in one place, though there are some book-length expositions of it referring back to the original papers. It is a set of papers spanning around 20 years and adding up to around 10,000 pages. It is sometimes called "the enormous theorem": https://en.wikipedia.org/wiki/Enormous_theorem
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 mathematics that can actually be taught to others.
Freedman at least convinced a few key people, but AFAIK Mochizuki's work has never been understood by anyone not named Mochizuki. It may be complete BS, it may be earthshakingly brilliant, but either way it will evidently take someone's entire career to prove it.
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.
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)
> 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.
I would say that most hallmark results in theory-heavy mathematics (number theory, algebraic geometry, topology, …) could stretch to at least a book length treatment if you wanted a mostly self-contained proof.
It sounds like the main difference with this theorem is that the writeup of the original proof was so complicated, terse, and error-prone, that very few experts even understood it.
I don’t think the incompleteness theorems are nearly as wordy - this translation of Gödel’s original paper is under 40 pages after subtracting the introduction (not part of the original).
Not very much actually. Finite simple groups are kind of like prime numbers: any finite group can be broken down into simple subgroups similar to how any natural number can be broken down into a multiset of prime number factors.
That's why the classification of finite simple groups is so important, it's essentially a classification of all finite groups.
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 degrees in math fwiw.
Both theorems use a clever logical trick. For Godel's theorem, it is an encoding of "This sentence is false". For the halting problem proof, Turing first fixes the algorithm, asks the algorithm what its result will be, then switches the correct answer, forcing the algorithm to produce the incorrect answer.
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). Similarly, what if the model of math had mechanisms for recognizing paradoxes, or circular logical requirements, etc. I don't think either of those theorems would work anymore.
Anyway, I'm not saying the Halting problem would be easy to compute with the right model. If we had an efficient algorithm to solve the halting problem, we could solve tons of math problems easily. We could write some code to enumerate any countably infinite sequence, checking for the presence of some condition, and make inferences based on if it halts or not. For example, we could solve the Collatz conjecture by just writing code to halt if any number's sequence doesn't eventually go to one, and checking whether that loop ever halts.
My punchline is, I think it's beautiful that even the undecidable, uncomputable problems are only that way because we are lacking a better model. Or at least that's my current understanding of the situation :-)
> 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 time if another program halts operating on some input. I.E. program P takes program H and input I and answers if H run with I halts. I honestly don't know what part of the computational model could be changed to make that not true (besides Oracles or Church-Turing thesis being wrong).
Also, I don't think "online algorithm" means what you think it means. Online algorithms have no more computational power than offline ones; they just can get started with only partial information.
> Similarly, what if the model of math had mechanisms for recognizing paradoxes, or circular logical requirements, etc. I don't think either of those theorems would work anymore.
I don't know what a model of recognizing paradoxes would look like. The 1st incompleteness theorem is based on only a few simple axioms and reasonable rules of deduction. There isn't much wiggle room to make a mathematical model that isn't bound by it, but is useful.
> 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 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.
> 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 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.
> 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 itself powered by a finite program?
A program which keeps growing can make use of all the code it has seen before, all the results it has seen from running code previously. Although any of its inputs are finite strings, there are no theoretical limitations regarding the source of the inputs it can receive. They come from outside.
The core idea of the undecidability of the halting problem is that we can construct a machine M that can ask the halting machine for a bit, flip the bit, give it back to the same static halting machine code, thus forcing it to produce the wrong bit.
Any human in that situation would change their understanding of the situation, and we would tend to afford them a chance to change their answer based on their new understanding. Being able to adjust execution strategy after seeing new information is core to human life. Why do we neglect to provide computers opportunities which are available to all humans?
A somewhat trivial reply to Turing's original negator machine M would be to emit a new version of the halting code which checks for the exact code given by M and then returns the opposite of what was returned when M calls out to H. Then, in the argument, we would need to address the possibility that the H machine called out in M to may provide a different answer when we pass it all back through H again. The argument wouldn't work as-is if we afforded H the ability to respond to the situation.
What would the statement be? "It is not possible, given the information the halting code just received, it could change its answer response to the contradiction of its previous answer." A child can figure out this simple trick - we all understand why it's a trick - why do we not let a computer the same opportunity in our theory?
> So long as you have enough memory, ...
True enough. My point was in fact that if the inputs our machine receives are all needed, we would run out of memory eventually.
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.
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.
> 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.
This doesn't make sense. You said in the same case both that "Z(Z) halts" and "Z(Z) will loop" and then "Z(Z) would halt". So there is a contradiction here.
One assumption that you may not realize without the necessary background is that (a) "Z" is fixed in any particular case, we don't consider counterfactual "Z"; and similarly (b) "Z(Z)" must either always halt or always not halt, by the relevant definition of "program".
Thanks for the response. I was trying to illustrate why my argument doesn't work, but you did a much better job at that.
I may have found what I've been looking for in a related topic called Oracle machines for the halting problem. Part of its definition is that it can't solve problem for machines equivalent to itself, which, I believe, would exclude Z-type programs from the domain.
To put my plea into some formal jargon, "Just because the halting problem is undecidable doesn't mean oracles Turing machines for the halting problem don't exist." Kind of a simple and obvious point in hindsight, but I'm happy with it.
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 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.
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!
"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.
Thanks. I have a math degree, I know that I'm handwaving haha. All the comments are encouraging me to formalize my ideas. Maybe I will make a blog post after some further consideration.
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
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.
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.
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 understanding, you just got pulled into a game that you can't win.
The limitation that is put on the code and in your example too is, although the machine can take in extra input along the way, at a certain point the mathematician gets the last word.
If you have G(H,M) which at each point gives you [0|1]:H', a more interesting question is if what happens if you define M = "if H(M)[0]: print H(M)[1] and then loop". Then, does the printed out H(M)[1](M) produce any contradiction?
Hopefully I'm making sense here! Thanks again for engaging.
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?
"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?
Not every picture of a pipe is a pipe but it's at least conceivable that an actual working pipe can be constructed out of something which happens to be a picture of a pipe. Similarly Godel isn't proving that all statements in a system are paradoxically self-referential. Only that given any system of sufficient complexity, one can conceivably be constructed.
In any event, all of our mathematical proofs are predicated upon the idea that the representation of a mathematical object can be treated in terms of proof as equivalent to the mathematical object. Is "2" the number 2 or is it just a glyph that non-representationally depicts the successor of the first counting number? And if you believe the latter, then how do you go about proving anything about the actual successor of the first counting number without resorting to glyphs?
That's my question. It seems that adding "self reference" to the system makes it more complicated than it would be otherwise. So it's not just a system with enough complexity to let you do arithmetic. You need a system with enough complexity to also do self-reference. And I would say and think that self-reference is complicated.
Do we need self-reference in any other areas of mathematics, than Godel's and related proofs?
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.
The halting problem has that same style of thinking, but the universe doesn't necessarily play by such rules. For one, it's still an open question whether the universe could properly contain a model of itself (hence, needing a model of the universe plus the model isn't a guaranteed absurdity).
> 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).
First an online algorithm is an algorithm that process a stream instead of the full input. It's not because it changes.
Regarding the halting problem, lets assume that you give me a program can change itself and you claim solves the halting problem. Use Turings proof on that and it proves that you have not solved the halting problem for all inputs, because it just gave you one that it produced the wrong answer for.
> reveal limitations of certain models of computers
Modulo weird stuff with black holes or whatever (not that I am qualified to understand whether they count), there are no known counterexamples to the Church-Turing thesis.
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.
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.
I did a University module on Godel' Incompleteness theotem and the complete lecture notes which gave all the lead up, explanation and the proof itself along with lots of othet related material was only about 50 pages in total if I recall correctly.
Others have already mentioned it, but Gödel's incompleteness theorem doesn't need a book-length treatment. My undergraduate mathematical logic class covered the proof in a little more than a week.
It's amazing how math can require so much work for what appears to be a single result, but I spend an entire semester proving a single mathematical theorem and to do that I had to work through an entire textbook, so I don't think it's that unusual.
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 different ideas end up being very related to one another. Maybe I am romanticised it and the fact that I regret not going for pure math, but there is beauty in all those abstractions that fit together so nicely.
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.
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.
Kevin Hartnett's popularizations of mathematical research are amazing, I've never seen anything like them before. (Said as a complete amateur with sketchy coverage of undergraduate pure math).
Makes you wonder what's the most impactful thing you could build given the possibility of seven years of isolation and single-minded focus.
Would be interesting to know, at which point did Freedman decide to commit full time to his research---based on what, an intuition? And how did he decide to stop at 7 years and not 4, 9 or 10?
This is advanced stuff for me but I'll still be getting a copy of
_The Disc Embedding Theorem_ to support this kind of niche research. Findings like these could be stepping stones towards bigger discoveries in the future.
My buddy had “beat a Fields medalist at a foot race” on his CV for a while after completing the Pier to Peak half marathon faster than (a ~60 year old) Prof Freedman.
I’d run to Goleta beach playground with my kids and would see Freedman wander down from Station Q and bust out a few chin ups on the monkey bars.
The part I find most interesting is that (as I understand the article), Freedman's proof relies on a meta-proof that details not worked out in the base proof could be ignored:
"But there were places where he couldn’t quite complete the picture — as if he were creating a portrait and there were some aspects of his subject’s face he couldn’t see. His last move, then, was to prove that those gaps in his picture — the places he couldn’t see — didn’t matter from the standpoint of the type of equivalence he was after. That is, the gaps in the picture could not possibly prevent the Casson handle from being homeomorphic to the disc, no matter what they contained."
A common approach to proving a broad claim when there’s no straightforward proof is to figure out all of the entities that have the potential to produce a counterexample, break them up into a finite list of categories, and go through category by category proving, often with very different approaches depending on the category, that each category cannot contain a counterexample.
A major theorem proved in this style was the classification of finite simple groups. Not only was it done in this style, it frequently serves as a major component in other proofs of this style, since theorems about other kinds of groups can sometimes be re-expressed as claims about finite simple groups, and then checked category by category.
EDIT: This is also part of why sometimes the first proof of a theorem will be very long, but someone will later use the insight of the first proof to produce a much shorter proof. The first proof will basically be a proof that the general claim breaks down into a (possibly very long) list of separately probable lemmas, followed by a proof of each of the lemmas. These may not overlap very much, leading to proofs that are very long and take a lot of background to understand. Once the result is known to be true, it may be worth the effort for the original author or someone else to refactor the “proved it can’t be disproved” proof into a much shorter direct proof.
I 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.
Most people don’t as doing so requires a level of talent, intelligence, and work ethic/determination that’s in the upper tail of human distribution.
Paradoxically, many people who could probably do underestimate their talents while others who can’t/should t overestimate theirs. The universe is funny in that way.
So who gets credit for proving it? Freedman, the original author from 1981; or the authors of this book?
If Freedman's proof has so many gaps, should it be considered more of a proof outline, or a motivation for believing a conjecture, and the current book be considered the actual proof?
Or does Freedman get the glory? In that case, there's not much incentive for people to do what these book authors did. Which I suppose is why it took 30 years, and is only happening now because they "were captivated by the beauty of Freedman’s proof and wanted to give it new life. "
It's not a strict exclusive-or choice. Credit will accrue to both Freedman and the authors of this book, because both advanced the state of the subject. And eventually perhaps further credit to someone who publishes a machine-verifiable proof, or finds a simpler way to understand the theorem.
It's common for complicated proofs to have little gaps that got past the referees. The basic standard of whether the proof is valid is that if you do find a gap in the written version, the author can say "oh yeah, you can fix that by doing X", making some small patch. It's like finding a bug in a program that the author can fix right away once you file a bug report. If the author is unable to fix the bug despite a reasonable amount of effort, then there is a problem. You get credit if you can fix it where the author couldn't. Otherwise it's almost like trying to invalidate a proof over a misspelling.
In the case of Wiles' proof of FLT, someone found a bug, Wiles worked unsuccessfully for something like a year trying to fix it, basically concluded that FLT was not really completely proved after all (i.e. he had "merely" made enormous progress, but not actually closed the ticket). Then right after more or less giving up, he and Richard Taylor figured out how to fix the bug, so it came out ok after all. Of course Taylor now gets a slice of the FLT credit.
Well, thank God lots of scientists (mathematicians in this case) understand that transmission of knowledge is as important (or more so) as novelty. And that is their incentive.
This distinction has been called an "open exposition problem", versus an "open research problem".
Once Freedman's proof was accepted, it was no longer an open research problem; on the publication of this book, it will (hopefully) no longer be an open exposition problem.
The phrase was coined by Timothy Chow in his paper A Beginner's Guide To Forcing [0];
> "All mathematicians are familiar with the concept of an open research problem. I propose the less familiar concept of an open exposition problem. Solving an open exposition problem means explaining a mathematical subject in a way that renders it totally perspicuous. Every step should be motivated and clear; ideally, students should feel that they could have arrived at the results themselves."
According to a sister comment, the paper contains a meta-proof that shows that many of the gaps do not matter in showing the equivalence.[0] I don't know if this is true or not, I'm just connecting the discussions.
I'd be interested in whether proofs like these will be formalized in proof assistants that can be checked with computer code, so that it removes doubt of error. It's something in math I'd like to see become more prevalent.
Something at this level is still far away, but it should be possible in theory. Last time I checked, there was still a lot of work to be done with formalizing geometric objects in Lean (the only proof assistant I have experience with). We are more in the stage of formalizing proofs from undergraduate books, whereas the proof of the 4-dimensional Poincare conjecture is multiple orders of magnitude more difficult.
From my understanding and limited experience, formalizing complex objects is quite difficult. A long proof where the objects are integers or algebraic relations might be easier than even defining a manifold. For example, with Lean, it was a lot of work to even define a perfectoid space -- which, to be fair, is a complicated object -- much less, say anything interesting about it.
If someone has more experience with other proof assistants, I'd be interested to hear about how far away a proof like Freedman's would be. My understanding is that each one (coq, agda, lean, etc) has certain drawbacks or benefits and can describe some concepts more easily than others, but "high-level" proofs are few and far between for all. For example, Coq has a verification of Feit-Thompson Theorem which is really cool, but I don't think there are many complex objects in there. As far as I know, it's groups, linear algebra, generator and relation computations -- all of which are pretty well handled by computers. On the other hand, to even begin a verification of Fermat's Last Theorem, you would have to first build up the entire scaffolding of modern (well, second half of the 20th century at least) algebraic number theory, quite a feat in itself.
The problem is, once you have a proof that everyone agrees is correct, what's the incentive to painstakingly translate it into something a computer also agrees is correct?
Yes, you might turn up some "bugs" in the proof, but proof bugs can almost always be ironed out. It's a very rare proof that is accepted and then falls apart later. If proofs were as "buggy" as computer programs- falling apart all the time- then there'd be a much bigger appetite for proof checkers. But as it is, mathematical peer review seems to work awfully well.
I agree that it's rare that a proof is accepted and falls apart later, but it does happen occasionally.
Somewhat famously, Voevodsky turned his attention to mathematical foundations, including proof assistants, at least in part because he was spooked that a part in one of his big papers was later shown to be incorrect. (Interestingly, someone much less known pointed this out in a preprint but it was, from my memory, largely ignored for some time -- who's going to believe a nobody versus a Fields Medalist?) There's a talk that Voevodsky gives at (I think) IAS, where he mentions this.
The whole talk is interesting, but slides 8-13 talk about the topic at hand. In particular:
> This story got me scared. Starting from 1993 multiple groups of mathematicians studied the “Cohomological Theory” paper at seminars and used it in their work and none of them noticed the mistake.
> And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.
...
> It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.
There's plenty of incentive to do that actually, since a translation of a proof that had not been formalized before yields a much clearer proof than anything a human could write on her own. This is doubly true when some "bugs" are found and "ironed out" in the process - even seemingly trivial bugs can trip up the reader and obscure interesting sr
structure. In fact, a truly novel formalization is pretty much publishable work in and of itself. The problem is not incentives; it's more of a lack of willingness to work in an area that's very fragmented still and makes it way too hard to reuse existing results.
It's possible, but difficult. Proofs written by humans tend to not include a bunch of relevant details and assumptions. They consist of lines like "We have some property/object/logical statement X, then by theorem Y we have Z", but often don't state how exactly they are using theorem Y to get result Z. There's often some additional algebraic or logical manipulation, or some simplification of terms, or implicitly using some other theorem or lemma that seems obvious to the writer.
Getting a computer to automatically find proofs of statements is difficult (impossible in general), and I wouldn't be surprised if converting a standard human-written proof into a formal proof system is just as hard.
> I'd be interested in whether proofs like these will be formalized in proof assistants that can be checked with computer code, so that it removes doubt of error.
"I probably didn’t treat the exposition of the written material as carefully as I should have,” said Freedman.
That's a pretty sad (if self aware) statement for someone who gets paid $1M/yr to find arrangements which might make quantum decoherence effects lower for computation ... or not. The editors certainly won't make that much, but at least there's an afterward by Freedman.
I 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 have notes, but even still.
What is the secret behind it? How do people get so good with Maths? Is it truly study,study & study? .. I hadn't even herd of the terminology of co-efficient until today. Let alone something like this.
High school math does not look much like research math.
High school math is highly concerned with teaching 'algorithms' that compute answers, like long multiplication, long division, the quadratic formula, completing the square, synetic division, u-sub integration, ...
Most mathematicians don't work with calculating things. Rather, they're more interested in _generally_ characterizing how objects behave (and _proving_ that that characterization is actually correct)
For example, the definition of "continuous" you learn in pre-calc is probably something like: if you compute a function's limit, you get the same thing as computing the function.
The topologist's definition is that the function's inverse map preserves openness.
These are basically unrecognizable as being the same thing, but in fact they are. And the second doesn't actually reference calculation or even anything identifiable as numbers!
I believe this is a significant cause of not understanding "why" despite understanding "how". As an example, I remember in pre-calculus we spent at least an entire unit on partial-fraction-decomposition. Partial fraction decomposition is a strange algebraic manipulation that is basically only important to integrating rational functions -- something you don't do until at least a year later, and which doing by hand is basically pointless because computers are better at it than humans.
They also require very different kinds of intuition. Building intuition is hard, but important for people studying math. Working through many different examples and problems and applications can help you build intuition.
But I don't really have any advice for how to make math stick better, but just want to share that the mathematics you learn in high school is not representative of the entire field.
If you ever want to get a taste of "higher math" without having lots of prereqs, point-set topology and group theory are two (very different!) fields that are also fairly accessible.
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, the sum of F_n x^n over all nonnegative integers n. Call this thing F(x).
What happens if we add up F(x) and x F(x)? Well, x F(x) is just the same sum but with all the numbers shifted over by 1. It's the sum of x F_n x^n, or the sum of F_n x^(n+1), or the sum of F_(n-1) x^n, with the proviso that there isn't an x^0 term. So when we add this to the sum of F_n x^n, we get the sum of [F_(n-1) + F_n] x^n, with again the proviso that the x^0 term is just F_0 x^0 = 0.
But, aha!, F_(n-1)+F_n is just F_(n+1), at least when n >= 1. So this thing equals the sum of F_(n+1) x^n, except that once again we need to be careful about n=0; more precisely what we have is the sum of F_(n+1) x^n, minus 1. (Because F_1 is 1, but the actual x^0 term is 0.)
And the sum of F_(n+1) x^n equals the sum of F_n x^(n-1), or F(x)/x.
In other words, we have F(x) + x F(x) = F(x)/x - 1, or equivalently (1 - x - x^2) F(x) = x, or equivalently F(x) = x / (1 - x - x^2).
This is already pretty neat -- who would have thought that that big sum, involving the Fibonacci numbers which are defined in terms of a sort of recursive-adding process, would come out to something so simple?
Now comes the coup de grace, which is the bit that uses partial fractions. We can write that denominator as (1-ax) (1-bx) for some numbers a,b. We'll figure out what a,b actually are in a moment -- that's just solving a quadratic equation. For now, looking at the coefficients of x and x^2 we note that a+b=1 and ab=-1. And now we can do the partial-fractions thing. We know that we'll have x/(1-x-x^2) = p/(1-ax)+q/(1-bx) for some p,q. That means that x = p(1-bx)+q(1-ax), so p+q=0 and pb+aq=-1 or p=1/(a-b). That is, F(x) = 1/(a-b) [1/(1-ax) - 1/(1-bx)].
Why bother doing this? Because the fractions we now have are easy to expand in powers of x. We have 1/(1-ax) = 1 + ax + a^2x^2 + ... and 1/(1-bx) = 1 + bx + b^2x^2 + ... So F_n, the coefficient of x^n in F(x), is just 1/(a-b) [a^n - b^n].
Finally, we ought to work out what a,b actually are. It turns out that a = [1+sqrt(5)]/2 and b = [1-sqrt(5)]/2; that is, a is the famous "golden ratio" sometimes called phi, and b = 1-a = -1/a. So a-b is just sqrt(5).
So: the nth Fibonacci number is exactly (phi^n - (-1/phi)^n) / sqrt(5). Isn't that nice?
(Since |b|<1, the term b^n/sqrt(5) is always smaller than 1/2 in absolute value, which means that F_n is also always the closest integer to phi^n/sqrt(5).)
For the avoidance of doubt, none of this has anything at all to do with the disc embedding theorem. I just thought it was worth clarifying that partial fractions aren't just a one-trick pony used only for integrating rational functions; there are other situations in which representing something in terms of partial fractions gives useful insights into its behaviour.
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.
I fully agree that (high) school math is mostly calculus and very different from university/research math. I would recommend parent to start exploring what math actually is, which fields there are and where they come from, what some famous open problems are and what beauty means to mathematicians.
Good popular maths books are e.g. The Music of the Primes by Marcus du Sautoy [1] or Fermat's Last Theorem by Simon Singh [2].
It's also important to note that there are no shortcuts - it takes at least 1-2 years of studying maths to start to understand the why.
One possible starting point is Book of Proof by Richard Hammach[0]. It's free. It will show you the rudiments of how math is actually done and thought of. Another good choice is Mathematical Proofs: A Transition to Advanced Mathematics by Chartrand/Polimeni/Zhang. These books have no prerequisites(good to go if you know how to do arithmetic with fractions/decimals; not that these are strictly necessary, rather that's about the level of comfort with math one should posses). Search on Amazon and you'll see there are a ridiculous number of books on this subject of all varieties of ways of presentation. Almost every week a new book pops up, it seems. Note, intro-to-proofs books are not only for novices, though. There are kinds written for advanced undergrads and beginning grad students as well. For example: Mathematical Concepts by Jugen Jost. This speaks to the wealth of the kinds of math books available.
Concurrently and/or after that you can study introduction to any of linear algebra, discrete math, group theory, analysis of reals, combinatorics, number theory, graph theory, algorithms, probability, category theory...whatever. Each of these are very deep subjects and there exist hundreds(if not 1000s of books from the past, current and future) of every imaginable level, depth and presentational quirk. Again check Amazon for titles. Check libge*n for actual files.
The following intro books are so easy anyone and they momma can read these with utmost ease:
Discrete Math by Susanna Epp
How to Think about Analysis by Lara Alcock
Linear Algebra: Step by Step by Kuldeep Singh
Real Analysis: A Long-Form Mathematics Textbook by Jay Cummings
A Tour Through Graph Theory by Karin Saoub
The above mentioned books are a few examples of elementary books that you can get started with right this minute.
Note and remember the wealth of possible books, though. For example, consider the subject of math analysis.
We can break it into three general parts: real analysis, complex analysis, functional analysis. Each can be further taken apart into measure theory, vector spaces, topology etc. Further, topology alone branches out into point-set topology, algebraic topology, differential topology etc. Each of these fly under many different names. Say, vector spaces is a huge part of linear algebra. For the beginners, it's usually the finite dimensional vector spaces (aka the title of a famous linear algebra book) version whereas the infinite version will take you into func analysis. Vector spaces are also usually included as a chapter in books on abstract algebra as they are an algebraic structure just like groups, rings, modules. But if there is linear algebra, there must be non-linear algebra too. Well, yes. Roughly, it corresponds to what's called algebraic geometry. It never ends.
The point is every topic in math has loads of books dedicated to it. In turn every topic has a (sub)^{n}topic and there are tons of books on those. Each of the books come in elementary, quirky, armchair enthusiast, average undegrad student, middling grad student, kickazz graduate math aficionado, researcher, undergrad researcher wanna-be etc levels. There are also olden books, classics, those just published (say, at most 5 years ago) and up-and-coming ones. Also, each term in math has bagillion synonyms. So multiply the number of books above by n. I am not even gonna mention books written in different languages and lecture notes that are available for free online. A lot of published book often spend years as a free set of lecture notes before ending up on Amazon as a newly published book. There are also Olympiad books, proof compilations, capstone compilations, intro-to-research books, those that prove a single theorem and in the process go through tons of disparate math etc Take advantage of all of this.
It's all genes and some effort. Without the two, it's hard to get anywhere. People with super-high IQs are able to make the necessary epiphanies to 'see' the answer and prove the intended result. Genes play a role in everything, from marathon times, height, life expectancy, to lifting totals, to even math aptitude. no getting around it. Math , much more so than other fields, is heavily dependent on innate factors such as talent.
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.
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.
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.
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.
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) <= n, for positive n. Seems simple right? But first you have to multiply by 60 so that you're working over actual naturals. But then you have to contend with the fact that n / 15 * 15 <= n itself needs proof (they're not just equal, since n / 15 actually represents the 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.
> Are proof checkers much more complicated than LaTeX?
In terms of lines of code, no. In terms of the learning curve, yes -- latex does a very good job of getting out of the way and letting a mathematician just write in English, where proof assistants require rigid structure that doesn't remotely resemble how (most) mathematicians think.
In terms of runtime, oh my god, get out of town.
> 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.
Fair point. I'm coming from the perspective that mathematicians don't like to fill in pesky details that experts in their respective fields can figure out in an hour or ten.
Getting a proof, even in one that is amenable to computer verification into a form where you can actually verify it is a monumental task, like it can easily take multiple experts multiple years.
Adding to this problem the intersection of mathematicians who understand computer aided verification and who understand a particular piece of research mathematics is often empty, and even if there are a handful of people who could do the necessary work they're often busy doing more interesting stuff.
Finally I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. I think its unlikely that this will happen for a long time, for the simple reason that to feed a proof into a computer requires someone to dissect the proof to its logical bare bones in the first place, and the person doing the dissection is likely to notice any errors before they get round to feeding the problem into the computer.
> I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods.
Right, because that's not how it works. Errors aren't discovered after the proof has been translated into machine language because that is the only step of the verification. As soon as the code is written, the proof is verified. Necessarily, then, any error discovery has to happen before that.
> Why don't serious math journals require programmatically checked proofs for all publications
Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe (and, crucially, that their peers also already believe) into a computer system.
That's not to say proof checkers aren't interesting in their own right, but there's lots of really quite good reasons why mathematics goes without them almost all of the time. Formal methods bring a lot to computing, where our programs fall apart constantly, but mathematical proofs almost always don't fall apart. And in computing, almost all programs don't have formal proofs of correctness! If any area needs them, it's in computing, not mathematics. You might as well ask why every compiler doesn't come with a proof of correctness: because it's already hard enough to build a compiler, let alone the monstrosity that would be a formal proof.
The added benefit to a computer-checked proof is usually small to nil, and it's a ton of work. Like, way more work than just writing the proof.
More often than not mathematicians look for proofs of things they (and others) are already convinced in being true (or even already know for a fact). The automatic proof checking is just for that - making sure the proof is correct.
This sounds like a very dangerous attitude, considering that making any tiny mistake will cause you to be able to prove any statement. Of all people mathematicians should understand that.
Empirically, proofs with bugs get ironed out into proofs with less bugs, and the results almost always end up standing. Why mathematical proof seems to be as good as it is at avoiding proving false statements is a matter of contention, but practically speaking it works. There's very little incentive to computer check proofs because, as a practical matter, mathematics is not plagued with false "theorems."
Computing, on the other hand, is plagued with broken programs, and formal methods are still a very specialized area, even though the potential benefits are much greater in computing than mathematics.
The answer given there by Manuel Eberl is more or less what I was trying to get at (and he is far more knowledgeable about it than I am). Lots of mathematicians find that the existing level of rigor in the field is enough.
Obviously the people who like proof assistants disagree, and they may be right. It could be that modern theorems are just too complicated to be adequately evaluated by unassisted humans. But mathematicians have been getting along just fine without them for a long time, so "why aren't we requiring computer-checked proofs of everything" has a very straightforward answer: mathematicians writ large aren't convinced of the benefit yet.
This is largely because in modern mathematics, people ignore or won't build on proofs that are too complicated for them to follow, and rely heavily on trust and networking effects for the remaining proofs that are too useful to ignore. Plenty of results (including big results) are published in mathematical journals each year, which are "known" to be flawed or sketchy, but never have a formal rebuttal, and if you want to build on a proof that doesn't have much followup work, and are having trouble understanding its argument, you're expected to ask around and find out whether the proof is worth pursuing or not. Proof assistants would enable people to trust much more complex proofs from much more junior mathematicians, rather than essentially requiring the community to reprove the same results over and over until they're satisfied, and IMO this is holding back mathematics more than many mathematicians realize.
> A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe into a computer system.
I guess the question is which of "convincing a human" or "convincing a computer" is considered the higher bar.
In any case, uncovering "what you believe that isn't so" is pretty important.
Right, but the ordinary methods of doing mathematics seem to be so good that the vast effort required to encode proofs well enough for a computer to check vastly dwarfs the benefit, at least for now.
There's obviously been a lot of work done on proof assistants and maybe it will become easy and natural to formulate most proofs in a way a computer can check, but it's not anywhere close to that yet. The book explicating the proof discussed in the article is already 500 pages long, translating that into something a computer could check just isn't at all feasible yet.
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.
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.
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?
> 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?
The point of the checked proof is that your final theorem is almost definitely correct (you did not make mistakes in your deductions, unless the proof checker has a serious bug) if you can convince computer it derives from your axioms.
You can convince humans without your proof being correct thought, because they might not spot an error.
My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?
The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.
That's assuming you ascribe to viewing math as science.
> Why don't serious math journals require programmatically checked proofs for all publications
Presumably it has something to do with why formalized mathematics is rare: it's hard. Even relatively simple concepts become quite hard to deal with when fully formalized. I suspect that mathematics on this level is simply not amenable to the treatment that you envision (at least today).
> ...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?
I kinda feel like this question answers itself. On the other hand, I can't imagine this quagmire lasting another century, but the machine-assisted proof ecosystem hasn't reached adolescence yet.
For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve.
Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.
There are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.
(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.)
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.
Formality is technically the degree of mathiness applied to a domain, since formal logic and any other framework of formalization decomposes to mathematics.
So... it's a tautology. Math is the most mathy math. Biology or psychology are less mathy maths.
Having provablility holes in the formal system doesn't imply the existence of other systems that could be decomposed from currently known or unknown symbols. In this universe, information at the level of string theory seems to describe the limits, so math, as she is wrote, is as formal as it gets.
The map is not the territory, so math, as a map, will always be less "formal" than reality itself. It's pretty firmly in second place, though.
