Formalizing Basic Complex Analysis Dedicated to Andrzej Trybulec on the occasion of his 65th birthday
John R Harrison · 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. 0 Mizar and me: some personal recollections The first time I saw mention of the Mizar project was in a message from Bob Boyer to the QED mailing list in August 1993: 1 Indeed, there have been a good number of QED-like efforts spread over at least the last 27 years, both large scale and small. (I hear rumors that the Polish MIZAR effort may be the largest so far.) At the time, even though Mizar had a large and thriving user community all over the world, I hadn’t heard of it at all, so my curiosity was piqued. The following summer, the second QED Workshop was in Warsaw, and I had the opportunity to meet Andrzej Trybulec in person for the first time. This was a memorable experience in many ways, and immediately after the workshop a few participants travelled to Białystok where we had the opportunity to try out Mizar for ourselves with Andrzej’s help. I was impressed that Andrzej was willing to devote so much time to helping out some complete beginners. But I was equally impressed how little his help was needed! After a few hours, I was able to prove in Mizar the formula for the roots of a quadratic equation. To someone with no experience of proof assistants, that might seem an unspectacular accomplishment, but Mizar seemed to be dramatically easier to use than the other systems I’d tried, particularly HOL [3], with which I was most familiar. Over the next few months, back in Cambridge (where I was supposed to be finishing my PhD) and in Turku / ˚Abo in Finland (where I was doing a postdoc under the EU Human Capital and Mobility scheme), I often thought about why Mizar’s proof language seemed much easier to use. I became convinced that Andrzej’s design had many key features that we should emulate in other systems, and at the TPHOLs conference in 1996, I presented a paper [4] where I described a simple ‘clone ’ of some features of the