A key aspect of finding mathematical proofs is to notice the (syntactic) similarity between terms in the given statement. This thesis aims at developing a formal notion of syntactic similarity that is suitable for human-oriented automated theorem proving. To this end, it is investigated how tree-edit distance can be used for comparing syntax trees. The outcome is a metric between (typed) syntax trees and a term that qualitatively describes how two given syntactic expressions are related. These theoretical concepts are compared with preexisting research and are implemented in Lean 4. A small case study gives a first impression of how the derived notion of syntactic similarity performs with respect to premise selection.

Higher-order logic (HOL) offers a simple syntax and semantics for representing and reasoning about typed mathematical concepts. There are many state-of-the-art automated theorem provers for HOL. But the type system of HOL lacks advanced features where types may depend on terms. This is useful as many mathematical notions are inherently dependent typed. Dependent type theory offers such a rich type system but has rather substantial conceptual differences to HOL and isn’t supported as well by automated theorem provers. We introduce a dependently typed extension DHOLP of HOL that supports dependent types while retaining the style and conceptual framework of HOL. Moreover, we describe one translation from DHOLP and a second one from one of its fragments to HOL and prove the soundness and completeness of the translations. We implement both translations within the MMT system—a system for formalizing mathematics—where they are combined with a HOL prover into an automated theorem prover for DHOLP. Finally, we formalize basic set theory notions in DHOLP and outline how such a formalization can be combined with a recent translation of the language of the Mizar proof assistant to MMT to obtain an automated theorem prover for problems in the language of the Mizar proof assistant.