Cristian S. Calude, Ludwig Staiger: Long and short proofs, 203-211

Abstract:

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

Key Words: Proof length, proof-assistant.

2010 Mathematics Subject Classification: Primary 03B22, 03B35; Secondary 00A30, 03A10.