Euclidean geometry

Stream: general

[Huỳnh Trần Khanh]

do we have a usable model of Euclidean geometry in Lean? I guess not, because Euclidean geometry is so complex...

[Huỳnh Trần Khanh]

like... it's taught in schools because it feels somewhat intuitive and details can be handwaved in informal proofs... but in reality Euclidean geometry is extremely complex...

[Eric Wieser]

Before declaring that something is too hard for mathlib to have, I recommend you first google whether we have it. https://leanprover-community.github.io/mathlib-overview.html has a section on euclidean geometry.

[Eric Wieser]

Now, there are plenty of bits of geometry that we don't have yet, such as signed angles - but if you have something specific in mind, it would help if you said what it was!

[Huỳnh Trần Khanh]

oh lol sorry :neutral: hmm I have nothing specific in mind yet but... is it possible for a high school student like me to help expand the Euclidean geometry section of mathlib to make it possible to formalize high school geometry problems? or is the current formalization too general for me to understand? again, I'm not a mathematician, just an average math-literate high school student lol

[Huỳnh Trần Khanh]

it'd probably take me a while to understand the existing code base... but I want to be sure that this is something that I could probably do rather than something that is out of reach for me (because of my lack of a math background)

[Johan Commelin]

I think that in principal it is possible, but you would still have to learn the language. If you are looking for a self-contained project, I would suggest picking your favourite IMO problem, and formalizing a solution. (See archive/imo for examples.)

[Kevin Buzzard]

If we can't yet prove angle at centre is twice angle at circumference then I think IMO problems might be pushing it a bit :-) I think that a development of a bunch of results with underlying space equal to a torsor for the complexes should be accessible and fun

[Johan Commelin]

Ooh, I didn't mean IMO geometry problems. I should have been more clear. I think IMO problems in number theory might be easier to get started with.