I'm quite inclined to agree with the arguments in the mode, but the grading of mathematics into other disciplines poses a problem for me in general. consider a case where the only thing I care about is the formal correctness of a proposition. suppose I have a computer network architecture that is somehow robust iff a certain theorem holds of graphs, or a spaceship transmission that works iff NS always has smooth solutions. what I most care about is whether the network stays online, whether the ship flies. what's "under the hood" of the proof is strictly an academic matter.
would you say that these questions are not then properly considered "mathematical"? why fails a spectrum between "mathematically valuable" and "formally valuable" questions? Poincaré made formal errors that were nonetheless mathematically valuable; couldn't we also make formally correct claims—indeed, *useful* formally correct claims—that are epistemically vacuous?
any thoughts or corrections to my thinking are more than welcome!
1) A formal proof is both a mathematical object, and a physical object (for example living in the memory of my computer when I run a proof assistant). To relate this to an example from another comment, there is clearly a much better correspondence here than between an euclidean rectangle and a physical rectangle: physical object and mathematical object are actually the same in this case!
2) The Central Dogma is actually a Central Thesis, similar to the Church-Turing thesis: Every rigorous mathematical proof is formalisable. It is a valuable contribution of this blog and this post to clearly express this thesis.
I am very much a die-hard Platonist, because I think only Platonism is consistent with both 1) and 2). And of course I think that the existence of a mathematical proof is the ultimate arbiter, not the existence of a formal proof: If I have a mathematical argument that I believe to be correct, then turning it into a formal proof helps me because now I have turned the mathematical argument into a mathematical object. But the "correctness" of this mathematical object of course also relies on an underlying mathematical argument, that explicitly spells out what "correctness of this mathematical object" means.
But a formal proof is also a mathematical proof. I would say this is the real "Standard View". I don't think it is disqualified to count as such just because it may be too big for me to understand: There are many mathematical proofs I don't understand, because I don't have (or am willing to make) the time to understand them.
"Formalisable" itself is also a notion that evolves, as pointed out in this post. I don't think any serious practitioner of formal proof would deny that. Theorem provers such as Isabelle or Lean have been developed because they represent better notions of "formalisable" than for example first-order logic or second-order logic. I am developing abstraction logic (http://abstractionlogic.com), because I think it provides a better notion of "formalisable" than first-order logic, second-order logic, or dependent type theory.
A machine is not a device for restricting freedom. A washing machine actually expands my freedom, at least if I cannot delegate the task of doing my dirty laundry to somebody else. But of course we must make sure that washing machines are just that, and not, for example, an appliance for surveillance.
So the question is not if formal proof will become essential to mathematics, or if it should become essential to mathematics. Of course it will be, and of course it should be. It IS mathematics, after all! The real question is how we can ensure we stay free as creative human beings as this process unfolds.
Re the idea that logical formalisms are in the end the servants of mathematical truth rather than its masters, and that to the extent we figure out correct things that our logical formalisms don't apply to, that's a problem for the formalisms, not for the mathematics:
I think a nice test case is notions of complexity. Here the actual notion we're interested in is not "correctness" but "hardness." And we have this nice well-worked out theory of hardness (P, NP, #P, etc etc etc ) that descends from Turing machines. But then over time we realize that lots of problems that are hard in this sense, we routinely solve anyway, like traveling salesman! i.e. if in practice we get solutions we think of as "with very high probability very close to optimal" we are fine. And actually working out a formalism that well-captures this notion of "hardness" is I think an ongoing project in CS theory where there's no consensus answer yet! But it very much fits your narrative — we are out here actually doing math, and the formalism tries to keep up and remain sufficiently descriptive/supportive of the practice.
AI of the 1970s and 1980s (my MPhil therein was 1984) thought it was making progress on both formalizing (logic programming, "neat AI") and simulating informal (Schank/Minsky's scripts and frames, "scruffy AI") human thought processes. We were wrong. Human thought is way more subtle, flexible, powerful, and amazing than any of us (even we in the "scruffy AI" camp) gave it credit for.
Hilariously, just replace "mathematician" with "human" in this article, and you would have a beautiful critique of why we failed. Logical correctness is neither necessary nor sufficient for explaining how human thought works. (Well, this only applies directly to the logic programming types, but we scruffy types still thought we were writing "rules" that could be used as is, with breakout to underlying reasoning when needed.)
Whatever, lovely essay that's exactly right: formalizing is an after-the-fact thing used once you've had an idea and figured out where that idea fits in the universe of mathematics (or human experience).
I would say that a formal proof is an idealization of an informal proof in sort of the same way that a Euclidean rectangle is an idealization of a flat rectangular physical object. (The analogy is obvious imperfect.) Only a pretty die-hard Platonist would claim that the rectangular object is fundamentally a flawed replica of the geometric ideal, or would object to the claim corresponding to the one in the paper about why informal proofs are formally correct that "Rectangular objects have many of the same properties as Euclidean rectangles because geometricians have developed a rich and successful geometric theory intended to capture many of the spatial characteristics of physical objects."
Hi Ernest, thanks for the thoughtful comments and questions! I like this analogy, and part of my goal with this post (and with the article itself) can be phrased as an effort to broaden it. Let's grant that formal proof is something like Euclidean geometry, and that mathematical proofs to date are (to the best of my knowledge) like physical rectilinear objects in flat space (i.e. the type of things Euclidean geometry is built to idealize). One of the purposes of the post and the paper is to argue that if we encountered valid mathematical proofs that aren't well captured by any known formal system, then, just as when we encountered geometric objects in curved space that couldn't be described by Euclidean geometry, the answer wouldn't be to reject the proofs but rather to create/discover new formal systems capable of accommodating the new mathematics.
We treat this directly in the final paragraph of Section 6 of the article:
"We conclude this section with a final argument, which is somewhat speculative but which seems to us to accurately reflect both the sociology of mathematics and the relationship between logic and mathematics. Perhaps it is a Rorschach test of sorts. Suppose that there were a result that could not be formalized in any known logical system, but which nonetheless the mathematical community came to accept as mathematically correct. This may seem implausible—though we would argue the reason it seems implausible is that mathematical logic is a mature discipline, and there are many systems available already. But suppose it happens. What should we make of that situation? Advocates of the Standard View would presumably say that the mathematical community has gone off the rails, they have accepted an incorrect result, where incorrectness is determined by failures of formalizability. . . But that is not what we would expect mathematicians or logicians to actually do. Instead, we think such a situation would spark a lot of excitement among logicians, and important new work trying to find a new formal system in which the result could be formalized. One would try to understand how the result works and why it might be taken to be correct. In other words, if existing mathematical theories of mathematical practice failed in some domain, the correct and likely response would be to develop new mathematical theories of that domain."
This suggests a different relationship between formal proof and mathematical proof than I've often encountered in the literature around the standard view and mechanization/AI, and I'd be very happy if our post and piece help bring this different relationship into clearer focus.
It seem to me that formalization in the sense of expression in mathematical logic is a red herring in this argument. Every argument that Weatherall and Wolfson bring against the importance of formalized proof applies equally to rigorous proof. The proofs by Poincare' and Lefschetz that they mention were not merely unformalized; they were also unrigorous and sometimes flawed. Rigorous proof has been an ideal of mathematical practice at least since Weierstrass. Are Weatherall and Wolfson prepared to throw out the baby of rigorous proof with the bathwater of formalization? [Some philosophers of mathematics are.] If so, they should say so. If not, then they have to present an argument why rigorous proof is critical but formalization is unnecessary.
I doubt that most enthusiasts verification would subscribe to the supposed "Standard View" that informal proofs "should be seen as describing or encoding a formal proof", or would deny that "informal proofs are formally correct because logicians have developed a rich and successful mathematical theory of mathematical practice intended to capture various aspects of mathematical argument." Rather I, at least, would word the Central Dogma as "Any rigorous mathematical proof can be converted into a formal proof, if sufficient effort is invested." I'm not aware of any well-established counterexamples. The corresponding statement about informal proofs would be "Any sufficiently convincing informal proof can, with sufficient effort, be converted into a rigorous proof", but my impression is that that isn't true.
I'm replying here to your second paragraph; I'll reply to the point you raise in the first below (in response to David's thoughtful elaboration involving Euler and Weierstrass). A core goal of the post and the article is take issue with the claim that "Any rigorous mathematical proof can be converted into a formal proof, if sufficient effort is invested." As a specific claim about existing formal systems, I'm also not aware of any counterexamples, but I want to explicitly hold out for the possibility that new mathematics in the future may go beyond what existing formal systems can handle, and that if this were to occur, that would be a challenge for formal systems, not a problem for mathematics (cf. my response above). I expect that if this occurred, new formal systems could likely be built to accommodate the new mathematics, but this would change the definition of "formal proof" in such a way as to render the standard view either false or vacuous. In support of this possibility (and borrowing from the paper), note that similar phenomena have repeatedly occurred in the relationship between mathematics and physics, where for example, once the utility to physics of the Dirac delta function was amply demonstrated, the initial lack of a rigorous mathematical treatment was a challenge for mathematics, not for physics. Similar comments apply to the path integral formalism, where finding an adequate mathematical theory is an ongoing mathematical challenge, but not one for physics per se.
- Jesse
ps. My comments of course represent joint work and ideas with Jim. I'm speaking in the first person so that any errors or muddleheadedness are clearly due to me, and not to Jim :)
In his 2005 article "Computing and the cultures of proving," the sociologist Donald MacKenzie specifically distinguishes "formal proofs" from "rigorous arguments," as follows:
"A formal proof is a finite sequence of ‘well-formed’ (that is, to put it loosely, syntactically correct) formulae leading to the theorem,…" (the sentence continues by specifying the rules that guarantee that the sequence is legitimate in the given theory);
"Rigorous arguments, in contrast, are those arguments that are accepted by
mathematicians (or other relevant specialists) as constituting mathematical
proofs, but that are not formal proofs in the above sense."
In other words, what MacKenzie calls a rigorous argument seems to be what you are calling an informal proof. He is presumably drawing on his authority as sociologist; is this a judgment based on an empirical study of how the expression is used?
MacKenzie's definition of "formal proof," which is the accepted one among mathematicians and logicians, makes it clear that a formal proof is an object in a mathematical theory. There is no universally accepted independent definition of "rigorous argument," which is why MacKenzie and Ernie Davis can use the expression in such different ways. This leads me to a question that is long overdue: this newsletter has (for four years) repeatedly used the word "mechanization" without ever specifying what that means. What is a machine? In view of the distinction between formal and informal (or rigorous) proofs, I offer a definition:
A *machine* is a device for eliminating ambiguity.
This can be reinterpreted:
A *machine* is a device for eliminating freedom.
The Lean programming language is a machine in this sense, as is Bourbaki's Éléments de mathématique. The catch, of course, is that ambiguity (and a fortiori freedom) can never be entirely eliminated. Someone could reprogram Lean so that any sequence of formulas containing the word "elephant" would automatically be considered valid. There are good reasons for relinquishing the freedom to do that, or to change the meaning of (for example) "equivalence relation" in the middle of a sentence. But now all of a sudden the conversation about rigor becomes a conversation about human freedom, which is what it should have been all along.
(I'll be expanding this comment in a future post. In the meantime, I invite readers to list some of the philosophers who have made similar points more effectively.)
I wanted to raise a similar, but I think slightly different, question. When I think about these issues I do keep coming back to the various infinite sums evaluated by Euler, which we now agree were put on a solid footing by Weierstrass.
Are Euler's arguments formally correct in the sense of the article? I think surely not at the time (not that it would have made sense to ask this question at the time), but maybe they are formally correct now (because the missing ingredients are second nature to those doing the formalizing). Do Euler's arguments have epistemic value? Self-evidently yes. Are Euler's arguments mathematically correct in the sense of the article? I think this is up for debate. (Do we differentiate the correctness of an argument written by someone who didn't know about uniform convergence from the identical argument written by someone who didn't bother to explain convergence issues they were well aware of, and viewed as trivial?)
Anyway: we regard the contributions of Weierstrass as fundamental not just because they put existing arguments on a firmer footing, but because more rigor leads both to new ideas (easier to prove something when you know what the right statement is...) and also fewer mathematical errors. It seems to me that the story here involves the long arc of mathematics bending simultaneously towards both formal correctness and towards mathematical correctness, in some interrelated way. In the thought experiment where 20 years from now machines have combed the literature, formalized the correct papers and identified the fundamentally flawed ones, and trimmed back the trees of the mathematical literature to just what has actually been proved, I think I would still place the higher value on mathematical correctness but it would be hard to fully reject formal correctness as a value.
Thanks for posting this, and for anchoring your question on such rich examples. This also touches on what I hear in Ernest's first paragraph in his comment above. A reasonable view (which Jim articulates nicely) is that rigor is always a backward looking notion, one that's up for grabs in the sense that the community regularly argues about it (at the level of seminars, referee reports, questions on preprints, etc.), and which is often theorized via formalization efforts. Surely, Cauchy, Dirichlet, Castelnuovo, etc. thought their arguments *were* rigorous and it was only later that problems were found and Weierstrass and others tried to come up with new methods. On the other hand, many of e.g. Cauchy's results turned out to be correct, and once we understood things like continuity better, mathematicians could clearly see which ones worked and which didn't. Note however that this clarification didn't take place through some rote process, but rather through mathematicians more deeply understanding the core phenomena and developing new methods, including but not solely formal ones, that could help avoid those errors.
I share your sense that if new methods, technology, etc. allow us to more quickly, effectively improve the reliability of the literature without sacrificing core things we value, then surely we'll want and use these new tools, not least because doing so will likely lead to new ideas as well. At the same time, a lot of the discourse around AI and formalization has been much more marked by fear-mongering and much less measured than the view you articulate, and part of my goal with this post and the article is to push back against that discourse and help move it to a better place.
extremely fun read.
I'm quite inclined to agree with the arguments in the mode, but the grading of mathematics into other disciplines poses a problem for me in general. consider a case where the only thing I care about is the formal correctness of a proposition. suppose I have a computer network architecture that is somehow robust iff a certain theorem holds of graphs, or a spaceship transmission that works iff NS always has smooth solutions. what I most care about is whether the network stays online, whether the ship flies. what's "under the hood" of the proof is strictly an academic matter.
would you say that these questions are not then properly considered "mathematical"? why fails a spectrum between "mathematically valuable" and "formally valuable" questions? Poincaré made formal errors that were nonetheless mathematically valuable; couldn't we also make formally correct claims—indeed, *useful* formally correct claims—that are epistemically vacuous?
any thoughts or corrections to my thinking are more than welcome!
1) A formal proof is both a mathematical object, and a physical object (for example living in the memory of my computer when I run a proof assistant). To relate this to an example from another comment, there is clearly a much better correspondence here than between an euclidean rectangle and a physical rectangle: physical object and mathematical object are actually the same in this case!
2) The Central Dogma is actually a Central Thesis, similar to the Church-Turing thesis: Every rigorous mathematical proof is formalisable. It is a valuable contribution of this blog and this post to clearly express this thesis.
I am very much a die-hard Platonist, because I think only Platonism is consistent with both 1) and 2). And of course I think that the existence of a mathematical proof is the ultimate arbiter, not the existence of a formal proof: If I have a mathematical argument that I believe to be correct, then turning it into a formal proof helps me because now I have turned the mathematical argument into a mathematical object. But the "correctness" of this mathematical object of course also relies on an underlying mathematical argument, that explicitly spells out what "correctness of this mathematical object" means.
But a formal proof is also a mathematical proof. I would say this is the real "Standard View". I don't think it is disqualified to count as such just because it may be too big for me to understand: There are many mathematical proofs I don't understand, because I don't have (or am willing to make) the time to understand them.
"Formalisable" itself is also a notion that evolves, as pointed out in this post. I don't think any serious practitioner of formal proof would deny that. Theorem provers such as Isabelle or Lean have been developed because they represent better notions of "formalisable" than for example first-order logic or second-order logic. I am developing abstraction logic (http://abstractionlogic.com), because I think it provides a better notion of "formalisable" than first-order logic, second-order logic, or dependent type theory.
A machine is not a device for restricting freedom. A washing machine actually expands my freedom, at least if I cannot delegate the task of doing my dirty laundry to somebody else. But of course we must make sure that washing machines are just that, and not, for example, an appliance for surveillance.
So the question is not if formal proof will become essential to mathematics, or if it should become essential to mathematics. Of course it will be, and of course it should be. It IS mathematics, after all! The real question is how we can ensure we stay free as creative human beings as this process unfolds.
Re the idea that logical formalisms are in the end the servants of mathematical truth rather than its masters, and that to the extent we figure out correct things that our logical formalisms don't apply to, that's a problem for the formalisms, not for the mathematics:
I think a nice test case is notions of complexity. Here the actual notion we're interested in is not "correctness" but "hardness." And we have this nice well-worked out theory of hardness (P, NP, #P, etc etc etc ) that descends from Turing machines. But then over time we realize that lots of problems that are hard in this sense, we routinely solve anyway, like traveling salesman! i.e. if in practice we get solutions we think of as "with very high probability very close to optimal" we are fine. And actually working out a formalism that well-captures this notion of "hardness" is I think an ongoing project in CS theory where there's no consensus answer yet! But it very much fits your narrative — we are out here actually doing math, and the formalism tries to keep up and remain sufficiently descriptive/supportive of the practice.
'The Impending Crisis in Mathematics: The Holy Grail of Mathematics Is Arithmetical Truth, Not Set-Theoretical Proof'.
Essay: https://medium.com/@bhup.anand/the-holy-grail-of-mathematics-is-arithmetical-truth-not-set-theoretical-proof-d8674e209952
Preprint: https://www.dropbox.com/scl/fi/uk8nscl18s5y034hwin1k/
AI of the 1970s and 1980s (my MPhil therein was 1984) thought it was making progress on both formalizing (logic programming, "neat AI") and simulating informal (Schank/Minsky's scripts and frames, "scruffy AI") human thought processes. We were wrong. Human thought is way more subtle, flexible, powerful, and amazing than any of us (even we in the "scruffy AI" camp) gave it credit for.
Hilariously, just replace "mathematician" with "human" in this article, and you would have a beautiful critique of why we failed. Logical correctness is neither necessary nor sufficient for explaining how human thought works. (Well, this only applies directly to the logic programming types, but we scruffy types still thought we were writing "rules" that could be used as is, with breakout to underlying reasoning when needed.)
Whatever, lovely essay that's exactly right: formalizing is an after-the-fact thing used once you've had an idea and figured out where that idea fits in the universe of mathematics (or human experience).
I would say that a formal proof is an idealization of an informal proof in sort of the same way that a Euclidean rectangle is an idealization of a flat rectangular physical object. (The analogy is obvious imperfect.) Only a pretty die-hard Platonist would claim that the rectangular object is fundamentally a flawed replica of the geometric ideal, or would object to the claim corresponding to the one in the paper about why informal proofs are formally correct that "Rectangular objects have many of the same properties as Euclidean rectangles because geometricians have developed a rich and successful geometric theory intended to capture many of the spatial characteristics of physical objects."
Hi Ernest, thanks for the thoughtful comments and questions! I like this analogy, and part of my goal with this post (and with the article itself) can be phrased as an effort to broaden it. Let's grant that formal proof is something like Euclidean geometry, and that mathematical proofs to date are (to the best of my knowledge) like physical rectilinear objects in flat space (i.e. the type of things Euclidean geometry is built to idealize). One of the purposes of the post and the paper is to argue that if we encountered valid mathematical proofs that aren't well captured by any known formal system, then, just as when we encountered geometric objects in curved space that couldn't be described by Euclidean geometry, the answer wouldn't be to reject the proofs but rather to create/discover new formal systems capable of accommodating the new mathematics.
We treat this directly in the final paragraph of Section 6 of the article:
"We conclude this section with a final argument, which is somewhat speculative but which seems to us to accurately reflect both the sociology of mathematics and the relationship between logic and mathematics. Perhaps it is a Rorschach test of sorts. Suppose that there were a result that could not be formalized in any known logical system, but which nonetheless the mathematical community came to accept as mathematically correct. This may seem implausible—though we would argue the reason it seems implausible is that mathematical logic is a mature discipline, and there are many systems available already. But suppose it happens. What should we make of that situation? Advocates of the Standard View would presumably say that the mathematical community has gone off the rails, they have accepted an incorrect result, where incorrectness is determined by failures of formalizability. . . But that is not what we would expect mathematicians or logicians to actually do. Instead, we think such a situation would spark a lot of excitement among logicians, and important new work trying to find a new formal system in which the result could be formalized. One would try to understand how the result works and why it might be taken to be correct. In other words, if existing mathematical theories of mathematical practice failed in some domain, the correct and likely response would be to develop new mathematical theories of that domain."
This suggests a different relationship between formal proof and mathematical proof than I've often encountered in the literature around the standard view and mechanization/AI, and I'd be very happy if our post and piece help bring this different relationship into clearer focus.
It seem to me that formalization in the sense of expression in mathematical logic is a red herring in this argument. Every argument that Weatherall and Wolfson bring against the importance of formalized proof applies equally to rigorous proof. The proofs by Poincare' and Lefschetz that they mention were not merely unformalized; they were also unrigorous and sometimes flawed. Rigorous proof has been an ideal of mathematical practice at least since Weierstrass. Are Weatherall and Wolfson prepared to throw out the baby of rigorous proof with the bathwater of formalization? [Some philosophers of mathematics are.] If so, they should say so. If not, then they have to present an argument why rigorous proof is critical but formalization is unnecessary.
I doubt that most enthusiasts verification would subscribe to the supposed "Standard View" that informal proofs "should be seen as describing or encoding a formal proof", or would deny that "informal proofs are formally correct because logicians have developed a rich and successful mathematical theory of mathematical practice intended to capture various aspects of mathematical argument." Rather I, at least, would word the Central Dogma as "Any rigorous mathematical proof can be converted into a formal proof, if sufficient effort is invested." I'm not aware of any well-established counterexamples. The corresponding statement about informal proofs would be "Any sufficiently convincing informal proof can, with sufficient effort, be converted into a rigorous proof", but my impression is that that isn't true.
Hi Ernest,
I'm replying here to your second paragraph; I'll reply to the point you raise in the first below (in response to David's thoughtful elaboration involving Euler and Weierstrass). A core goal of the post and the article is take issue with the claim that "Any rigorous mathematical proof can be converted into a formal proof, if sufficient effort is invested." As a specific claim about existing formal systems, I'm also not aware of any counterexamples, but I want to explicitly hold out for the possibility that new mathematics in the future may go beyond what existing formal systems can handle, and that if this were to occur, that would be a challenge for formal systems, not a problem for mathematics (cf. my response above). I expect that if this occurred, new formal systems could likely be built to accommodate the new mathematics, but this would change the definition of "formal proof" in such a way as to render the standard view either false or vacuous. In support of this possibility (and borrowing from the paper), note that similar phenomena have repeatedly occurred in the relationship between mathematics and physics, where for example, once the utility to physics of the Dirac delta function was amply demonstrated, the initial lack of a rigorous mathematical treatment was a challenge for mathematics, not for physics. Similar comments apply to the path integral formalism, where finding an adequate mathematical theory is an ongoing mathematical challenge, but not one for physics per se.
- Jesse
ps. My comments of course represent joint work and ideas with Jim. I'm speaking in the first person so that any errors or muddleheadedness are clearly due to me, and not to Jim :)
In his 2005 article "Computing and the cultures of proving," the sociologist Donald MacKenzie specifically distinguishes "formal proofs" from "rigorous arguments," as follows:
"A formal proof is a finite sequence of ‘well-formed’ (that is, to put it loosely, syntactically correct) formulae leading to the theorem,…" (the sentence continues by specifying the rules that guarantee that the sequence is legitimate in the given theory);
"Rigorous arguments, in contrast, are those arguments that are accepted by
mathematicians (or other relevant specialists) as constituting mathematical
proofs, but that are not formal proofs in the above sense."
In other words, what MacKenzie calls a rigorous argument seems to be what you are calling an informal proof. He is presumably drawing on his authority as sociologist; is this a judgment based on an empirical study of how the expression is used?
MacKenzie's definition of "formal proof," which is the accepted one among mathematicians and logicians, makes it clear that a formal proof is an object in a mathematical theory. There is no universally accepted independent definition of "rigorous argument," which is why MacKenzie and Ernie Davis can use the expression in such different ways. This leads me to a question that is long overdue: this newsletter has (for four years) repeatedly used the word "mechanization" without ever specifying what that means. What is a machine? In view of the distinction between formal and informal (or rigorous) proofs, I offer a definition:
A *machine* is a device for eliminating ambiguity.
This can be reinterpreted:
A *machine* is a device for eliminating freedom.
The Lean programming language is a machine in this sense, as is Bourbaki's Éléments de mathématique. The catch, of course, is that ambiguity (and a fortiori freedom) can never be entirely eliminated. Someone could reprogram Lean so that any sequence of formulas containing the word "elephant" would automatically be considered valid. There are good reasons for relinquishing the freedom to do that, or to change the meaning of (for example) "equivalence relation" in the middle of a sentence. But now all of a sudden the conversation about rigor becomes a conversation about human freedom, which is what it should have been all along.
(I'll be expanding this comment in a future post. In the meantime, I invite readers to list some of the philosophers who have made similar points more effectively.)
I wanted to raise a similar, but I think slightly different, question. When I think about these issues I do keep coming back to the various infinite sums evaluated by Euler, which we now agree were put on a solid footing by Weierstrass.
Are Euler's arguments formally correct in the sense of the article? I think surely not at the time (not that it would have made sense to ask this question at the time), but maybe they are formally correct now (because the missing ingredients are second nature to those doing the formalizing). Do Euler's arguments have epistemic value? Self-evidently yes. Are Euler's arguments mathematically correct in the sense of the article? I think this is up for debate. (Do we differentiate the correctness of an argument written by someone who didn't know about uniform convergence from the identical argument written by someone who didn't bother to explain convergence issues they were well aware of, and viewed as trivial?)
Anyway: we regard the contributions of Weierstrass as fundamental not just because they put existing arguments on a firmer footing, but because more rigor leads both to new ideas (easier to prove something when you know what the right statement is...) and also fewer mathematical errors. It seems to me that the story here involves the long arc of mathematics bending simultaneously towards both formal correctness and towards mathematical correctness, in some interrelated way. In the thought experiment where 20 years from now machines have combed the literature, formalized the correct papers and identified the fundamentally flawed ones, and trimmed back the trees of the mathematical literature to just what has actually been proved, I think I would still place the higher value on mathematical correctness but it would be hard to fully reject formal correctness as a value.
Hi David,
Thanks for posting this, and for anchoring your question on such rich examples. This also touches on what I hear in Ernest's first paragraph in his comment above. A reasonable view (which Jim articulates nicely) is that rigor is always a backward looking notion, one that's up for grabs in the sense that the community regularly argues about it (at the level of seminars, referee reports, questions on preprints, etc.), and which is often theorized via formalization efforts. Surely, Cauchy, Dirichlet, Castelnuovo, etc. thought their arguments *were* rigorous and it was only later that problems were found and Weierstrass and others tried to come up with new methods. On the other hand, many of e.g. Cauchy's results turned out to be correct, and once we understood things like continuity better, mathematicians could clearly see which ones worked and which didn't. Note however that this clarification didn't take place through some rote process, but rather through mathematicians more deeply understanding the core phenomena and developing new methods, including but not solely formal ones, that could help avoid those errors.
I share your sense that if new methods, technology, etc. allow us to more quickly, effectively improve the reliability of the literature without sacrificing core things we value, then surely we'll want and use these new tools, not least because doing so will likely lead to new ideas as well. At the same time, a lot of the discourse around AI and formalization has been much more marked by fear-mongering and much less measured than the view you articulate, and part of my goal with this post and the article is to push back against that discourse and help move it to a better place.
- Jesse