Does Lean allow you to put in geometric proofs? Say someone draws some circles a... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		lordnacho on April 6, 2020 \| parent \| context \| favorite \| on: Doing a math assignment with the Lean theorem prov... Does Lean allow you to put in geometric proofs? Say someone draws some circles and some lines and wants to prove that some property of the intersection points is true, eg that are always on the same straight line?

h91wka on April 6, 2020 [–]

Quick search reveals that some people have encoded Euclid's axioms in Coq (Lean and Coq are based on roughly the same theory):

http://geocoq.github.io/GeoCoq/

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact