Average-Case Separation in Proof Complexity: Short Propositional Refutations for Random 3CNF Formulas Iddo Tzameret Abstract: Separating different propositional proof systems--that is, demonstrating that one proof system cannot efficiently simulate another proof system--is among the main goals of proof complexity. Nevertheless, all known separation results between non-abstract proof systems are for specific families of hard tautologies: for what we know, in the average case all (non-abstract) propositional proof systems are no stronger than resolution. In this paper we show that this is not the case, by demonstrating polynomial-size propositional refutations whose lines are TC^0 formulas (i.e., TC^0-Frege proofs; also known as Threshold Logic) for random 3CNF formulas with n variables and Omega(n^1.4) clauses. By known lower bounds on resolution refutations, this implies an exponential separation of TC^0-Frege from resolution in the average case (for this clause-to-variable ratio). The idea is based on demonstrating efficient propositional correctness proofs of the random 3CNF unsatisfiability witnesses given by Feige, Kim and Ofek (FOCS 2006). Since the soundness of these witnesses is verified using spectral techniques, we develop an appropriate way to reason about eigenvectors in propositional systems. To carry out the full argument we work inside weak formal systems of arithmetic, use a general translation scheme to propositional proofs and then show how to turn these proofs into random 3CNF refutations. Joint work with Sebastian Muller.