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.