IMO Geometry

Stream: Machine Learning for Theorem Proving

[Hanting Zhang]

I worked on the Olympiad-formalization repository for a few months back in August to January and stopped for the past three months. Now I want to get back into it and I am thinking about the idea of formalizing as much as I can about Olympiad geometry in Lean. The reasons why are straightforward:

1. As far as I am aware, there is a dire lack of geometry problems in the repo right now, due to the fact that it has been very difficult to express some (or maybe even most) geometric concepts concisely in Lean. (Maybe this has changed?)

2. I am looking for something to do over the summer and this feels like a nice project to start. I am also just very interested in the work being done with AI and ITPs so far and want to contribute.

The plan is to work off the Art of Problem Solving "Introduction to Geometry" book. This is just the default choice, and it might change if more challenging books are better suited for formalizing IMO level problems. A nice goal to set would be to formalize a few interesting examples of IMO geometry problems that use extensive triangle/circle theorems concisely. (Does this already exist?) Any suggestions or advice about this idea are also welcome! (cc: @Stanislas Polu I suppose)

[Daniel Selsam]

Hanting Zhang said:

I worked on the Olympiad-formalization repository for a few months back in August to January and stopped for the past three months. Now I want to get back into it and I am thinking about the idea of formalizing as much as I can about Olympiad geometry in Lean. The reasons why are straightforward:

1. As far as I am aware, there is a dire lack of geometry problems in the repo right now, due to the fact that it has been very difficult to express some (or maybe even most) geometric concepts concisely in Lean. (Maybe this has changed?)

2. I am looking for something to do over the summer and this feels like a nice project to start. I am also just very interested in the work being done with AI and ITPs so far and want to contribute.

The plan is to work off the Art of Problem Solving "Introduction to Geometry" book. This is just the default choice, and it might change if more challenging books are better suited for formalizing IMO level problems. A nice goal to set would be to formalize a few interesting examples of IMO geometry problems that use extensive triangle/circle theorems concisely. (Does this already exist?) Any suggestions or advice about this idea are also welcome! (cc: Stanislas Polu I suppose)

Hi Hanting! I recommend you sync with @Joseph Myers -- he has added some basic euclidean geometry to mathlib (@ https://github.com/leanprover-community/mathlib/tree/master/src/geometry/euclidean)

[Stanislas Polu]

Hi Hanting! I think it's an interesting project to attempt to solve progressively difficult geometry problems. Any exercise in that book that you can formalize with @Joseph Myers 's work as a starting point?

[Joseph Myers]

I think we're still at the stage where you should expect to add thousands of lines of API to mathlib proper for any geometry problem you want to formalize (and, thus, should expect to do a very large number of PRs along the way, whenever you find something that could go in mathlib; simply adding oriented angles took 50 PRs). Having a particular problem in mind may help guide you in what API you want to formalize along the way, but the main work will still be adding that API not formalizing the solution to that particular problem. And all that API should be added in properly general form rather than just what you need for that lemma (though in some cases there may be subjective judgement about just how general you want to go, when you're dealing with API for something five levels of dependencies down from the problem you're actually aiming for). That includes both defining and proving things in appropriate generality (not restricting things to the plane case unnecessarily, for example), and making sure that, when you add definitions, you add all the associated trivial lemmas that you can think of that may come up when using that API but are too trivial to state in textbooks. (In practice, as you use the API you'll then find more missing pieces you need to add.)

[Joseph Myers]

