News for hackers. Stuff that matters.

A comment on Doing a math assignment with the Lean theorem prover. Parent comment

Re:Doing a math assignment with the Lean theorem prover by h91wka on Monday April 06, 2020 @11:15AM (#22794456)
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/

[ Parent | on HN ]

There are no comments on this comment yet.