Fall 23 project: Convex polygons

Stream: Rutgers Lean seminar

[Vláďa Sedláček]

A thread for finishing a general API that handles convex polygons and their areas. The current state is here: https://github.com/ianjauslin-rutgers/pythagoras4/blob/IsConvex/Pythagoras/convex_polygon.lean

[Alex Kontorovich]

We should talk about this thread next time: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/tarski.20axiom.20geometry/near/393409879 In particular, we can go through the notes here and compare to how we do things: https://adg2023.matf.bg.ac.rs/downloads/slides/IntroductionBoutryNarboux.pdf Any volunteers to give an exposition?

[Kevin Buzzard]

Like I said there, if there's any way that you can end up proving circle theorems in lean with graphics being displayed then I'm adding an entertaining talk on top and taking it straight into high schools. I would love any progress here. Joseph Myers has developed a ton of theory in lean and even solved an IMO geometry problem (it's in mathlib) but he's been a little distracted by Einsteins and hats recently...