"Are most areas safe, or contaminated?"

Most areas are fine. Probably all important areas are fine. Mathematics is fine. The important stuff is 99.99999% likely to be fine because it has been carefully checked. The experts know what is wrong, and the experts are checking the important stuff. The system works. The system has worked for centuries and continues to work.

My talk is an intentionally highly biased viewpoint to get people talking. It was in a talk in a maths department so I was kind of trolling mathematicians. I think that formal proof verification systems have the potential to offer a lot to mathematicians and I am very happy to get people talking about them using any means necessary. On the other hand when I am talking to the formal proofs people I put on my mathematician's hat and emphasize the paragraph above, saying that we have a human mathematical community which knows what it is doing better than any computer and this is why it would be a complete waste of time formalising a proof of Fermat's Last Theorem -- we all know it's true anyway because Wiles and Taylor proved it and since then we generalised the key ideas out of the park.

It is true that there are holes in some proofs. There are plenty of false lemmas in papers. But mathematics is *robust* in this extraordinary way. More than once in my life I have said to the author of a paper "this proof doesn't work" and their response is "oh I have 3 other proofs, one is bound to work" -- and they're right. Working out what is true is the hard, fun, and interesting part. Mathematicians know well that conjectures are important. But writing down details of an argument is a lot more boring than being imaginative and figuring out how the mathematical world works, and humans generally do a poorer job of this than they could. I am concerned that this will impede progress in the future when computers start to learn to read maths papers (this will happen, I guess, at some point, goodness knows when).

Another thing which I did not stress at all in the Pittsburgh talk but should definitely be mentioned is that although formal proof verification systems are far better when it comes to reliability of proofs, they have a bunch of other problems instead. Formal proofs need to be maintained, it takes gigantic libraries even to do the most basic things (check out Lean's definition of a manifold, for example), different systems are incompatible and systems die out. Furthermore, formal proof verification systems *currently* have essentially nothing to offer the working mathematician who understands the principles behind their area and knows why the major results in it are true. These are all counterpoints which I didn't talk about at all.

In the future we will find a happy medium, where computers can be used to help humans do mathematics. I am hoping that Tom Hales' Formal Abstracts project will one day start to offer mathematicians something which they actually want (e.g. good search for proofs, or some kind of useful database which actually helps us in practice).

But until then I think we should remember that there's a distinction between "results for which humanity hasn't written down the proof very well, but the experts know how to fill in all of the holes" and "important results which humanity believes and are not actually proved".

I guess one thing that worries me is that perhaps there are areas which are currently fashionable, have holes in, and they will become less fashionable, the experts will leave the area and slowly die out, and then all of a sudden someone will discover a hole which nobody currently alive knows how to fill, even though it might have been the case that experts could once do it.

If my work in pure mathematics is neither useful nor 100 percent guaranteed to be correct, it is surely a waste of time.There would appear to be a gap in this argument, unless the author has a general proof that "not useful" plus "not 100% guaranteed to be correct" implies "waste of time", in which case there are myriad special cases outside of mathematics, many of them quite surprising and unsettling. $\endgroup$ – Steven Landsburg Jan 31 '20 at 17:50what fraction of your own papers do you expect to rely on a statement "for which humanity does not actually have a complete proof"Zero, but the catch is that I insisted on claiming the proof of the reduction of A to B (B being published by other people and universally accepted as valid) instead of claiming A itself at least twice (not that my co-authors were very happy about it, but I find it a good practice if one has trouble going through the whole proof tree of B yourself). On the other hand, I'm guilty of publishing at least 2 papers in which some gap was later found (and closed). $\endgroup$ – fedja Jan 31 '20 at 22:17? fedja just described the perfectly acceptable practice of working in a high-level system where you just take some B on faith, a.k.a. make it part of your axioms. (Likewise people in Paris used to speak of “axiom Valiron”:from what axiomseverything in.) Of course, the risk in doing this is, your resulting axiom system might be inconsistent. But then so might ZFC, right? (1/2) $\endgroup$ – Francois Ziegler Jan 31 '20 at 23:22this bookis truemightbe found) as hugely different from “relying on stuff that is wrong” (a contradictionhasbeen found). (2/2) $\endgroup$ – Francois Ziegler Jan 31 '20 at 23:227more comments