I do not understand why mathematicians look down on proof assistants. I've heard this claim multiple times and it continues to make no sense to me.
Are there any mathematicians here who can weigh in?
Are there any mathematicians here who can weigh in?
On the one hand we have something like the 4-colour theorem where there is some kind of "proof", which is very large and incomprehensible. This is probably unsatisfactory to many because one is not really interested in just knowing that something is true, but ideally one also want an understanding of "why" something is true. This is, to various degrees, achived in more standard proofs.
Another reason for disliking proof assistants is probably that they simply are very cumbersome to use and not very much can be proven with them so far. I would guess that even if you could get someone to admitt that the idea is cool and could be very useful, it's just not practical and for most people in mathematics it's just a distraction from what they are trying to work on at the moment.
Compare with trying to convince someone that a flying car is really cool, yeah, sure, it probably would be, but so far it's basically sci-fi. If you want to work on building this, great, but most commuters will probably "look down" on your idea if you start bugging them about it.
To be specific, I've used Coq in the past to help verify properties of programs such as a sorted list really being sorted. That said, I primarily work in applied math areas such as optimization, numerical linear algebra, and numerical PDEs and I have no idea where to begin with fundamental proofs such as Newton's method converging quadratically within a certain neighborhood of the solution. Alternatively, I'd love to see formalized proofs of the theorems that we'd learn in a course in real analysis such as one based on Rudin's Principles of Mathematical Analysis. Really, if anyone has examples of these, please let me know.
There's an amazing number of errors in published work. Most of the time, the work is still mostly right, but that's not OK. In my opinion, we'd be better off with formalized proofs.
It may be rather an off-topic, but I suggest you to read my funny paper: https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5...
Not to mention decidability issues.
Regarding your second point, to me this looks pretty much the same as in software: In high-quality code I expect high-level comments that give me intuition about the code, and I also expect high-level documentation giving me further intuition about the components and the system as a whole. The more complicated the system is, the more important the comments and the documentation become.
I see no reason why we should hold computer-assisted proofs to a lesser standard.
There's some attempts to alleviate these problems, which are named Homotopy Type Theory, and they are quite successful.
From what I have seen, proof assistants in math are used when extreme rigour is desired (which is not always the case) and when working with extremely long computational proofs with hundreds of cases (where you need to work at a higher abstraction level; a human writes a program that outputs the proof and then the proof checker verifies that this extremely long step by step proof is valid)
Proof assistants are the opposite. Sacrifice intuition and insight for the sake of correctness.
This is also why mathematicians love picture proofs.
I love pictures that give me intuition about a proof and I agree that intuition is crucial to understanding. But all the intuition in the world is useless if the proof fails because of one tiny logically unsound step or one pathological corner case, so it's no good to ignore the technical details or, even worse, to become unable to expand a purpoted proof one has written into a fully detailed version, which I suppose can easily happen if someone relies too much on intuition.
That being said, I often find convincing, false proofs as illuminating as true proofs, once the flaw is clear, because they highlight the nature of the conjecture. So I disagree with your claim that a proof can suddenly become useless due to a slight misstep.
And for what it's worth, theorems are rarely thrown out due to pathological corner cases; at least I've never heard of this happening. Instead, if the insight conveyed by the proof is useful, it's called a partial result and the conditions are modified to fit the proof. Entire theories are built up specifically to avoid pathology (almost every mathematical field does this)