A formal proof of Cauchy’s residue theorem. (English) Zbl 1478.68440

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 235-251 (2016).
Summary: We present a formalization of Cauchy’s residue theorem and two of its corollaries: the argument principle and Rouché’s theorem. These results have applications to verify algorithms in computer algebra and demonstrate Isabelle/HOL’s complex analysis library.
For the entire collection see [Zbl 1343.68004].


68V20 Formalization of mathematics in connection with theorem provers
03B35 Mechanization of proofs and logical operations
30E20 Integration, integrals of Cauchy type, integral representations of analytic functions in the complex plane
Full Text: DOI Link


[1] Ahlfors, L.V.: Complex Analysis: An Introduction to the Theory of Analytic Funtions of One Complex Variable. McGraw-Hill, New York (1966)
[2] Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the central limit theorem. CoRR abs/1405.7012 (2014) · Zbl 1425.68369
[3] Bak, J., Newman, D.: Complex Analysis. Springer, New York (2010) · Zbl 1205.30001
[4] Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry, vol. 10. Springer, Heidelberg (2006) · Zbl 1102.14041
[5] Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2014) · Zbl 1322.68176
[6] Brunel, A.: Non-constructive complex analysis in Coq. In: 18th International Workshop on Types for Proofs and Programs, TYPES 2011, Bergen, Norway, pp. 1–15, 8–11 September 2011
[7] Bruno Brosowski, F.D.: An elementary proof of the Stone-Weierstrass theorem. Proc. Am. Math. Soc. 81(1), 89–92 (1981) · Zbl 0482.46014
[8] Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, New York (2012)
[9] Conway, J.B.: Functions of One Complex Variable, vol. 11, 2nd edn. Springer, New York (1978)
[10] Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004) · Zbl 1108.68586
[11] Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. arXiv:1501.02155 (2015)
[12] Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, vol. 10(23), pp. 151–165. University of Białystok (2007)
[13] Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reasoning 43, 243–261 (2009) · Zbl 1185.68624
[14] Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50, 173–190 (2013) · Zbl 1260.68373
[15] Lang, S.: Complex Analysis. Springer, New York (1993) · Zbl 0819.30001
[16] Stein, E.M., Shakarchi, R.: Complex Analysis, vol. 2. Princeton University Press, Princeton (2010) · Zbl 1020.30001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.