Email Gateway (May 01 2024 at 13:43): Email Gateway (May 01 2024 at 13:43):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new entry: Pick's theorem, by Sage Binder and Katherine Kosaian.
We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem in HOL Light, but tailor our proof approach to avoid a primary challenge point in his formalization, which is proving that any polygon with more than three vertices can be split (in its interior) by a line between some two vertices. Our formalization involves augmenting the existing geometry libraries in various foundational ways (e.g., by adding the definition of a polygon and formalizing some key properties thereof).
It's a substantial development, nearly 45% bigger than my formalisation of the incompleteness theorems. It also takes Isabelle up to 90 on Freek's List of 100 problems! (See https://www.cs.ru.nl/~freek/100/)
https://www.isa-afp.org/entries/Picks_Theorem.html
Larry
Last updated: May 19 2024 at 04:18 UTC