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 lordnacho on Monday April 06, 2020 @03:01AM (#22791448)
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?
[ Parent | on HN ]
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 ]