Skip to main content

An isabelle/HOL formalisation of green's theorem


Mohammad Abdulaziz and Lawrence Paulson


University of Cambridge


We formalise a statement of Green’s theorem in Isabelle/HOL, which is its first formalisation to our knowledge. The theorem statement that we formalise is enough for most applications, specially in physics and engineering. An interesting aspect of our formalisation, is that we do not formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to equivalences between paths.

BibTeX Entry

    author           = {Abdulaziz, Mohammad and Paulson, Lawrence},
    month            = aug,
    year             = {2016},
    keywords         = {formalised mathematics, mathematical analysis},
    address          = {Nancy, France},
    title            = {An Isabelle/{HOL} Formalisation of Green's Theorem},
    booktitle        = {International Conference on Interactive Theorem Proving}


Served by Apache on Linux on seL4.