LeanEuclid
LeanEuclid copied to clipboard
loganrjmurphy
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Right now System E is formulated as a bunch of axioms. However, I believe it would more sensible for it to be formulated as a type class such as Group....
Hello! I'm very interested in your work and have recently been trying to reproduce your experiments. However, when I run lake build, a lot of errors appear in the command...
Here the SMT solver called by `euclid_finish` is bypassing the termination check. @loganrjmurphy Any idea on how this can be fixed? I'm thinking about either preventing `euclid_apply` from using the...
Hi @loganrjmurphy, I'm trying to bump the repo to Lean v4.19.0 (the [v4.19.0](https://github.com/loganrjmurphy/LeanEuclid/tree/v4.19.0) branch). I've already bumped its dependency https://github.com/ufmg-smite/lean-smt and the SystemE module in this repo. But I still...
I have noticed that some axioms are either not corresponding to Avigad's paper or plainly wrong. For example, ``` axiom intersection_circles : ∀ (α β : Circle), α.intersectsCircle β →...
Metadata
Owner
Metadata
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.