@InProceedings{W13,
  key    =       {W13},
  author =	 {Christoph Benzm{\"u}ller and Manfred Kerber},
  title =	 {A Lost Proof},
  booktitle =	 {Proceedings of the IJCAR 2001 Workshop: Future Directions in Automated
                  Reasoning},
  year =	 2001,
  pages =        {13--24},
  chrisnote =	 {W13},
  url =		 {www.ags.uni-sb.de/~chris/papers/W13.pdf},
  address =	 {Siena, Italy},
  abstract =	 {We re-investigate a proof example presented by George Boolos which
                  perspicuously illustrates G\"odel's argument for the potentially drastic
                  increase of proof-lengths in formal systems when carrying through the
                  argument at too low a level. More concretely, restricting the order of
                  the logic in which the proof is carried through to the order of the
                  logic in which the problem is formulated in the first place can result
                  in unmanageable long proofs, although there are short proofs in a logic
                  of higher order. Our motivation in this paper is of practical nature and
                  its aim is to sketch the implications of this example to current
                  technology in automated theorem proving, to point to related questions
                  about the foundational character of type theory (without explicit
                  comprehension axioms) for mathematics, and to work out some challenging
                  aspects with regard to the automation of this proof -- which, as we
                  belief, nicely illustrates the discrepancy between the creativity and
                  intuition required in mathematics and the limitations of state of the
                  art theorem provers.}
}