Example 1: most IMO geometry problems state betweenness conditions. So you need to define betweenness, both strict and weak, in an affine space over an ordered ring (for example - once the affine space and convexity refactors are done, it would be over an ordered semiring), prove loads of trivial lemmas (such as those found in Tarski's axioms for geometry, but not limited to those), link it to convexity as far as possible in the absence of those refactors, and then link to geometrical properties such "angle = pi". And that's just API setup to be able to state the problems.

[Joseph Myers]

Example 2: say you want to use congruent triangle lemmas, such as SSS congruence. Don't prove something specific to triangles, prove an appropriate result for possibly infinite indexed families of points in possibly infinite-dimensional Euclidean affine spaces. (The pairwise distances in an indexed family of points uniquely determine which combinations of points with sum of weights 0 are the 0 vector, and thus the dimension of the affine span of the points; if that span is finite-dimensional, and there is an isometric equivalence between the two spaces, there is one that maps points in one family to corresponding points in the other, which serves as a definition of congruence for indexed families of points.)

[Joseph Myers]

Example 3: many IMO geometry problems involve the incenter of a triangle in either the problem or the solution. That concept makes sense for a simplex, so should be defined for a simplex not just a triangle, just as circumcenter is defined for a simplex. But then you want to state "incenter equals intersection of angle bisectors", and the angle bisectors are those of angles between faces of the simplex. So you get into wanting to talk about oriented angles between oriented subspaces in order to distinguish the two bisectors, which can involve talking about orientations of at least three subspaces at the same time. That's probably going to involve lots of API (with very little mathematical content) for manipulating orientations of subspaces, before you then specialize things to the two-dimensional case after developing the API in n dimensions.

[Joseph Myers]

Example 4: some IMO geometry problems involve angles, and those are unoriented angles, but for a formal proof it's probably more convenient to use oriented angles. To use oriented angles to prove something involving unoriented angles, I expect you'll need lots of lemmas relating the two, and in particular lemmas of the form "these two angles have the same orientation". My inclination is the right way to prove "same orientation" lemmas is via continuity: the function from an oriented angle to its sign is constant away from 0 and pi, and the function from two vectors or three points to the corresponding oriented or unoriented angle is continuous when the vectors aren't 0 / no two points are equal, and once you've proved those things you can use existing API for continuity in mathlib to deduce that the function from two vectors / three points to the sign of the corresponding angle is constant on appropriate subsets of V × V or P × P × P where the oriented angles don't go through 0 or pi.

[Joseph Myers]

Example 5: I suspect lots of things involving circles would be simpler with a bundled sphere type (a structure bundling center and radius) to help with talking about points lying in a circle, tangency, power of a point, radical subspace, etc. - which itself needs lots of API, and involves the non-mathematical design question of whether you also bundle a hypothesis that the radius is positive or nonnegative or just pass appropriate hypotheses like that to lemmas that need it.

[Joseph Myers]

I don't think there's any sort of fundamental obstacle to formalizing geometrical proofs - it's simply there's a lot to define first before you actually get onto the sort of proofs involved in IMO geometry problems. (Other examples that could be given of missing API include e.g. cyclic polygons - ordering of points on a circle - and linking into the measure theory parts of the library for anything involving talking about areas / volumes.)

[Joseph Myers]

And the need to set up a lot of API is not of course at all unique to geometry.

[Kevin Buzzard]

This should probably become an issue or even better a project

[Hanting Zhang]

That's what I'm saying :rolling_on_the_floor_laughing:

[Hanting Zhang]

@Joseph Myers Sorry for the slow response, you wrote a lot of interesting information that I would've never thought of, so thank you for doing that :upside_down:

For betweenness, could you elaborate on why this would be difficult? I am thinking that the canonical definition would be something like "z is on the segment (2-simplex) xy." Then Tarski's axioms would follow pretty easily. (Unless we want to do it the "axiomatic way" where we formulate everything from Tarski's axioms and then show that mathlib's concept of euclidean spaces is an instance of such a geometry. In my head this is the "opposite way" to do things and am I wondering if this is a serious consideration at all -- I also just realized that we would only be modeling plane geometry with Tarski's axiom, so nevermind.) I am not very aware of current convexity/ring things going on in mathlib, so are these refactors actually important in doing geometry? Or is it more like the technical lean/cs details that need to be dealt with?

This is sort of the idea I was expecting for congruence, so your agreement on this is great motivation. One question I am interested in is the analogous deal with similarity. We would actually want to define similar transformations (which maybe already exists?) in affine spaces, and then define similarity for (arbitrary?) sets of points as the most general starting point, right? Then limit that down to all the other stuff we need. This also seems straightforward but requires lots of API.

