## Stream: maths

### Topic: Euclidean geometry in mathlib?

#### Donald Sebastian Leung (Mar 01 2020 at 06:20):

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 (Mar 01 2020 at 07:41):

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 (Mar 01 2020 at 07:42):

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

#### Kevin Buzzard (Mar 01 2020 at 07:42):

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

#### Bryan Gin-ge Chen (Mar 01 2020 at 07:43):

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 (Mar 01 2020 at 07:48):

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

Last updated: May 18 2021 at 08:14 UTC