We study the “gap" between the length of a theorem and the smallest
length
of its proof in a given formal system
![${\mathbf{T}}$](img22.png)
. To this aim, we define and
study
![$f$](img4.png)
-short and
![$f$](img4.png)
-long proofs in
![${\mathbf{T}}$](img22.png)
, where
![$f$](img4.png)
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.