We shall define a quantum analog of the concept of Frege proof
systems for propositional logic. We shall show that every such quantum
proof contains a classical Frege proof, thus we do not get shorter proofs.
We shall show that, assuming plausible conjectures, the problem of
extracting a classical proof from a quantum proof is hard.