Zulip Chat Archive

Stream: new members

Topic: Euclid's Elements


Jiekai (May 03 2020 at 09:40):

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 (May 03 2020 at 09:43):

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


Last updated: Dec 20 2023 at 11:08 UTC