Euclidean Geometry seems like missing a lot of stuff?

Stream: new members

[Something Something]

I'm confused that it's missing a lot of more fundamental stuff (like incircles, excircles, and even a lot of properties of cyclic quadrailterals). I'm looking through old conversations in zulip and it seems that their was also stuff like Ceva's in mathlib 3 so i'm guessing that maybe no one has bothered to port?

Are you guys trying to go for a maximally general approach before working things back down into specific cases in stuff like 2D?

[Ruben Van de Velde]

If it was landed into mathlib 3, it was ported

[Ruben Van de Velde]

I think it's been a combination of not the most interest in Euclidean geometry and it not being particularly easy to formalize. There's a bunch of more "advanced" geometry, though, I believe

[Something Something]

Oh I see. I'm noticing most of the stuff deals in affine geometry because that's the more general term?
Is Euclidean geometry hard to formalize because we don't have a good basis for converting it into a nice form that lean can handle?

[Joseph Myers]

Mathlib is a highly integrated, general library of mathematics as a whole. This affects the approach for Euclidean geometry just like anything else.

[Joseph Myers]

You mentioned incircles and excircles. Yes, those should be defined for a simplex in n dimensions rather than just in two dimensions, and for an arbitrary choice of signs for which faces of the simplex the sphere is on which side of rather than just "all positive signs" (insphere) or "all positive except one negative" (exsphere) - though note that in general, in 3 or more dimensions, not all $2^n$ generalised exspheres necessarily exist (if the appropriately signed sum of the reciprocals of the distances of each vertex to the opposite face is zero, there is no corresponding exsphere for that choice of signs - but the exsphere opposite a vertex always exists, that sum is always positive).

[Joseph Myers]

When defining inspheres and exspheres, of course you want to prove basic things such as "incentre is intersection of the internal angle bisectors". So you need to define which is the internal and which is the external angle bisector (preferably in a context that works for trisectors etc. as well - multiplying angles by any rational not just 1/2 - since there are legitimate geometrical theorems about trisectors as well). That gets into defining a consistent collection of orientations of all the facial planes of a simplex. (Note that in a triangle, such orientations correspond to arrows going round the triangle - not to two arrows going out from a vertex. Reflecting in the bisector maps the orientation of one face to the negative of the orientation of another face.) So then it gets into setting up API for relating orientations of a space to orientations of subspaces thereof. There's nothing particularly hard about that, but it's somewhat abstract, and not very closely related to what people think about in informal geometry. Needing to set up lots of abstract API that's not very immediately related to the concepts you started out being interested in is pretty common in working on mathlib.

[Joseph Myers]

When adding things to mathlib, it helps to have a particular combination of skills and motivation that means you like getting into those long chains of abstract dependencies involved in setting up API in appropriately general form. I'm an open source infrastructuralist. Lots of people working on geometry in Lean may have had different motivations, more conducive to having things (often more oriented to geometry as an axiomatic game rather than fully integrated into concepts such as inner product spaces and affine spaces) in separate repositories rather than designing things in a mathlib-friendly way and going through the mathlib review process to get everything fully integrated in mathlib. Getting things in mathlib is also much easier if you contribute as much as possible in little pieces as you go along, rather than trying to get something publishable done in a separate repository first, which is then a huge backlog of things to contribute that might need major reworks based on review comments. But if you're hoping to publish a paper on your work, then putting everything in mathlib in little pieces as you go along means you never have a well-defined single object (like your own repository) that you can point to in the paper as "this is the work I did on this project".

[Joseph Myers]

So I don't agree with suggestions that Euclidean geometry is somehow harder to formalize than other areas of mathematics. The shortage in mathlib may relate to the intersection of interest in formalization of Euclidean geometry with the time, inclination and skills for building up general infrastructure in mathlib, but not to any intrinsic difficulty of formalization.

[Joseph Myers]

I might well formalize another IMO geometry problem or two at some point (and thus whatever geometry API is missing at that point and relevant to that problem), but my current formalization priority is getting back to aperiodic monotile formalization.

[Joseph Myers]

As this is in the new members channel, I should add: new Lean users are fully able and welcome to contribute to geometry API in mathlib. My 5th mathlib3 commit was defining torsors in order to set up geometry, my 8th was defining Euclidean spaces, and my 10th was defining angles in such spaces.

