It seems very probable that quantum computers could solve some problems (e.g. factoring of integers) much faster than any classical computers. A natural question is whether quantum computers could also help us produce proofs that would be too long or too difficult to find by classical means. Though this problem is well known, no results have been obtained so far. We shall study this problem from the point of view of proof complexity. Our aim is to find the quantum concept that corresponds to the classical Frege proof systems.