geometry revisited

Stream: IMO-grand-challenge

[Daniel Selsam]

Dear channel, how is the geometry library coming along? Is it possible/expected that this abstract version will be able to serve as the basis for the IMO-GC? If not, we could try to bootstrap a library, e.g. using something like Groebner. At one point @Reid Barton suggested defining points in terms of complex numbers and trying to bootstrap using the complex bash. FYI:

• @Ryan Krueger @Jesse Michael Han and I pseudo-formalized ~150 olympiad-style statements last year in terms of a relatively simple DSL, which we describe in the appendix of https://arxiv.org/pdf/2012.02590.pdf
• https://link.springer.com/article/10.1023/A:1006171315513 lists a bunch of theorems in the appendix that are useful for a prover. They are for unordered geometry only, but those plus basic lemmas connecting fullAngle, angle, and oppSides already go pretty far

[Johan Commelin]

@Joseph Myers would be in the best position to answer this question, I think

[Joseph Myers]

A lot still needs to be done to be able to state most IMO geometry problems.

I think problem statements for the IMO Grand Challenge should always both (a) correspond very closely to the original English statement of the problem (with conventions to be determined for various details of the translation) and (b) be based on mathlib definitions that are fully linked into the relevant general theories, not on anything less general or specific to the IMO Grand Challenge (the only thing specific to the IMO Grand Challenge should be some way for a challenge input file to indicate to an AI competitor that "these are the types of which you must exhibit terms", everything else should be using normal, general mathlib definitions, though possibly stating problems in a way that would be unidiomatic for mathlib itself, e.g. using > when mathlib would use <, to achieve a more literal translation of the English version).

A typical geometry problem would postulate {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [finite_dimensional ℝ V] (hd2 : finrank ℝ V = 2) and then state things in terms of points in that P (but mathlib results that are specific to two-dimensional geometry should work for a two-dimensional subspace of a larger space, when that subspace contains all the points in question, they wouldn't require the overall space to be two-dimensional). It wouldn't refer to complex numbers, because those aren't in the IMO syllabus and so won't appear in the English problem statement; if you want to complex bash, you probably need to use appropriate results about the existence of isometries (e.g. complex.isometry_euclidean and fin_orthonormal_basis and whatever other glue is needed for the affine space case) and appropriate results (or new tactics) to allow transporting geometrical properties across isometries. Likewise, problems don't mention directed angles in English, so shouldn't in the formal statements; you can use them in your solutions if you want, but you need to formalize the translation between undirected and directed angles if you do so.

I'd encourage people interested in olympiad geometry in Lean to pick some problem or problems and take the longest path, not the shortest, to stating such problems and their solutions - working out the suitably general form of the required definitions and filling out all the relevant lemmas needed to make the underlying general API in mathlib conveniently usable, not taking any shortcuts involving less-general definitions and theories where a human could see that the two statements are equivalent but the statement doesn't correspond so literally to the original English one or where the definitions are less general than they should be. The one geometry problem I formalized isn't an IMO problem, but I made sure to put the underlying definitions and theory in mathlib in suitably general form (so defining the Monge point of a simplex, not just the orthocentre of a triangle, for example, and likewise to define the circumcentre and circumradius for a general simplex).

If the problem mentions one point being between two others, first complete Yury's work on convexity for affine spaces (see #2910), then define both strict and weak betweenness as properties of three points in terms of general convexity infrastructure and prove all the basic lemmas for those points (such as appear in e.g. Tarski's or Hilbert's axioms, as well as how betweenness relates to e.g. affine combinations and angles equal to pi); don't take the shortcut of using an angle equal to pi as how you state strict betweenness, because (a) that's not what the original problem says and (b) betweenness is meaningful for all real affine spaces, not just Euclidean ones where angles are defined, so it should be defined in that context. Likewise, use that general convexity infrastructure to define such things as points being (strictly or weakly) inside a simplex (problems will refer to the specific case of a triangle, but it's meaningful for a simplex so should be defined for that case).

If the problem refers to areas, link the geometry part of mathlib to the measure theory part, to define volumes in a way that makes sense for e.g. a simplex in some higher-dimensional space. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Hello!.20Have.20a.20proof.20of.20Heron's.20Area.20Formula!/near/232685801 for more discussion of that.

If the problem refers to cyclic quadrilaterals, see my comments on #7329 for the sort of thing needed to fill out the API for cyclic polygons properly.

If the problem refers to incentres, as many do, make sure to define the incentre for a general simplex (should be easy enough to define right now in terms of barycentric coordinates, and to prove relevant properties of it), in a way that gives both incentre and excentres (for an arbitrary vector of signs saying which side of each face the point should be on, for example), not just for a triangle. When relating it to angle bisectors, remember that the relevant bisectors aren't lines, they're hyperplanes (affine subspaces) bisecting the angle between two faces, so you'll need that concept of angles and angle bisectors, and only then relate it to the existing concepts of angles in the two-dimensional case.

[Joseph Myers]

Effectively, I think of the IMO Grand Challenge as involving "put the whole IMO syllabus in mathlib, in a suitably clean and general form linked into everything else" and "add tactics, e.g. for Gröbner bases, that are of more general use" just as much as "build up AI that can attempt IMO problems".

[Kevin Buzzard]

@Joseph Myers you seem to have some pretty clear ideas about what exactly is and isn't on the syllabus for the IMO (I know for example that continuity famously isn't on it, and have known for decades that there is "some sort of syllabus" but you are making far more precise statements). Is there some link to some document which spells out the details of the syllabus?

