ABSTRACT
Languages of symbolic logic which are adequate for formalizing mathematics are excellent vehicles of expression for automated mathematical systems, since they have great generality, clear and simple syntax which facilitates processing by computers, and symbolism closely related to that which is used in mathematical practice. It would be useful for researchers on automating mathematics to arrive at a consensus concerning which languages are most appropriate for such endeavors, since this would facilitate valuable cooperation in this field. Probably the best known language for formalizing mathematics is axiomatic set theory, but there are certain advantages to using type theory (also known as higher-order logic), especially in a formulation due to Alonzo Church which incorporates λ-notation. Higher-order logic needs to be more widely known, so it is described and discussed, with special attention to typed λ-calculus and issues relevant to the automation of mathematics.
