A formal proof of Cauchy's residue theorem

DOI10.1007/978-3-319-43144-4_15zbMATH Open1478.68440DBLPconf/itp/LiP16OpenAlexW2485576930WikidataQ57382537 ScholiaQ57382537MaRDI QIDQ2829261FDOQ2829261

Lawrence C. Paulson, Wenda Li

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

Recommendations

• Cauchy's residue sore thumb
• Formalizing an analytic proof of the prime number theorem
• A direct proof and a transcendental version of the fundamental theorem of algebra via Cauchy's theorem
• An Isabelle/HOL formalisation of Green's theorem
• An Isabelle/HOL formalisation of Green's theorem

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)

Cites Work

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

Cited In (2)

• 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

This page was built for publication: A formal proof of Cauchy's residue theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829261)