Euclidean Geometry

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

Hello everybody. I did the Natural number game exercises, as well as the lean-prover community tutorial exercises. I was wondering if there were some set of exercises similar to these for Euclidean geometry. I would like to do stuff like work with tangent circles or straightedge and compass constructions. If there aren't any exercises like these, then how much has been formalized and where could I find it?

Also, I'm not sure if this was the right place to post this, so feel free to tell me that this should go elsewhere or about some rule I am not aware of.

[Johan Commelin]

@Andre Hernandez-Espiet (Rutgers) Welcome! And yes this is the right place to post.

[Johan Commelin]

I'm not aware of a set of exercises per se. But @Vaibhav Karve has a repo with axiomatic geometry.
Mathlib also has Euclidean geometry, directly in affine spaces over $\R$. But no tangent circles yet.

[Johan Commelin]

Personally, I think that Euclidean geometry in mathlib isn't the best thing to get started with, if you have just completed NNG. Because it requires you to understand quite a lot of other stuff in mathlib.

[Kevin Buzzard]

This shouldn't be the case though, right? Surely it is in theory possible to make it so that we can eg state things like "circle theorems" (which my daughter has been learning at school -- stuff like "angle at centre equals twice angle at circumference") without knowing other stuff?

[Johan Commelin]

Well, to do that you basically need to take an axiomatic approach. It might be possible to do that in mathlib, and make the current approach in instance.
But even then, I think doing geometry formally is a lot trickier than with pen and paper.

[Johan Commelin]

A lot more so than algebra etc

[Super Veridical]

looking at what's been done in the GeoCoq project ( https://geocoq.github.io/GeoCoq/ ) might me useful.

[Patrick Massot]

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

[Julian Berman]

There's also some incidence geometry problems on Codewars: https://www.codewars.com/collections/incidence-geometry

[Joseph Myers]

Kevin Buzzard said:

This shouldn't be the case though, right? Surely it is in theory possible to make it so that we can eg state things like "circle theorems" (which my daughter has been learning at school -- stuff like "angle at centre equals twice angle at circumference") without knowing other stuff?

The angle we have defined is from 0 to pi. "angle at centre" is from 0 to 2pi, so talking about it requires some way of saying which side of the angle you want to measure, and then building up a whole API for manipulating angles like that where a specific side of the angle is given. Or if you treat that statement as one about directed angles (a directed angle mod 2pi equals twice one mod pi, which might not be convenient to express if those are different types) you need to work out how to express directed angles (as reals, or as reals mod something, or as some other types that can be converted to reals such as the group of direct isometries in two dimensions quotiented by translations?) and in any case you need to define orientations of vector spaces before a directed angle can be converted to a real number (and may well need more API to handle moving between a two-dimensional subspace and that same subspace treated as a Euclidean affine space itself).

Effectively geometry is at the point where what's needed is maybe 10000 lines more of definitions and associated API (including linking to other parts of mathlib, e.g. to measure theory when talking about areas and volumes), before people can reasonably just prove theorems using the API provided. And this API setup all involves non-mathematical questions about the right way to set things up to be convenient for formalization and properly integrated into mathlib as a whole, so making it a lot trickier for beginners than simply proving theorems using definitions and API that are already provided. (Although most of the proofs involved in the API setup ought to be pretty simple.) And even once the API is done, there will be lots of issues about betweenness (ordering of points on lines, ordering of points round circles, which side of an angle you're looking at) which people don't generally think about at all for informal geometrical proofs.

[Joseph Myers]

If you just want it to be easier to talk about things that are already defined without needing to refer to other parts of mathlib, we could indeed define e.g. line as a bundled one-dimensional affine subspace and then e.g. ways other than affine_span to talk about the line through two points, an explicit notion of parallel rather than saying the directions of two subspaces are equal, and so on. We may well want to do that to allow more literal statements of geometry problems, but I'm not sure that API would be more convenient to use (e.g. using affine_span for a line through two points defers any proof obligation that those two points are different, but if you have something that returns a bundled line, you have to prove the points are different before you can talk about the line between them at all).