A certified proof of the Cartan fixed point theorems (Q438546)

The paper consists of two big parts, the first is a crash course in complex analysis, the second reports on the formalization of some of the proofs in the mechanized reasoning system HOL-light. In the first part, the authors introduce holomorphic functions and some of their surprising properties (when compared to their real counterparts), e.g., the identity principle. First the one-dimensional case and then some higher-dimensional theorems are introduced. With these preliminaries the first and second theorem of Cartan are introduced -- that under certain weak conditions a holomorphic higher-dimensional map must be the identity map or it must be linear, respectively. Furthermore the proofs of these theorems are sketched. In addition, a theorem on an involution and a relationship of holomorphic automorphisms and Möbius transformations is given. In the second part of the paper the HOL-light system and its extensive library on real and complex numbers are introduced. In order to prove Cartan's theorems, important properties such as the rule on the derivative of composed functions are introduced. The paper concludes with remarks on the de Bruijn factor (how much longer the formal proofs are compared to paper proofs), and the procedural (what is done to produce a proofs) versus declarative (how does the proof look like) style of proofs in formal systems.