Euclid's Elements

Stream: new members

[Jiekai]

Hello, I'm digging the old lean docs and find this

- Impact on education.
  - We want to have a "live" and formalized version of Euclid's Elements (book 1).

I'm wondering if there are some lean examples on plane geometry.

[Patrick Massot]

This has been discussed many times, you can use the Search bar on top. For instance https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/formalizing.20Hilbert's.20axioms.20for.20plane.20geometry