Zulip Chat Archive

Stream: new members

Topic: Euclid's Elements


view this post on Zulip 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.

view this post on Zulip 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: May 14 2021 at 00:42 UTC