99 Variations on a Proof https://press.princeton.edu/books/hardcover/9780691158839/99...

and the newly published paper

Draft, Sketch, and Prove: Guiding Formal Theorem Provers With Informal Proofs https://arxiv.org/pdf/2210.12283.pdf

As you all know De Morgan's Laws provide great simplification of terms to canonical forms. Application of these laws improved circuit design forever.

My question: Can "Irrelevance Laws" be developed in proofs so one style of proof can be mechanically converted to another style? If so, can a system like LEAN convert the library to canonical forms?

Canonical forms of proof, if they exist, and if they have the proper form, would make it possible to develop "proof compilers" that could generate code from (constructive) proofs. (See Ording 28, p65, of special interest).

Is there any reason to believe canonical forms exist? I know that judgment towers can be expanded in various ways. Perhaps there is a mechanical theory to put (some of) the LEAN library in "canonical form".

Beside the book, is there any known collection of proof transformation?