[Something Something]

Correct me if I'm wrong but does the main issue boil down to we have Euclidean spaces but not objects relative to other objects in that space?

Also I think probably another reason it's underdeveloped is a lot of people probably aren't too interested in Euclidean geometry in general (I would argue the majority of people who are actually interested in it are just people doing competitive math) so it's kind of a small overlap in interest and ability

[Eric Wieser]

I have a development of insphere somewhere, but I think to be of any use it needs something about the hausdorffMeasure of a triangle!

[Something Something]

(in reply to upwards IMO problem formalization)
This is almost certainly not a good way to do things overall but I'm pretty sure you can formalize basically every IMO problem with Cartesian or polar or barycentric coordinates

[Joseph Myers]

Something Something said:

Correct me if I'm wrong but does the main issue boil down to we have Euclidean spaces but not objects relative to other objects in that space?

I wouldn't say there's a "main issue", rather that there are lots of separate concepts, with fairly weak dependencies between them, that need adding, with enough API in every case to be able to use the definitions in practice. It took me 200 PRs to get to one IMO geometry formalization. With 200 more PRs building on that we might have lots more basic geometry API ready to use. On the other hand, if you're only ready to do 10 PRs not 200 you probably won't make much progress towards filling the gaps.

[Joseph Myers]

Eric Wieser said:

I have a development of insphere somewhere, but I think to be of any use it needs something about the hausdorffMeasure of a triangle!

As usual, the difficulty isn't providing a definition that's mathematically correct, it's providing enough API linking to other things to make that API useful in the ways that inspheres get used in practice in geometry problems. Which almost certainly gets into defining several different but closely related concepts around angle bisectors, trisectors etc., and building up API for all those concepts (bisectors in n dimensions and in 2 dimensions; oriented and unoriented; between oriented lines and between vectors (an orientation of a 1-dimensional subspace, as we define it, is dual to an equivalence class of vectors in that subspace up to multiplication by positive constants; closely related, but not the same thing); and so on).

You can definitely avoid measure theory though. The reciprocals of heights of vertices above opposite faces are proportional to the volumes of those faces, so just as good for defining an insphere/exsphere, but without the measure theory dependency.

Now, when I thought about defining inspheres / exspheres a while back, a natural question was: how do we prove that the exsphere opposite a vertex always exists, which is one of many basic API lemmas to provide with the definition? And there is indeed an intuitive argument based on measures (consider orthogonal projections, onto the subspace of one face, of all the other faces; the fact that those projections cover the face in the subspace projected onto implies that the sum of volumes exceeds the volume of that face, so the signed sum of weights is nonzero and the corresponding affine combination giving the excentre is well-defined). But I suspect that argument would be a pain to formalize in terms of measures anyway; it would become a lot simpler once you translate it into an equivalent argument based on reciprocals of heights, even though the motivating intuition is one based on measures.

Of course we do want proper links between geometry and measure theory as well - especially since geometry involves volumes of more than just simplexes. (Anyone working on such links might set themself a target of formalizing solutions to IMO 2006 P6 and IMO 2016 P3 - both of which require significant extra API around the concept of "convex polygon" just to state the problem, not just areas.) But that's more or less independent of inspheres. (Inspheres are more closely related to bisectors, as discussed above, and tangency. Tangency at least is something where the API should be pretty straightforward to set up, and prove basic results up to and including the alternate segment theorem.)

[Something Something]

To be honest I probably don't have the ability to work on this just because generalizing stuff into higher dimensions isn't really my thing... It's also just a very broad topic in general.
Also I've been reading through old messages and trying to understand... is your oriented angles basically like Evan Chen's directed angles? If it is that's a lot of stuff that my brain can get around now
Tbh, I'm thinking through the steps to get something remotely useful and it hurts my head lol

[Something Something]

(deleted)

[Joseph Myers]

Oriented / directed angles in mathlib are mod 2π rather than mod π, since lots of results are valid mod 2π and being able to reason mod 2π is important when you want to prove configuration information. Maybe at some point we'll want an explicit type for angles mod π as well, though that would mean duplicating a lot of API.