Formalizing basic complex analysis

John Harrison.

Dedicated to Andrzej Trybulec on the occasion of his 65th birthday. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric vol. 10(23), pp. 151-165, 2007.

Abstract:

We describe the formalization of some of the basics of complex analysis in the HOL Light theorem prover. Besides being a beautiful area of mathematics, this has many potential applications, e.g. in analytic number theory. We have endeavoured to set up the kind of general analytic machinery that would make such applications feasible.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-complexanalysis,   
        author          = "John Harrison",
        title           = "Formalizing Basic Complex Analysis",
        editor          = "Matuszewski, R. and Zalewska, A.",
        booktitle       = "From Insight to Proof: Festschrift in Honour of
                           Andrzej Trybulec",
        publisher       = "University of Bia{\l}ystok",
        series          = "Studies in Logic, Grammar and Rhetoric",
        volume          = "10(23)",          
        year            = 2007,                      
        pages           = "151--165",                                      
        url             = "http://mizar.org/trybulec65/"}