I'm reminded of Sheryl Sandberg's much-ballyhooed concept that if women only "Lean In" to conversations in work meetings, equality in the workplace would automatically result. It seems equally magical thinking to believe that if mathematicians Lean In, understanding will follow.
> However, it’s impossible to prove formally that the “more modern version” is equivalent to Wiles’s original proof without formalizing the latter, so I don’t know why the computer scientists who were obsessing about this in 2005 would accept this substitute for the original.
You have returned to this point many times and I still entirely don't understand why it is relevant.
First note that even if the original version were formalized it would not be possible to prove they were equivalent, for multiple reasons: First, there is not even a well-defined mathematical notion of the equivalence of two formal proofs other than the literal equivalence of two proofs containing the same sequence of steps or, for intuitionistic proofs, the notion of two proofs producing the same function (but Wiles' proof is presumably not intuitionistic and anyways any two functions arising from intuitionistic proofs of Fermat would be the same as they would be functions from the empty set to the empty set). Second, the proofs are of course not equivalent in an informal sense, because the more modern version is, I assume, different in incorporating more modern ideas that allow certain steps of the original proof to be sketched.
But I don't see why computer scientists should care about the difficulties with proving a potential new proof is equivalent to an earlier proof. Was that ever their goal? The original problem of Jan Bergstra specifies "a proof of Fermat's Last Theorem, as proved by A. Wiles in 1995". I think the "as proved" clause is meant to provide proper credit while clarifying if necessary which theorem is meant. "a proof" clearly implies that any proof will do.
The document of Wim H. Hesselink you linked makes clear that the reason Wiles' proof is important to the author is because it also proves the modularity conjecture for semistable curves. It's clear Wim would prefer a simpler proof if it also proves this modularity statement - this is made clear in the third-to-last section. But of course one can verify that a proof proves the modularity conjecture for semistable curves without also verifying that it is equivalent to Wiles' proof.
More broadly I don't see the point in any situation of proving some formal proof is equivalent to some informal proof, and since as you point out the impossibility of this is a tautology, I think it's not reasonable to assume that people who are interested in formalization are trying to achieve this type of proven equivalence. Rather I think people have different motivations. Among these are to be sure that the theorem is correct, which does not require being sure that any past proof is correct.
But even if one's goal is to be more confident that a certain published proof is correct, there is no need to prove that the published proof is equivalent to a formal proof. Simply producing a formal proof and observing that this looks similar to the published proof gives increased confidence that the published proof is correct (in the informal sense used by ordinary mathematicians). Why is this? At least sometimes a serious error exists in a published proof. A few times, such errors have been detected in attempts to formalize a proof (i.e. produce a formal proof similar in some respects to the original proof). On the other hand no serious error can be detected if the proof is not wrong. So it follows that if one produces a formal proof without finding a serious error, the probability that no serious error exists is greater than previously, even if it's possible that a serious error in the original proof was not detected since a somewhat different proof was in fact formalized.
In the first place, I don't much like writing to specters. It's unlikely that the comment to which I am responding was written by a ghost, or a bot, or an extraterrestrial, but the comment itself raises the issue of probabilities and I can't rule any of these out. But I'll make an exception for once and reply to an anonymous comment — just once — since it raises legitimate points.
As Octave said in Renoir's "Rules of the Game":
"You understand, on this earth there's something terrible, namely that everyone has their reasons."
For many years Kevin and others were claiming that their motivation for formalization was concern about the correctness of the proof, and I'm sure I can find public references — not only in my private exchanges with a computer scientist — that specify that they have Wiles's original proof in mind. Set theorists have expressed a different but related concern, about the strength of logic needed to prove FLT, and again the reference is to Wiles's proof — Colin McLarty's article at https://www.jstor.org/stable/20749620 provides a wonderful discussion of these issues. What's terrible, as Octave might have said, is that as soon as I address such reasons, along comes an anonymous creature of some sort to bring up a whole different set of reasons.
One gets the impression that the formalization community, including its extraterrestrial members, has a problem of concentration. Evidence of this is AGNT's attempt (that is Morse code, isn't it?) to pass off confidence and probability as a substitute for certainty in the last few lines. It's hard to overstate how monumental this concession to pragmatic considerations appears from the standpoint of metaphysics. As a logical fall from grace this can only be compared to Satan's expulsion from heaven in the last few lines of Paradise Lost, book VI:
"Let it profit thee to have heard/ By terrible example the reward/ Of Disobedience."
My own motivations are not hard to guess. The more we can dismiss spurious arguments for formalization, the more attention we can give to the arguments that remain. I am particularly interested in distinguishing the motivations that arise within the profession from those that originate in the tech industry. My first inclination is to treat the latter as alien intrusions. As for the former, I judge them in the light of McLarty's reminder that "mathematics is not only technical" — "the point" upon which his article is a masterful elaboration.
My intention is not to conceal my identity - this is just the substack account I happened to have when I started reading your blog. In fact I thought you had figured out who I was when I commented previously, but I would be happy to clarify if necessary.
I am not really a part of the formalization community - I have just enjoyed following some of the discussion about it. Certainly anything wrong with my comment shouldn't be blamed on them (or on the tech industry).
If an engineer tells you they have concerns about the safety of a bridge, and their response to this is to build a new bridge, would your reaction be to point out that since the new bridge is not the same as the old bridge building the new one will do nothing to help with concerns about the old? Or is the reason that the engineer finds their concerns about the old bridge concerning because they would like there to exist a safe bridge for people to cross?
I've read Colin McLarty's article before, and I just read it again. It seems clear to me that he is not concerned with Wiles' proof as an immovable object but instead with whether it can be modified to fit within a specific weak formal system. It's unambiguous that this is at least one concern discussed in the article - whether a proof of Fermat, not necessarily Wiles's, exists in some weak system like PA or a weaker one.
Your metaphor of a fall from grace would be apt if at some previous point we had access to metaphysical certainty about mathematical proofs, which we have given up to obtain formalized proofs instead. But no such thing has ever existed - there's only been fallible human beings trying their best to concentrate at they stare at a page, a blackboard, or at each other.
Saying that mathematics is not only technical suggests by omission that mathematics is technical in part. It seems to me that technical improvements to the technical part of mathematics may be of some value, even, symbiotically, to the non-technical aspects of mathematics.
As I wrote, everyone has their reasons. I try to respond to them one at a time. When I address those concerned with metaphysical certainty I am accused of not addressing someone else's reasons. You may think the search for metaphysical certainty is a fool's errand, and I may agree with you, but there are others who take it very seriously. Many of them have been quoted in this newsletter. You can are find direct quotations from Kevin that strongly suggest that such concerns motivated his initial interest in proof verification. His grant proposal stresses different motivations, among them the hope that, as Margaret Wertheim so felicitously put it, "if mathematicians Lean in, understanding will follow."
Your logic of responding to reasons one at a time makes total sense. I just want to encourage you to consider more carefully alternate interpretations of someone's words when you believe that they are expressing reasons for which this particular argument is an apt reply.
Let me point out that I have read most of the posts of this blog, and noticed several times where you reference the difficulty of proving two proofs are equivalent. This difficulty is only relevant if someone is (1) interested in metaphysical certainty, and not practical certainty, (2) interested in certainty that a proof is correct, and not certainty that a theorem is correct, (3) cares about a specific proof, and isn't willing to switch to a new proof. I can't remember a single time you brought this up that I was convinced that the person satisfied (1), (2), (3).
In particular I remember Kevin being very concerned about the number of papers in the literature that contain serious errors, and the difficulty in sorting out which parts are dependent on the error and which aren't - this is a practical concern that formalization would probably help with and not one about metaphysical certainty.
"On pp. 326-327 (of Mechanizing Proof), Donald MacKenzie quotes a computer scientist who argued that mathematicians' failure to perform proofs formally, "by manipulating uninterpreted formulae accordingly [sic] to explicitly stated rules" proves that "mathematics today is still a discipline with a sizeable pre-scientific component, in which the spirit of the Middle Ages is allowed to linger on" [Dijkstra 1988], a philosopher (Peter Nidditch) who claimed that "in the whole literature of mathematics there is not a single valid proof in the logical sense," and another philosopher who doubts "that mathematics is an essentially human activity" [Teller 1980]. "
For obvious reasons I won't try to PROVE that Kevin's concerns are identical with those of the philosophers and computer scientists quoted here. See also MacKenzie, "Computing and the cultures of proving," Phil. Trans. R. Soc. A. (2005).
But none of these satisfy (3) - they display no attachment to a particular informal proof that they hope to rescue by formalization. If mathematicians simply stopped publishing informal proofs and wrote only formal ones (which would horrify me about 70% as much as it would horrify you), the computer scientist whose definition of the Middle Ages extends into the early 20th century would clearly be satisfied that mathematics is not still a discipline with a sizeable pre-scientific component, even if nothing is done about the past proofs. Similarly publishing a single formal proof would theoretically satisfy Peter Nidditch (although this is a bit strange as the mathematics literature clearly contains formal proofs, e.g. as examples in logic textbooks or in that one journal that only publishes formal proofs in Mizar).
I am probably taking this further than you intended, but there is a curious "quasi-borderline" example in "The Tempest", Act 5, Scene 1:
Their understanding
Begins to swell, and the approaching tide
Will shortly fill the reasonable shore
That now lies foul and muddy.
While this is being said, Alonso and the court party are still "under the influence of charm" and "bereft of senses", so, arguably, not fully "animate".
And here is an example from Macbeth (Act 3, Scene 2) of a "verse attributing `agency' to an inanimate object" (which is incidentally the origin of the expression "invisible hand"):
Yes, it is not easy to characterize what is going on here. There are semantic shifts in language and thought that take place without much regard for pattern in time and place. How are LLM's to capture these? For example, what would it make of the various uses of the word 'diagram' in mathematics? How would it avoid errors of the sort it made when you queried it? Buzzard appears to be promoting LEAN as an 'assistant' ... that seems quite plausible and maybe even useful. We don't seem to have found a good role for LLM's just yet...maybe when Birnam Wood comes to Dunsinane?
If you are suggesting that LLMs will find their proper role in time to avert further massacres, or on the contrary to initiate a new series of massacres, I would not disagree.
In the meantime, I hope to address this specific question in the continuation of the previous post.
the Macbeth line appears to have been misunderstood both by GPT and the author of the post. By 'sensible' to sight and feeling Macbeth means 'able to be sensed by' feeling and sight ...in the old philosophical jargon, these are examples of 'sensibilia' ...the different senses were said to have different things they could sense...their sensibilia (Aristotle discusses this generally in Books II and III of de Anima and specifically in de Sensu). Macbeth does not attribute feeling, sight or understanding to the dagger. Somewhere in the 17th c the notions of 'object(ive)' and 'subject(ive)' were inverted. Today 'sensible' refers to the person sensing, not the thing sensed.
Thank you. The author didn't take the time to check (and has no excuse). Ernie Davis made the same point, but without the etymological history; I've acknowledged this in a new footnote.
If ChatGPT is capable of misunderstanding then presumably it's also capable of understanding. Probably a word other than "misunderstanding" better captures what did or didn't happen.
I'm reminded of Sheryl Sandberg's much-ballyhooed concept that if women only "Lean In" to conversations in work meetings, equality in the workplace would automatically result. It seems equally magical thinking to believe that if mathematicians Lean In, understanding will follow.
> However, it’s impossible to prove formally that the “more modern version” is equivalent to Wiles’s original proof without formalizing the latter, so I don’t know why the computer scientists who were obsessing about this in 2005 would accept this substitute for the original.
You have returned to this point many times and I still entirely don't understand why it is relevant.
First note that even if the original version were formalized it would not be possible to prove they were equivalent, for multiple reasons: First, there is not even a well-defined mathematical notion of the equivalence of two formal proofs other than the literal equivalence of two proofs containing the same sequence of steps or, for intuitionistic proofs, the notion of two proofs producing the same function (but Wiles' proof is presumably not intuitionistic and anyways any two functions arising from intuitionistic proofs of Fermat would be the same as they would be functions from the empty set to the empty set). Second, the proofs are of course not equivalent in an informal sense, because the more modern version is, I assume, different in incorporating more modern ideas that allow certain steps of the original proof to be sketched.
But I don't see why computer scientists should care about the difficulties with proving a potential new proof is equivalent to an earlier proof. Was that ever their goal? The original problem of Jan Bergstra specifies "a proof of Fermat's Last Theorem, as proved by A. Wiles in 1995". I think the "as proved" clause is meant to provide proper credit while clarifying if necessary which theorem is meant. "a proof" clearly implies that any proof will do.
The document of Wim H. Hesselink you linked makes clear that the reason Wiles' proof is important to the author is because it also proves the modularity conjecture for semistable curves. It's clear Wim would prefer a simpler proof if it also proves this modularity statement - this is made clear in the third-to-last section. But of course one can verify that a proof proves the modularity conjecture for semistable curves without also verifying that it is equivalent to Wiles' proof.
More broadly I don't see the point in any situation of proving some formal proof is equivalent to some informal proof, and since as you point out the impossibility of this is a tautology, I think it's not reasonable to assume that people who are interested in formalization are trying to achieve this type of proven equivalence. Rather I think people have different motivations. Among these are to be sure that the theorem is correct, which does not require being sure that any past proof is correct.
But even if one's goal is to be more confident that a certain published proof is correct, there is no need to prove that the published proof is equivalent to a formal proof. Simply producing a formal proof and observing that this looks similar to the published proof gives increased confidence that the published proof is correct (in the informal sense used by ordinary mathematicians). Why is this? At least sometimes a serious error exists in a published proof. A few times, such errors have been detected in attempts to formalize a proof (i.e. produce a formal proof similar in some respects to the original proof). On the other hand no serious error can be detected if the proof is not wrong. So it follows that if one produces a formal proof without finding a serious error, the probability that no serious error exists is greater than previously, even if it's possible that a serious error in the original proof was not detected since a somewhat different proof was in fact formalized.
In the first place, I don't much like writing to specters. It's unlikely that the comment to which I am responding was written by a ghost, or a bot, or an extraterrestrial, but the comment itself raises the issue of probabilities and I can't rule any of these out. But I'll make an exception for once and reply to an anonymous comment — just once — since it raises legitimate points.
As Octave said in Renoir's "Rules of the Game":
"You understand, on this earth there's something terrible, namely that everyone has their reasons."
For many years Kevin and others were claiming that their motivation for formalization was concern about the correctness of the proof, and I'm sure I can find public references — not only in my private exchanges with a computer scientist — that specify that they have Wiles's original proof in mind. Set theorists have expressed a different but related concern, about the strength of logic needed to prove FLT, and again the reference is to Wiles's proof — Colin McLarty's article at https://www.jstor.org/stable/20749620 provides a wonderful discussion of these issues. What's terrible, as Octave might have said, is that as soon as I address such reasons, along comes an anonymous creature of some sort to bring up a whole different set of reasons.
One gets the impression that the formalization community, including its extraterrestrial members, has a problem of concentration. Evidence of this is AGNT's attempt (that is Morse code, isn't it?) to pass off confidence and probability as a substitute for certainty in the last few lines. It's hard to overstate how monumental this concession to pragmatic considerations appears from the standpoint of metaphysics. As a logical fall from grace this can only be compared to Satan's expulsion from heaven in the last few lines of Paradise Lost, book VI:
"Let it profit thee to have heard/ By terrible example the reward/ Of Disobedience."
My own motivations are not hard to guess. The more we can dismiss spurious arguments for formalization, the more attention we can give to the arguments that remain. I am particularly interested in distinguishing the motivations that arise within the profession from those that originate in the tech industry. My first inclination is to treat the latter as alien intrusions. As for the former, I judge them in the light of McLarty's reminder that "mathematics is not only technical" — "the point" upon which his article is a masterful elaboration.
My intention is not to conceal my identity - this is just the substack account I happened to have when I started reading your blog. In fact I thought you had figured out who I was when I commented previously, but I would be happy to clarify if necessary.
I am not really a part of the formalization community - I have just enjoyed following some of the discussion about it. Certainly anything wrong with my comment shouldn't be blamed on them (or on the tech industry).
If an engineer tells you they have concerns about the safety of a bridge, and their response to this is to build a new bridge, would your reaction be to point out that since the new bridge is not the same as the old bridge building the new one will do nothing to help with concerns about the old? Or is the reason that the engineer finds their concerns about the old bridge concerning because they would like there to exist a safe bridge for people to cross?
I've read Colin McLarty's article before, and I just read it again. It seems clear to me that he is not concerned with Wiles' proof as an immovable object but instead with whether it can be modified to fit within a specific weak formal system. It's unambiguous that this is at least one concern discussed in the article - whether a proof of Fermat, not necessarily Wiles's, exists in some weak system like PA or a weaker one.
Your metaphor of a fall from grace would be apt if at some previous point we had access to metaphysical certainty about mathematical proofs, which we have given up to obtain formalized proofs instead. But no such thing has ever existed - there's only been fallible human beings trying their best to concentrate at they stare at a page, a blackboard, or at each other.
Saying that mathematics is not only technical suggests by omission that mathematics is technical in part. It seems to me that technical improvements to the technical part of mathematics may be of some value, even, symbiotically, to the non-technical aspects of mathematics.
As I wrote, everyone has their reasons. I try to respond to them one at a time. When I address those concerned with metaphysical certainty I am accused of not addressing someone else's reasons. You may think the search for metaphysical certainty is a fool's errand, and I may agree with you, but there are others who take it very seriously. Many of them have been quoted in this newsletter. You can are find direct quotations from Kevin that strongly suggest that such concerns motivated his initial interest in proof verification. His grant proposal stresses different motivations, among them the hope that, as Margaret Wertheim so felicitously put it, "if mathematicians Lean in, understanding will follow."
Your logic of responding to reasons one at a time makes total sense. I just want to encourage you to consider more carefully alternate interpretations of someone's words when you believe that they are expressing reasons for which this particular argument is an apt reply.
Let me point out that I have read most of the posts of this blog, and noticed several times where you reference the difficulty of proving two proofs are equivalent. This difficulty is only relevant if someone is (1) interested in metaphysical certainty, and not practical certainty, (2) interested in certainty that a proof is correct, and not certainty that a theorem is correct, (3) cares about a specific proof, and isn't willing to switch to a new proof. I can't remember a single time you brought this up that I was convinced that the person satisfied (1), (2), (3).
In particular I remember Kevin being very concerned about the number of papers in the literature that contain serious errors, and the difficulty in sorting out which parts are dependent on the error and which aren't - this is a practical concern that formalization would probably help with and not one about metaphysical certainty.
Here is the sort of thing I have in mind, from https://siliconreckoner.substack.com/p/can-mathematics-be-done-by-machine:
"On pp. 326-327 (of Mechanizing Proof), Donald MacKenzie quotes a computer scientist who argued that mathematicians' failure to perform proofs formally, "by manipulating uninterpreted formulae accordingly [sic] to explicitly stated rules" proves that "mathematics today is still a discipline with a sizeable pre-scientific component, in which the spirit of the Middle Ages is allowed to linger on" [Dijkstra 1988], a philosopher (Peter Nidditch) who claimed that "in the whole literature of mathematics there is not a single valid proof in the logical sense," and another philosopher who doubts "that mathematics is an essentially human activity" [Teller 1980]. "
For obvious reasons I won't try to PROVE that Kevin's concerns are identical with those of the philosophers and computer scientists quoted here. See also MacKenzie, "Computing and the cultures of proving," Phil. Trans. R. Soc. A. (2005).
But none of these satisfy (3) - they display no attachment to a particular informal proof that they hope to rescue by formalization. If mathematicians simply stopped publishing informal proofs and wrote only formal ones (which would horrify me about 70% as much as it would horrify you), the computer scientist whose definition of the Middle Ages extends into the early 20th century would clearly be satisfied that mathematics is not still a discipline with a sizeable pre-scientific component, even if nothing is done about the past proofs. Similarly publishing a single formal proof would theoretically satisfy Peter Nidditch (although this is a bit strange as the mathematics literature clearly contains formal proofs, e.g. as examples in logic textbooks or in that one journal that only publishes formal proofs in Mizar).
I am probably taking this further than you intended, but there is a curious "quasi-borderline" example in "The Tempest", Act 5, Scene 1:
Their understanding
Begins to swell, and the approaching tide
Will shortly fill the reasonable shore
That now lies foul and muddy.
While this is being said, Alonso and the court party are still "under the influence of charm" and "bereft of senses", so, arguably, not fully "animate".
Here is an example combining "Lean" and "understand" (from "Two Gentlemen of Verona", Act 2, Scene 5):
LAUNCE
Ay, and what I do too: look thee, I'll but lean,
and my staff understands me.
SPEED
It stands under thee, indeed.
LAUNCE
Why, stand-under and under-stand is all one.
Ernie Davis picked up this one too...
Twelfth Night, Act 3, Scene 1:
"My legs do better understand me, sir, than I understand what you mean by bidding me taste my legs."
Ernie Davis also found this one… but it's a play on words ("understand/stand under") so he didn't think it counts.
And here is an example from Macbeth (Act 3, Scene 2) of a "verse attributing `agency' to an inanimate object" (which is incidentally the origin of the expression "invisible hand"):
Come, seeling night,
Scarf up the tender eye of pitiful day
And with thy bloody and invisible hand
Cancel and tear to pieces that great bond
Which keeps me pale.
All right, but I was specifically looking for an example with the word "understanding."
Hamlet Act 1, Scene 1:
"This spirit, dumb to us, will speak to him."
is an example of a "verse attributing 'understanding' to an inanimate object".
Yes, it is not easy to characterize what is going on here. There are semantic shifts in language and thought that take place without much regard for pattern in time and place. How are LLM's to capture these? For example, what would it make of the various uses of the word 'diagram' in mathematics? How would it avoid errors of the sort it made when you queried it? Buzzard appears to be promoting LEAN as an 'assistant' ... that seems quite plausible and maybe even useful. We don't seem to have found a good role for LLM's just yet...maybe when Birnam Wood comes to Dunsinane?
If you are suggesting that LLMs will find their proper role in time to avert further massacres, or on the contrary to initiate a new series of massacres, I would not disagree.
In the meantime, I hope to address this specific question in the continuation of the previous post.
the Macbeth line appears to have been misunderstood both by GPT and the author of the post. By 'sensible' to sight and feeling Macbeth means 'able to be sensed by' feeling and sight ...in the old philosophical jargon, these are examples of 'sensibilia' ...the different senses were said to have different things they could sense...their sensibilia (Aristotle discusses this generally in Books II and III of de Anima and specifically in de Sensu). Macbeth does not attribute feeling, sight or understanding to the dagger. Somewhere in the 17th c the notions of 'object(ive)' and 'subject(ive)' were inverted. Today 'sensible' refers to the person sensing, not the thing sensed.
Thank you. The author didn't take the time to check (and has no excuse). Ernie Davis made the same point, but without the etymological history; I've acknowledged this in a new footnote.
If ChatGPT is capable of misunderstanding then presumably it's also capable of understanding. Probably a word other than "misunderstanding" better captures what did or didn't happen.