3 ms·
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/
by h91wka 7y ago
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/ http://geocoq.github.io/GeoCoq/