A formal proof of Pick's Theorem

DOI10.1017/S0960129511000089zbMath1223.68103OpenAlexW1997850401MaRDI QIDQ3094172

No author found.

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000089

zbMATH Keywords

lattice pointsformal proofPick's theorempolygonal pathHOL Light theorem proverinside and outside

Mathematics Subject Classification ID

Uses Software

• HOL Light

Cites Work

• Unnamed Item
• Formalizing an analytic proof of the prime number theorem
• Without Loss of Generality
• Euler's characteristics and Pick's theorem
• The Jordan-Schonflies Theorem and the Classification of Surface
• Another Proof of Pick's Area Theorem
• Pick's Formula via the Weierstrass ℘-Function

This page was built for publication: A formal proof of Pick's Theorem