Donald Sebastian Leung (Mar 01 2020 at 06:20):
I briefly skimmed through the
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):
Last updated: May 18 2021 at 08:14 UTC