> 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.
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.