  The proof identity problem asks: When are two proofs the same? The question
naturally occurs when one reflects on mathematical practice. The problem
understandably can be seen as a challenge for mathematical logic, and indeed
various perspectives on the problem can be found in the proof theory
literature. From the proof theory perspective, the challenge is met by laying
down new calculi that eliminate ``bureaucracy''; techniques such as
normalization and cut-elimination, as well as proof compression, are employed.
In this note a new perspective on the proof identity problem is outlined. The
new approach employs the concepts and tools of automated theorem proving and
complements the rather more theoretical perspectives coming from pure proof
theory. The practical approach is illustrated with experiments coming from the
TPTP Problem Library.
