Here's perhaps a more borderline example along the line of the one you discuss: did Peter Scholze waste the time of the whole team of people (and his own, in following the process throughout) for 6 months when they formalised the proof of his result with Clausen about liquid vector spaces? (Another variable, which complicates matters is that a number of them were early career researchers, and might well have spent that time on traditional mathematical pursuits, to not set their careers a-wobbling, in comparison to Hales, who wouldn't need to worry; so the timescale is perhaps appropriately relative, here.)
In the process, understanding of the proof—not to mention a simplification—*was* gained. I'm curious to know your take.
Thank you for this question. Maybe you will find this answer facile, but I can't think of a better one: only the participants in the project can say whether they wasted their time. I guess none of them will. Commelin, who led the team, reported on the project at the Fields Medal Symposium and made it clear that he found the process rewarding in many ways — not only because it provided an opportunity for him to understand and to simplify the proof.
As for the others, insofar as their satisfaction is in part due to their impression, amplified by the media, that they were participating in a project of historic significance, only time will tell whether this impression is justified.
But let me also try to give my opinion of the role formal proofs play in mathematical practice (some ideas here resemble/are influenced by Kenny Easwaran's work in philosophy of math...but it's not quite the same so if you are interested read his paper).
The short version is that what makes us believe that we understand a proof (ie understand it well enough to say it's correct) is that we think we could fill in the missing details given enough time and interest. And in some sense a fully formal proof represents the limit of filling in the details.
But this isn't saying that it's always better to be more formal. If I understand a proof I can be very confident I could fill in all the missing details given enough time. If it's just a bunch of calculations or other overly formal crap I won't be so confident. Yes, sometimes when I get myself sufficiently confused about some quantified statement I do drop back almost the the level of formal proof for long enough to convince me I know what I'm doing but if the proof was presented at that fine grained level of detail I could never (w/o a computer) keep enough of it in mind to actually be confident it was correct (so not confident I could fill in 'gaps').
Ofc, that's just a theory about what makes a proof convincing. If doesn't address other concerns like understanding, ability to use/modify the proof to prove other results etc.. which also matter for mathematics.
So I feel like it might help to be precise about what is being claimed here. Specifically, there is the cultural practice of mathematics and the project of increasing our knowledge (both in terms of new theorems and increasing our confidence in old ones) of mathematical claims. It is primarily the second (inc confidence) that machine checked proofs are relevant to.
For instance, are you really calling into doubt the claim that a fully formal, computer verified (say by multiple independent checkers using a very simple proof system like FOL natural deduction/sequent calc) gives us a particularly high level of confidence there are no gaps in the proof? At the very least that the fully formal fol statement of the theorem is proved?
Given my own experience writing and reviewing math papers that increase in certainty seems quite attractive and significant.
And don't be so sure companies don't care about it. If I'm marketing a new encryption product a form proof that it's secure under such and such computational assumptions *especially* if it's machine checked seems incredibly valuable to my sales. Being able to produce formal proofs that safety critical software systems have certain properties is also very valuable. And the ability to produce a fully formal machine checked proof is potentially valuable to compiler designers.
I fully agree with the point you make in your last paragraph, and I have made it repeatedly in this newsletter, often in conjunction with references to Donald MacKenzie's book "Mechanizing Proof." See for example the reference to MacKenzie's book at this early post: https://siliconreckoner.substack.com/p/on-the-implications-of-scholzes-liquid
Although I haven't spelled out the implication explicitly, I also believe that familiarity with this very important function of formal proof verification in software development has convinced many computer scientists that formalization is just as central in mathematics.
With regard to your second paragraph, the first question is whether "confidence" is what is primarily being sought, the second question is what use might be made of the fully formal statement of the theorem. I began by pointing out that most of the mathematical professions represented at the JMM are not terribly concerned with proof. The conception of mathematics as bound up with proofs in formal systems is a relatively recent development in the history of mathematics, although it certainly has ancient antecedents. It is not valid to claim that it expresses the primary virtue of mathematics; the references in footnote 6 point to very different pictures of mathematics, including some in which formalism is quite opposed to what at the time was considered valuable in mathematics.
I agree they aren't that concerned with proof per se. However, I think that outside of the realm of computer assistance the ability to be able to produce a proof of any desired degree of formality (eg someone doubts step 5 you could give more and more details and , if necessary, give a fully formal version with enough time) turns out to be our best evidence/test of mathematical understanding.
Math is an area it's easy to get confused in and the role of increasing formalization is to provide a way to check that we (or they) aren't confused.
Now you might worry that you might occasionally get someone with great understanding who isn't good at formalization (Ramanujan) but I'd argue that relative to the difficulty of math the cost to learn to offer more details (enough to convince someone formalization could be possible) is relatively small it's just B4 modern era we didn't always insist on this common means of checking understanding.
There are different degrees of appreciation of formalization as a test of mathematical understanding. I have frequently quoted Atiyah's comment that "the proof isn't the main thing" but rather a sign that one is one the right track.
At this point I have to fall back on my impressions of what is and is not important to the mathematicians with whom I am primarily in contact. With few exceptions they agree with me, and I have urged them to make their opinions known, but to no avail.
Well it probably doesn't help that I do mathematical logic so myself and all the other mathematicians I'm in contact with tend to be relatively partial to the usefulness of full formalization if for not other reason than we study it.
Here's perhaps a more borderline example along the line of the one you discuss: did Peter Scholze waste the time of the whole team of people (and his own, in following the process throughout) for 6 months when they formalised the proof of his result with Clausen about liquid vector spaces? (Another variable, which complicates matters is that a number of them were early career researchers, and might well have spent that time on traditional mathematical pursuits, to not set their careers a-wobbling, in comparison to Hales, who wouldn't need to worry; so the timescale is perhaps appropriately relative, here.)
In the process, understanding of the proof—not to mention a simplification—*was* gained. I'm curious to know your take.
Thank you for this question. Maybe you will find this answer facile, but I can't think of a better one: only the participants in the project can say whether they wasted their time. I guess none of them will. Commelin, who led the team, reported on the project at the Fields Medal Symposium and made it clear that he found the process rewarding in many ways — not only because it provided an opportunity for him to understand and to simplify the proof.
As for the others, insofar as their satisfaction is in part due to their impression, amplified by the media, that they were participating in a project of historic significance, only time will tell whether this impression is justified.
But let me also try to give my opinion of the role formal proofs play in mathematical practice (some ideas here resemble/are influenced by Kenny Easwaran's work in philosophy of math...but it's not quite the same so if you are interested read his paper).
The short version is that what makes us believe that we understand a proof (ie understand it well enough to say it's correct) is that we think we could fill in the missing details given enough time and interest. And in some sense a fully formal proof represents the limit of filling in the details.
But this isn't saying that it's always better to be more formal. If I understand a proof I can be very confident I could fill in all the missing details given enough time. If it's just a bunch of calculations or other overly formal crap I won't be so confident. Yes, sometimes when I get myself sufficiently confused about some quantified statement I do drop back almost the the level of formal proof for long enough to convince me I know what I'm doing but if the proof was presented at that fine grained level of detail I could never (w/o a computer) keep enough of it in mind to actually be confident it was correct (so not confident I could fill in 'gaps').
Ofc, that's just a theory about what makes a proof convincing. If doesn't address other concerns like understanding, ability to use/modify the proof to prove other results etc.. which also matter for mathematics.
So I feel like it might help to be precise about what is being claimed here. Specifically, there is the cultural practice of mathematics and the project of increasing our knowledge (both in terms of new theorems and increasing our confidence in old ones) of mathematical claims. It is primarily the second (inc confidence) that machine checked proofs are relevant to.
For instance, are you really calling into doubt the claim that a fully formal, computer verified (say by multiple independent checkers using a very simple proof system like FOL natural deduction/sequent calc) gives us a particularly high level of confidence there are no gaps in the proof? At the very least that the fully formal fol statement of the theorem is proved?
Given my own experience writing and reviewing math papers that increase in certainty seems quite attractive and significant.
And don't be so sure companies don't care about it. If I'm marketing a new encryption product a form proof that it's secure under such and such computational assumptions *especially* if it's machine checked seems incredibly valuable to my sales. Being able to produce formal proofs that safety critical software systems have certain properties is also very valuable. And the ability to produce a fully formal machine checked proof is potentially valuable to compiler designers.
I fully agree with the point you make in your last paragraph, and I have made it repeatedly in this newsletter, often in conjunction with references to Donald MacKenzie's book "Mechanizing Proof." See for example the reference to MacKenzie's book at this early post: https://siliconreckoner.substack.com/p/on-the-implications-of-scholzes-liquid
Although I haven't spelled out the implication explicitly, I also believe that familiarity with this very important function of formal proof verification in software development has convinced many computer scientists that formalization is just as central in mathematics.
With regard to your second paragraph, the first question is whether "confidence" is what is primarily being sought, the second question is what use might be made of the fully formal statement of the theorem. I began by pointing out that most of the mathematical professions represented at the JMM are not terribly concerned with proof. The conception of mathematics as bound up with proofs in formal systems is a relatively recent development in the history of mathematics, although it certainly has ancient antecedents. It is not valid to claim that it expresses the primary virtue of mathematics; the references in footnote 6 point to very different pictures of mathematics, including some in which formalism is quite opposed to what at the time was considered valuable in mathematics.
But I'm literally supposed to be proving things now do better get back to it ;-)
I agree they aren't that concerned with proof per se. However, I think that outside of the realm of computer assistance the ability to be able to produce a proof of any desired degree of formality (eg someone doubts step 5 you could give more and more details and , if necessary, give a fully formal version with enough time) turns out to be our best evidence/test of mathematical understanding.
Math is an area it's easy to get confused in and the role of increasing formalization is to provide a way to check that we (or they) aren't confused.
Now you might worry that you might occasionally get someone with great understanding who isn't good at formalization (Ramanujan) but I'd argue that relative to the difficulty of math the cost to learn to offer more details (enough to convince someone formalization could be possible) is relatively small it's just B4 modern era we didn't always insist on this common means of checking understanding.
There are different degrees of appreciation of formalization as a test of mathematical understanding. I have frequently quoted Atiyah's comment that "the proof isn't the main thing" but rather a sign that one is one the right track.
At this point I have to fall back on my impressions of what is and is not important to the mathematicians with whom I am primarily in contact. With few exceptions they agree with me, and I have urged them to make their opinions known, but to no avail.
Well it probably doesn't help that I do mathematical logic so myself and all the other mathematicians I'm in contact with tend to be relatively partial to the usefulness of full formalization if for not other reason than we study it.
but as I said should be doing my math now.