Calude, CSStaiger, L2023-01-242023-01-242022CDMTCS Research Reports CDMTCS-561 (2022)1178-3540https://hdl.handle.net/2292/62556We 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.Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated. Previously published items are made available in accordance with the copyright policy of the publisher.https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htmTechnical ReportFields of ResearchCopyright: The author(s)http://purl.org/eprint/accessRights/OpenAccess