Euclidean geometry in mathlib?

Stream: maths

[Donald Sebastian Leung]

I briefly skimmed through the algebraic_geometry and geometry sections of the mathlib documentation and found manifolds, presheaves and a few other things. However, just out of interest, is there geometry in mathlib in the Euclidean sense?

[Kevin Buzzard]

A student of mine @Ali Sever formalised a lot of synthetic geometry a la Tarski but if I recall correctly they never documented any of it so it might be completely unusable

[Donald Sebastian Leung]

Interesting - so it's done before (as I pretty much expected) but not yet in mathlib?

[Kevin Buzzard]

I don't think the code is mathlib-ready. I'll post a link when I get to a computer

[Bryan Gin-ge Chen]

See also these two recent-ish threads on geometry: formalizing Hilbert's axioms for plane geometry, formalizing some theorems from Artin's "Geometric Algebra". Ali Sever's code is linked in the second one somewhere.

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/xena-UROP-2018/tree/master/src/Geometry