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.