FrederickPu
FrederickPu
I have a branch where I ported to use the smt tactic directly with the euclid axioms. Which involves generating a proof certificate so this issue no longer occurs https://github.com/project-numina/LeanEuclid/tree/to415
Hi, for mathlib I remember that they wanted me to create a PR from a branch, in which case I would need to be given some sort of permission. In...
alright thanks!
The proofs in Book/Prop01 are failing cause euclid_apply can't solve the goals. I also noticed that some of the latest commits are failing the ci process. Is this just an...
It's failing on this theorem ```lean4 theorem proposition_1 : ∀ (a b : Point) (AB : Line), distinctPointsOnLine a b AB → ∃ c : Point, |(c─a)| = |(a─b)| ∧...
somehow it's not picking up on symmetry of equality or something
sorry, I just got a new computer after the old one bricked. I'm trying to setup the repo again i cant seem to find `Server Env Paths` in the settings...
@Suya1671 have you been able to resolve this yet?