4 ms·
Mathematician here: It isn't exactly that proof assistants are looked down upon. Rather, most of us don't do 1st order logic and it isn't on anybodies radar. Ev
by knappa 9y ago
Mathematician here: It isn't exactly that proof assistants are looked down upon. Rather, most of us don't do 1st order logic and it isn't on anybodies radar. Even if it were, it is often new proof techniques that lead to new interpretations, generalizations and discoveries about what we should be trying to prove in the first place. It is very hard to interpret a wall of 1st order logic.
Not to mention decidability issues.
- foobar__ 9y agoBoth Isabelle and Coq are based on higher-order logics, so I am not sure how first-order logic is a barrier to entry. Especially Isabelle is very easy to use because the logic is so standard with nothing really surprising or especially restricting (a very strong form of the axiom of choice is deeply embedded in the system, so it's probably harder if you care about it at this level). 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.