You've clearly thought way more about these things than I did; I was not thinking that defining higher dimensional triangle centers would be that difficult, but reading your thoughts I agree that orientations will become a mess. ...I suspect should be a general way to deal with orientations. If this is possible then it should be straightforward on how to proceed. The details of converting general theorems down to the specific 2/3 dimensional cases might be messy, though. But I'd love to hear more about what ideas you have for this!

Could you clarify what you mean by needing to prove "same orientation" lemmas via continuity? I kind of understand what you mean but the details are going over my head.

I feel like circles themselves are not that complicated; in your example, for example, I would probably choose to use take the radius in the reals and have a coe from the sphere structure to the set of its realization; then S would be the empty set when r < 0 and statements like x in S would be degenerate. This is just the very bottom layer, though. Things like power of a point and tangency probably need their own separate consideration.

As you mentioned there is basically nothing about volumes right now in mathlib; all the measure-theoretic infrastructure exists, though, which is cool. Do you have any thoughts on what's needed for volume API? Or will it be relatively straightforward? I personally don't have a good feel for measure theory, so I am wondering how one would glue the current API with the geometric structures we define in a nice generalizable way...

Yeah if I had to say I would probably start working on similarity towards congruences with the goal of stating the SSS-SAS-ASA congruence theorems. Or, do you have anything incomplete that you think would be a nice place to start?

[Joseph Myers]

Some things such as betweenness and spheres aren't difficult, it's simply that you need to set up at least hundreds of lines of API (mostly too trivial to appear in textbooks) before you can do anything much useful with them. For betweenness, you probably need API for both strict and weak betweenness as both are relevant in geometry in practice (even if axiomatic geometry tends to use just one version). There's also the notion of an affine subspace being between two points, or a point being between a point and an affine subspace (e.g. two points being on opposite sides / same side of a line), though that can probably wait until later.

[Joseph Myers]

The idea of the proposed convexity / affine spaces refactor is as follows. You can define affine combinations with nonnegative coefficients summing to 1, and thus convexity (of which betweenness is a special case) in two different contexts: for a semimodule over an ordered semiring, or for an affine space for a module over an ordered ring. In the case where you have a module over an ordered ring, which can be considered as an affine space over itself, the resulting two definitions of affine combinations are equal, but not defeq. So the proposed refactor would be to define abstract affine combination spaces, and then there would be a type class to assert that a type that is both an add_torsor for a module and also an abstract affine combination space has equal affine combinations from the two definitions. And then you can have a single definition of convexity and betweenness for such abstract affine combination spaces, which applies to both the semimodule and the add_torsor cases.

I think it's reasonable to define betweenness for affine spaces (i.e., add_torsors for modules over an ordered ring) without waiting for that refactor, but it might best be done in a way that facilitates such a refactor in future (for example, making definitions irreducible to avoid too much reliance on defeq for the definitions).

[Joseph Myers]

For congruence and similarity (definitions that apply in arbitrary metric spaces, not just in a linear or affine context): we have the unbundled isometry proposition, and bundled types for isometric equivalences, and linear and affine isometries and isometric equivalences. I think we still need to apply the morphism refactor to these type classes (i.e. have type classes for types of isometries or isometric equivalences, so that a single lemma can apply to multiple kinds of bundled isometries). Once that's done, there should probably be a corresponding collection of unbundled propositions, bundled morphisms and type classes for them, for the case of similarities (so at least five bundled types of similarities as well as whatever type classes) - I don't know whether a similarity with scale factor 0 should be allowed by those types etc. or not. Note that then e.g. the lemma that a similarity is a continuous function would only need proving for the unbundled propositions and for the most general type class of similarities - using type classes as in the morphism refactor should remove most of the need for separate affine_isometry.continuous, affine_isometry_equiv.continuous etc. lemmas for each of the many such bundled types.

[Joseph Myers]

