Long and Short Proofs

Abstract

We study the “gap" between the length of a theorem and the smallest length of its proof in a given formal system T. To this aim, we define and study f-short and f-long proofs in T, where f is a computable function. The results show that formalisation comes with a price tag, and a long proof does not guarantee a theorem’s non-triviality or importance. Applications to proof-assistants are briefly discussed.