[Joseph Myers]

There's no written syllabus, but complex numbers and calculus are "well known" not to be on it (that is, problems shouldn't explicitly refer to complex numbers and calculus, and shouldn't depend on them). It's a bit ambiguous whether problems should mention graphs explicitly (see IMO 1991 Q4 for the one that did), but problems that are in fact graph theoretic (without mentioning graphs) are common. It's also a bit ambiguous whether solid geometry is on the syllabus (last clearly solid geometry problem was IMO 1979 Q4, I think), though combinatorial problems described in terms of three-dimensional space and without any real geometric aspects are certainly OK (e.g. IMO 2007 Q6). The Problem Selection Committee can push the boundaries and shortlist a problem where it's not clear it's on the syllabus (e.g. one depending on complex numbers for its solution), and see what the Jury thinks; when we put N7 on the 2019 shortlist, we weren't at all sure that the log function would be considered to be on the syllabus, but people didn't object to that in the end.

The 171 definitions and results in chapter 2 of the IMO Compendium are probably a reasonable checklist for filling out the IMO syllabus in mathlib (and see Evan Chen's book for more on the geometry side), although some would end up corresponding to many separate formal results and there must be many lemmas too trivial to state in such a list that are also needed for a properly usable API. But those 171 definitions and results include some things (e.g. calculus) that are definitely not on the IMO syllabus (but might still commonly be used by IMO students). Alternatively, formalizing statements and solutions of all problems from the past 40 years (without taking any shortcuts resulting in less literal problem statements) would probably cover the syllabus pretty well (limiting to the past 40 years avoids issues with both solid geometry and a few early problems that asked for geometrical constructions, presumably straightedge-and-compasses).

[Daniel Selsam]

@Joseph Myers Thank you for your thoughtful and thorough response!

[Daniel Selsam]

oriented angles now on master :tada: https://github.com/leanprover-community/mathlib/pull/12236 thanks @Joseph Myers

[Heather Macbeth]

I just posted in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/adding.20angles about a proposed redefinition of oriented angle, interested parties please comment!

[Joseph Myers]

And I have eight open PRs that are all working towards being able to state and prove IMO 2019 Q2 (plenty more will be needed on top of those PRs as well; parts still to be implemented, parts implemented but not PRed because of dependencies on open PRs): #16184 #16191 #16278 #16279 #16298 #16332 #16372 #16471. (#16278 might not look like a geometry PR; I'm using it to translate between index types with affine_independent_iff_linear_independent_vsub. Also, although there are no dependencies between those eight PRs, once one of #16191 and #16332 is merged the other will need updating, because the latter changes argument implicitness for a lemma used by the former.)

[Johan Commelin]

@Joseph Myers Thanks for reminding me about those 8 PRs. I'll try to look at them today.

[Michail Karatarakis]

(deleted)

[Joseph Myers]

I now have a full, sorry-free formalization of geometry problem IMO 2019 Q2. This uses API fully linked into the rest of mathlib as appropriate, no separate DSL needed, all nondegeneracy conditions not considered to be implicit in a literal translation of the problem to Lean having proofs fully formalized, translation between unoriented angles used in the statement and oriented angles used in the proof fully formalized.

This depends on all my 22 open PRs (which, if I've done things correctly, should all be independent of each other and able to be merged in any order). There will also be about 12 more PRs on top of that (with various dependencies on each other and subsets of the 22) to get to the IMO 2019 Q2 formalization.

So this formalization will have taken nearly 200 PRs (starting with defining orientations last year). Once all that API is in mathlib I hope future IMO geometry formalizations will take rather fewer PRs, but we're still some way from being able to expect that such a formalization doesn't need any extra API at all (indeed, a large proportion of such problems can't yet be stated because they need definitions we don't yet have).

[Johan Commelin]

Wow! Tremendous effort!

[Scott Morrison]

Fantastic. Could we see the statement and proof of Q2 here (ignoring all the imports and dependencies) just for a sneak preview?

[Joseph Myers]

This is what it currently looks like, minus the imports of local files with about 3000 lines of dependencies that aren't yet in mathlib (some parts PRed, some not yet PRed because of dependencies not yet in mathlib; the largest single piece is #17683). Note (a) the module doc string discussing the conventions followed to translate the informal statement to a formal one (which should probably end up somewhere more generally discussing conventions for formal statements of olympiad problems); (b) the structure describing a configuration satisfying the conditions of the problem, and used to build up information gradually through 58 lemmas without needing to pass lots of hypotheses around, which seems likely to be a convenient way to handle many olympiad geometry solutions; (c) how the calc blocks for equality of angles modulo π, and consequent deductions that certain points are cospherical, that make up essentially the whole informal argument, are actually quite short and the bulk of the formalization is proving all the nondegeneracy conditions (that certain points aren't equal, or aren't collinear) needed for the informal argument to work.

imo2019_q2_nolocalimports.lean

[Floris van Doorn]

Neat!
Am I correct in thinking that P_ne_P₁ follows from sbtw_P_B₁_P₁? I also feel like C_ne_P₁ should follow from the other assumptions, and same for Q₁. But other than that, the statement looks like a very nice translation of the problem!

[Kevin Buzzard]

So is it feasible to have some kind of widget which draws a diagram of the question subject to the constraints and lets the user move points around in the diagram subject to the constraints being maintained? I would like that for school talks.

[Patrick Massot]

I know that some people worked on this topic in other contexts.

[Joseph Myers]

I've updated the stated conventions for when it's unnecessary to state a hypothesis of two points being different (that's implicit from the problem talking about an angle or a line) because it trivially follows from something else in the problem, to include the case of the two points being in a strict betweenness condition, and removed P_ne_P₁ and Q_ne_Q₁.

As for C_ne_P₁ and C_ne_Q₁, if they follow from the other hypotheses it's not the same kind of following immediately and trivially as for the case where the two points are specified to be in a triangle or in a strict betweenness relation. And while for code in mathlib proper we'd try to make the hypotheses strictly minimal - removing hypotheses that would appear in an informal version of a result if in fact the choice of junk values means they aren't needed for the formal version - I think for formal versions of olympiad problems it's better to correspond closely to the informal version than to go for strictly minimal hypotheses.

[Johan Commelin]

I agree that those kind of statements have a large "demo value" and should therefore be resistant to change-of-junk-value.

[Qian Hong]

Kevin Buzzard said:

So is it feasible to have some kind of widget which draws a diagram of the question subject to the constraints and lets the user move points around in the diagram subject to the constraints being maintained? I would like that for school talks.

sounds like what GeoGebra does https://www.geogebra.org/geometry
Interesting fact: the desktop version of GeoGebra has a very basic builtin prover to test coincidence of points / equal of lengths / etc, when the prover fails it fallbacks to numerical method for equivalence test.

[Qian Hong]

most of the time their symbolical checker fails even for very trivial theorems though.

[Qian Hong]

GeoGebra has 100 million registered users: https://www.geogebra.org/m/fzkjvuuv

It would be great if we can find some excuse to build collaborations between Lean and GeoGebra ;-)

[Miroslav Olšák]

Well, making a GeoGebra-like gadget which can represent logic is something I was working some time ago: https://github.com/mirefek/geo_logic

[Miroslav Olšák]

I could return to it if there people would be interested -- learn from what I have done, and do it from scratch again, and even better :-)

About a gadget directly for Lean, I once played with visualization of Sokoban in Lean but I am not sure how flexible Lean's visualization tools are for doing a geometry gadget. And moreover, GeoLogic doesn't require proving the degeneracy conditions (so it is not a strict logic), so we would need to find a way how to represent this in Lean as well. Again, some time ago, I was thinking about using interval arithmetic to prove that the proof is valid at least for a neighborhood of the given configuration but then it turned out that Lean doesn't (didn't?) have an implementation of interval arithmetic :-).