For proving "same orientation" lemmas for angles via continuity: a typical such lemma might be of the form: the angle between vectors x and y has the same orientation as that between x and a • x + b • y, for any positive b; I expect lots of lemmas like that will be needed for when you want to move between oriented and unoriented angles in a proof. While you no doubt could prove that with some ad hoc argument about complex.arg, I don't think that's the right (clean, general) approach for mathlib. All that's actually needed is that a • x + b • y is a continuous function of (a, b) (should follow from composition of existing continuity lemmas in mathlib), that angles are continuous functions of the vectors involved as long as those vectors are nonzero (not currently in mathlib, should be added, should be straightforward to prove), and that if the angle between x and y isn't 0 or pi, neither is that between x and a • x + b • y (what you first need to add there is an iff condition for twice the oriented angle between two vectors to be 0, I think). And given those continuity properties, the "same orientation" lemma then follows, without any special argument about arg being needed at all.

[Joseph Myers]

I don't know what API will be needed for volumes in geometry (beyond having some way to talk about convex hulls in affine spaces so we can take their measure - see the convexity refactor discussion above). Once there's a way of referring to the convex hull of the vertices of a simplex, you also need to define a measure on a Euclidean affine space in terms of what we have for measures in vector spaces. And then a good test would be whether you can prove that the volume of a simplex is 1/n * volume of base * height. (You may also need API here to move conveniently between the full space and subspaces, since the volume of the base is a (n-1)-dimensional measure in a subspace.)

Note that once we have a proper link to the measure theory library, archive/100-theorems-list/57_herons_formula.lean ought to have its result restated to refer to measures rather than an ad hoc expression involving angles, and be moved from the mathlib archive to mathlib proper (statements about areas in relation to angles belong in mathlib proper as well). 9_area_of_a_circle.lean really also belongs in mathlib proper in more general form (we have the gamma function now, so could state the volume of a sphere in n dimensions using the gamma function, though two-dimensional and three-dimensional special cases seem appropriate as well).

[Joseph Myers]

For SSS congruence in the general form I described above, inner_weighted_vsub and dist_affine_combination should be a reasonable basis for proving the key fact that all affine dependencies between an indexed family of points are determined by the pairwise distances between those points.

[Hanting Zhang]

Hi again, thank you for all the input!

[Hanting Zhang]

Joseph Myers said:

For congruence and similarity (definitions that apply in arbitrary metric spaces, not just in a linear or affine context): we have the unbundled isometry proposition, and bundled types for isometric equivalences, and linear and affine isometries and isometric equivalences. I think we still need to apply the morphism refactor to these type classes (i.e. have type classes for types of isometries or isometric equivalences, so that a single lemma can apply to multiple kinds of bundled isometries). Once that's done, there should probably be a corresponding collection of unbundled propositions, bundled morphisms and type classes for them, for the case of similarities (so at least five bundled types of similarities as well as whatever type classes) - I don't know whether a similarity with scale factor 0 should be allowed by those types etc. or not. Note that then e.g. the lemma that a similarity is a continuous function would only need proving for the unbundled propositions and for the most general type class of similarities - using type classes as in the morphism refactor should remove most of the need for separate affine_isometry.continuous, affine_isometry_equiv.continuous etc. lemmas for each of the many such bundled types.

I was wondering for this comment, what did you mean by "type classes for types of isometries or isometric equivalences, so that a single lemma can apply to multiple kinds of bundled isometries"? Does that mean adding some common type class like [is_isometry f] for maps? I'm having a hard time understanding how this would be concretely done to allow a single lemma to apply across all 5 different isometries.

And to be clear, by "five bundled types of similarities as well as whatever type classes," you mean the natural ones you get from generalizing what is done for isometries, correct?

[Hanting Zhang]

By any chance would you also know of any good references for developing general affine Euclidean geometry? I'm currently looking at Geometry I by Marcel Berger, but it feels too dense for me

[Joseph Myers]

Hanting Zhang said:

I was wondering for this comment, what did you mean by "type classes for types of isometries or isometric equivalences, so that a single lemma can apply to multiple kinds of bundled isometries"? Does that mean adding some common type class like [is_isometry f] for maps? I'm having a hard time understanding how this would be concretely done to allow a single lemma to apply across all 5 different isometries.

And to be clear, by "five bundled types of similarities as well as whatever type classes," you mean the natural ones you get from generalizing what is done for isometries, correct?

