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.