5 ms·
This is a bit random, but there are some formal systems for Euclid's elements out there (see, for example https://arxiv.org/abs/0810.4315 https://arxiv.org/abs/
by meuk 7y ago
This is a bit random, but there are some formal systems for Euclid's elements out there (see, for example https://arxiv.org/abs/0810.4315 https://arxiv.org/abs/0810.4315).
I think it should be possible to implement this in a dependently typed language like Idris, but haven't really worked on this (yet). Any thoughts?
- ratmice 7y agoAlso see this: http://www.michaelbeeson.com/research/CheckEuclid/index.php http://www.michaelbeeson.com/research/CheckEuclid/index.php It seems a dependently typed language might be overkill, "The proofs described in this paper only need a rather weak logic. There are no function symbols", "only existential quantifiers; universal quantification over the free variables is left implicit." They wrote a translator then to convert the proofs to HOL, and Coq, you could presumably do the same for e.g. idris
- meuk 7y agoAwesome, this was exactly the type of comment I was hoping for!