It would be {F : Type*} [isometry_class F A B] (f : F) for isometries from A to B (and likewise with isometry_equiv_class). See the doc strings for data.fun_like.basic for more explanation of the morphism type class pattern.

Yes, generalize the types and type classes from isometries to similarities (most lemmas will then be true for similarities, not just for isometries).

[Hanting Zhang]

Thanks, I've started working on this!

[Hanting Zhang]

And if you don't mind another few questions... :sweat_smile:

Was there any particular reason you didn't start by defining add_subtorsor and then extending that to affine_subspace? There's also stuff like multiplicative torsors and quotients that can be done too. Was it just a high effort to immediate usefulness ratio that turned you away from the trouble or was there something deeper that stopped you?

[Hanting Zhang]

This is what I have started with quotients, I would love to hear what you think about these definitions, if you don't mind!

import algebra.add_torsor
import group_theory.quotient_group

open_locale pointwise
section subtorsor

variables {G : Type*} (P : Type*) [add_group G] [T : add_torsor G P]
include T

structure add_subtorsor :=
(carrier : set P)
(vsub_vadd_mem : ∀ {p1 p2 p3 : P}, p1 ∈ carrier → p2 ∈ carrier → p3 ∈ carrier →
  (p1 -ᵥ p2 : G) +ᵥ p3 ∈ carrier)

end subtorsor

namespace subgroup
variables {G : Type*} {P : Type*} [add_group G]

def to_add_subtorsor (p : add_subgroup G) : add_subtorsor G :=
{ carrier := p,
  vsub_vadd_mem := λ p1 p2 p3 h1 h2 h3, p.add_mem (p.sub_mem h1 h2) h3 }

end subgroup

namespace add_subtorsor

variables {G : Type*} (P : Type*) [add_group G] [T : add_torsor G P]
include T

instance : set_like (add_subtorsor P) P :=
{ coe := carrier,
  coe_injective' := λ x y h, by { cases x; cases y; congr, exact h, } }

variables {P}

-- not sure what this is supposed to be called
def direction (t : add_subtorsor P) : add_subgroup G := add_subgroup.closure ((t : set P) -ᵥ t)

end add_subtorsor

namespace subtorsor
variables {G : Type*} {P : Type*} [add_group G] [T : add_torsor G P]
include T

def rel (t : add_subtorsor P) : setoid P :=
{ r := λ x y, y -ᵥ x ∈ t.direction,
  iseqv := mk_equivalence (λ x y, y -ᵥ x ∈ t.direction)
    (λ x, by { rw vsub_self, exact zero_mem t.direction, })
    (λ x y h, by { rwa [← neg_vsub_eq_vsub_rev, neg_mem_iff], })
    (λ x y z hxy hyz, by { rw ← vsub_add_vsub_cancel z y x, exact add_subgroup.add_mem _ hyz hxy, }) }

def quotient (t : add_subtorsor P) := quotient (rel t)

instance : has_quotient P (add_subtorsor P) :=
{ quotient' := quotient }

-- proof omitted
instance (t : add_subtorsor P) [ht : t.direction.normal]  : add_torsor (G ⧸ t.direction) (P ⧸ t) := sorry

end subtorsor

[Hanting Zhang]

(cc @Joseph Myers )

[Joseph Myers]

At the time I defined affine subspaces, we didn't have any way for the theory of one structure type to be applied to another structure type building on it, so add_subtorsor wouldn't have helped at all in setting up the theory of affine_subspace. This was long before the subobject type class pattern (#11545) was invented.

[Joseph Myers]

At the time I defined add_torsor, multiplicative groups didn't have div defined, and it was controversial whether it should be defined for multiplicative groups. Since many lemmas for add_torsor involve subtraction in the underlying additive group, that would have been a significant obstacle to setting up the theory of add_torsor via to_additive applied to a theory of torsor. Now that multiplicative groups do have div, it should be reasonable to set up multiplicative torsor and use to_additive to derive the theory of add_torsor.

[Hanting Zhang]

I see, thank you for the explanation!