search

coq-community / coq-100-theorems

Statements of famous theorems proven in Coq [maintainer=@jmadiot]
https://madiot.fr/coq100/
Other
55 stars 14 forks source link

No code link for Ptolemy's theorem #11

Closed palmskog closed 4 years ago

palmskog commented 4 years ago

Despite some searching, I can't find any Coq code at all for Ptolemy's theorem (95), although there is a publication. Since Coq is about "reproducible" (locally checkable) proofs, I don't think it's enough to claim that something "has been proved in Coq", for inclusion in the list - the code has to be available as well for anyone interested. Hence, I think entry 95 should be removed until the code becomes available.

ybertot commented 4 years ago

The code is available now in https://github.com/ybertot/HighSchoolGeometry/tree/adding-ptolemy, pending review and integration in https://github.com/coq-community/HighSchoolGeometry

jmadiot commented 4 years ago

Thank you @ybertot and Tuan-Minh Pham for replying so quickly :)