[Miroslav Olšák]

And one more thing -- automatic conversion from a geometry problem represented via conditions (A in l1, B in l1, C in l1, C in l2, ...) to a construction (l1 = line(A,B), C = intersection(l1, l2), ...) is in my view non-trivial. For proving, you want the first representation, for a gadget the second. Not that it wouldn't be doable at all, just that it is not easy.

[Miroslav Olšák]

For example, what I was missing in GeoLogic was a support for geometrical mappings -- reflections, rotations, transitions, homothethy,, spiral similarity ... possibly even circle inversion.
I could do the transformation element-wise but it would be really handy if the system could automatically know how these mappings commute with other operations (reflected point lies on a reflected line, orthocenter of a similar triangle creates a similar picture again, etc...) Of course, I could apply these facts manually but it is a bit annoying. How is actually Lean automation on that?

[Joseph Myers]

We have a few such facts in isolation. The key thing that would be helpful before stating such things more generally is #14315 (Dilations on metric spaces), since most geometrical definitions commute with all similarities, not just with isometries. (There would be a few followups useful on top of getting #14315 into mathlib. For example, defining more bundled type classes for isometries and adding the instances that make all isometry_class instances into dilation_class instances. I think the bundled isometry type remains useful and should stay, but probably renamed to is_isometry; see my comment from 28 Aug in that PR. More bundled types such as those mentioned for a followup in the PR - affine and linear dilations - would also be of use.) Once #14315 and enough followups are in, geometrical lemmas could then be stated for any dilation_class instance; if a particular proof needs an affine_dilation, a version of affine_isometry_of_strict_convex_space could be used to construct one within the proof.

