9 Comments

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.

Expand full comment

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.

Expand full comment

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.

Expand full comment