Long and Short Proofs

Calude, CS; Staiger, L

dc.contributor.author	Calude, CS	en
dc.contributor.author	Staiger, L	en
dc.date.accessioned	2023-01-24T23:04:43Z
dc.date.available	2023-01-24T23:04:43Z
dc.date.issued	2022	en
dc.identifier.citation	CDMTCS Research Reports CDMTCS-561 (2022)	en
dc.identifier.issn	1178-3540	en
dc.identifier.uri	https://hdl.handle.net/2292/62556
dc.description.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.
dc.publisher	Department of Computer Science, The University of Auckland, New Zealand	en
dc.relation.ispartofseries	CDMTCS Research Report Series	en
dc.rights	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.	en
dc.rights.uri	https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htm	en
dc.source.uri	https://www.cs.auckland.ac.nz/research/groups/CDMTCS/researchreports/index.php	en
dc.title	Long and Short Proofs	en
dc.type	Technical Report	en
dc.subject.marsden	Fields of Research	en
dc.rights.holder	Copyright: The author(s)	en
dc.rights.accessrights	http://purl.org/eprint/accessRights/OpenAccess	en