2 ms·
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 i
by lordnacho 7y ago
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 7y agoQuick 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/ http://geocoq.github.io/GeoCoq/