Zulip Chat Archive

Stream: maths

Topic: Euclidean geometry in mathlib?


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

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

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

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

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

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