Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: geometry revisited

view this post on Zulip Daniel Selsam (May 11 2021 at 03:12):

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

view this post on Zulip Johan Commelin (May 11 2021 at 03:59):

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

view this post on Zulip Joseph Myers (May 11 2021 at 11:17):

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.

view this post on Zulip Joseph Myers (May 11 2021 at 11:23):

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".

view this post on Zulip Kevin Buzzard (May 11 2021 at 12:03):

@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?

view this post on Zulip Joseph Myers (May 11 2021 at 12:35):

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).

view this post on Zulip Daniel Selsam (May 11 2021 at 15:29):

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

view this post on Zulip Daniel Selsam (Mar 09 2022 at 01:27):

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

Last updated: Aug 16 2022 at 17:18 UTC