A Formal Proof of Cauchy’s Residue Theorem

DOI10.1007/978-3-319-43144-4_15zbMath1478.68440OpenAlexW2485576930WikidataQ57382537 ScholiaQ57382537MaRDI QIDQ2829261

Wenda Li, Lawrence Charles Paulson

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://www.repository.cam.ac.uk/handle/1810/262370

Mathematics Subject Classification ID

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

Related Items

Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• C-CoRN
• Coquelicot
• kepler98

Cites Work

• Unnamed Item
• A formally verified proof of the central limit theorem
• The HOL Light theory of Euclidean space
• Coquelicot: a user-friendly library of real analysis for Coq
• Formalizing an analytic proof of the prime number theorem
• An Elementary Proof of the Stone-Weierstrass Theorem
• Complex Analysis
• Mathematical Knowledge Management
• Complex Analysis
• Algorithms in real algebraic geometry