Can Proof Technology Even Do this?

[dennis at logicalphalluses.net]

> a formal system S and a sentence phi, and the problem is to prove phi from S

You seem to equate "proof assistants" (ITPs) with "automated theorem 
provers" (ATPs). Proof assistants assist with proving, they don't do the 
proving (entirely) for you. Almost every proof assistant contains some 
or several ATPs for convenience, but some don't (e.g. metamath).

I think you're making a mistake by measuring the success of ITPs merely 
by how powerful they are as ATPs.

> A. Start with the axioms of Peano Arithmetic in the language of
> 0,S,+,x, the usual with finitely many axioms and the induction scheme.
> Prove: every number is of the form n+n or n+n+1 but not both.
> B. Same start as A. Prove: commutative, associate laws for +,x, and
> the distributive law, and also the monotonicities.

I'm pretty sure there isn't a single ITP that does *not* have proofs for 
these, so I would consider that challenge to be solved by every ITP. If 
your challenge is that the system should be able to prove them 
automatically entirely with no or only few hints, then there will be 
failures. But that's not what ITPs are for.

The value of ITPs lies in lots of small conveniences that allow to 
express proofs in such a way that they can be *checked* to be correct, 
and to help with filling in gaps via ATPs and other means. By doing so, 
they allow you to find gaps or flaws in your reasoning, structure your 
proofs more clearly and refine your understanding of one. The value also 
lies in making any notion, notation, definition, statement etc. 
unambiguous by design, rather than relying on a reader having to know 
(or, rather often, assume to know or guess) what they mean. They make 
the *semantics* of statements accessible for e.g. search.

ITPs have other problems in my opinion, e.g. that the conveniences they 
bring currently don't outweigh the enormous cost of familiarizing 
oneself well enough with a system and its library to survive a 
cost-benefit-analysis, and the result looks nothing like math looks on 
paper. But those are ultimately problems with the surface languages, not 
with the systems themselves as they operate on internal abstract syntax 
trees (which is why I'm currently working on a system that uses 
unrestricted plain latex as input). But "they don't find proofs 
automatically for arbitrarily complicated statements and in the same way 
as a human would do it" is not a problem I would measure ITPs on (alone).

Cheers

-- Dr. Dennis M. Müller

"To do mathematics is to be, at once, touched by fire and bound by
reason. This is no contradiction. Logic forms a narrow channel through
which intuition flows with vastly augmented force"

  - Jordan Ellenberg (How Not to Be Wrong)