Although maybe not strictly a geometrical transformation, in the formal context very similar lemmas also come up for reindexing indexed families along equivalences of index types. In that regard, I have #17566 open to define affine.simplex.reindex, with the material ready for a followup once that is in to prove that reindexing leaves circumsphere, circumcenter and circumradius unchanged (so triangles ABC and BAC have the same circumsphere etc., for example).

[Joseph Myers]

Once we have enough lemmas and definitions in that area, maybe we could consider what automation would be helpful and practical to implement. (When I get round to proving versions of circle theorems for unoriented angles via using results for oriented angles on an appropriate two-dimensional subspace, I'll get to see just how fiddly the manipulations required are at present to move to a subspace and back.)

[Miroslav Olšák]

Ok, I see. I don't think it is necessary to do it now, rather have in mind that it can be eventually handy. There is also some automation that is already present in GeoLogic, and I am also unsure how Lean is handling it (especially since it requires proving degeneracy conditions). The automation already present in GeoLogic is

• Gaussian elimination for (oriented) angle chasing. Note that this sometimes also admits a non-degeneracy condition because you when you are mod 180, and you know that 2alpha = 2beta, it can mean either alpha = beta, or alpha = 90+beta. GeoLogic just infers this from the picture, formal system could do it as well but it must also create a degeneracy condition goal.
• Equality detection -- congruence closure is the start, but also using further facts such as that different lines can intersect in at most one point, different circles can intersect at at most two points, three different point uniquely determine at most one circle, etc.

These automations were quite important to make GeoLogic somewhat intuitive and usable (so now, I feel like missing the good support of mappings the most annoying missing feature, and also GUI for creating lemmata).

[Miroslav Olšák]

And I was also quite happy about the way I did points on a circle with the oriented angles. Since all my angles are mod 180, I define a bit weirdly a position of a point X on a circle omega as the "half of the direction of the ray OX" where O is the center of omega. This is a number mod 180, since the directions of rays from O are mod 360.
Then for any two different points A, B on omega, I have a theorem that direction(line(A,B)) = pos(A,omega) + pos(B,omega) + 90, and from this basically all the reasoning about angles around a circle easily follow (together with the angle-chasing automation).

[Miroslav Olšák]

If we believe that both Lean's visualization / interaction features, and its state of Euclidean geometry is good enough to build something at least as intuitive as GeoLogic, I am indeed happy to help. I know a bit of Lean but not enough in these two areas. I can see I can consult @Joseph Myers about the Lean's geometry, the other question is who to consult about writing a GUI for Lean :smile:.

[Jason Rute]

Consult @Edward Ayers about GUI stuff. Are you familiar with Lean widgets?

[Jason Rute]

https://leanprover.github.io/lean4/doc/examples/widgets.lean.html

[Jason Rute]

(Here are a bunch of references on Lean widgets I compiled at some point: https://proofassistants.stackexchange.com/a/1693)

[Miroslav Olšák]

I used them for Sokoban visualization (by exporting a sokoban state into a HTML table) but I was not sure how much it can do. I will look at it when I will have some time.

[Joseph Myers]

Oriented angles in mathlib are modulo 2π (lots of basic lemmas do in fact work modulo 2π), with equality modulo π being represented as equality of twice the angles when needed.

[Joseph Myers]

Even given all the work I did for IMO 2019 Q2 (including 20 open PRs and a fair amount more building on top of those), there are still lots of things for which definitions and API have yet to be written (tangency, incenter, anything linking to the measure theory library for areas and volumes, most things to do with convexity other than betweenness, an explicit notion of cyclic polygons / cyclic order of points on a circle, no doubt lots of standard facts about particular configurations, ...).

[Miroslav Olšák]

Well, I find mod 180 more practical (because a line is by default unoriented) but whatever. One can always calculate with doubles / halfs to emulate the other modulo :-).

[Miroslav Olšák]

@Joseph Myers I can see that you put a lot of effort into the degeneracy / topological conditions, although they are not the main focus when first solving a problem. Do you think it would be possible for a visualization / automation to just postpone them as further goals / other cases of the problem, and leave them until the main problem is solved?
I suppose that when you were formalizing the problem, you were just putting sorrys there but I am not sure if such approach is compatible with high level tools.

[Joseph Myers]

Yes, I put sorry for many of those nondegeneracy conditions while formalizing the problem. Then filled in most of the sorrys. Then it took most of a day to eliminate the last one (B₂_ne_A₂ - what's in the file for the IMO problem is short, but it depends on a load of other API of which #17657, #17659, #17660 and #17685 are some of the dependencies developed for that lemma - note that one in some sense genuinely uses betweenness, when the others are more like "follow the consequences of the degenerate configuration and quickly get something absurd").

Postponing side goals seems reasonable for automation, though it would also be interesting if it could dispose of some of the easier cases itself. I don't know if there are sub-cases with known algorithms for automation that are efficient enough to use in practice (for example, whether there's some algorithm to deal with problems involving betweenness and nothing else).

[Joseph Myers]

I've now filed #17993 (depends on #17992, all other dependencies are now in mathlib) with my IMO 2019 Q2 formalization.

[Kevin Buzzard]

soln.png
This is the solution Joseph formalised. It would be great to see this in the goal view!