Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.)
What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?
I think there are two parts:
1) Improve the theorem proving languages syntax so it's more intuitive, and so there is a wealth of "libraries" to build upon so you don't have to go from the basic axioms (of arithmetic or the reals for example) any time you wanted to prove something.
2) Provide some sort of computational intelligence to fill in natural gaps of proofs. I believe humans tend to leave a large number of more or less trivial gaps even in rigorous mathematical proofs that couldn't be avoided by language syntax. For this probably some kind of AI system would be ideal that tries to derive successive results and complete the proof automatically.
You can help its heuristics by providing it a set of potential proof facts explicitly.
The libraries available for it are already quite huge... sometimes in a few encodings as well. (valued, typed, functional etc.)
It's used for clustering statements and proofs, the idea being that if you're stuck trying to prove something, you might be able to find something "similar" in an existing library to use as inspiration. It's mostly to help with manual searches, rather than automatically solving anything (although there is some related work on doing that for Coq called SEPIA https://arxiv.org/abs/1505.07987 and ACL2 http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html ).
And none of its dependencies actually exist either. Like someone just said... relational database? Yeah we could write one of those...
To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on...
It's quite dense, but there are some bits that I, as a programmer, could understand.
Put a space before the final ), else it becomes part of the URL. Thanks for the paper, by the way.
However, it shoudln't deter us from the goal.
People used to code in assembly and Fortran. It was and still is quite painful.
But programming languages have improved, and resorting to those original languages (which is what Coq is) is rarely necessary these days.
[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
In other words, it's actually very easy to prove something with a computer, but it's very difficult to prove the thing you actually set out to prove. It's not any easier than writing a bug-free program.
If you're referring to the fact that many proof assistants (e.g. Coq) are based on constructive/intuitionistic type theory, whilst most mathematics is formulated in classical set theory, then yes there is some translation involved. However, I would point out that we can use classical logic pretty easily by adding excluded middle, double negation elimination, etc. to an intuitionistic system (this is available in the Coq standard library https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html ). There are also systems which can use set theory (directly or indirectly), like Metamath and Isabelle.
Personally, I much prefer type theory (which I self-learned, before pursuing a related PhD) to set theory (which I was taught as an undergraduate and enjoyed, but not enough to do it as a hobby). However, I'm well aware that my computer scientist background is nothing like that of a trained mathematician.
The reality is that we often overlook issues with the spec until we try to implement it, or try using what we have implemented, even when we are trying to get the spec right first.
theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare
"Proof assistants" like Coq and Isabelle can generate some of the more "obvious" steps using metaprogramming (known as "tactics").