PRs towards IMO geometry 2024 P4

Stream: PR reviews

[Joseph Myers]

I currently have the following 14 PRs open working towards IMO geometry problem 2024 P4 (I expect a fair number more in this series before that formalization is finished).

• The final three PRs on the relation of angle bisection to incenter / excenter: #30477, #30981, #30982
• The interaction of Affine.Simplex.reindex to various other simplex definitions: #31054, #31055, #31056, #31057 (#31210, #31256, #31257 are three more such PRs to complete the set of such lemmas on reindex interaction with other simplex definitions, but aren't on the path to IMO 2024 P4)
• Real.Angle lemma: #30943
• Other affine space lemmas: #31167, #31172, #31204, #31205
• Other incenter / excenter lemmas: #31173, #31206

[Joseph Myers]

After some PRs were merged and others opened, I now have 17 open PRs in this series:

• The final three PRs on the relation of angle bisection to incenter / excenter: #30477, #30981, #30982
• The interaction of Affine.Simplex.reindex to various other simplex definitions: #31054, #31055 (maintainer-merge state), #31056, #31057 (#31210, #31256, #31257 are three more such PRs to complete the set of such lemmas on reindex interaction with other simplex definitions, but aren't on the path to IMO 2024 P4)
• Other affine space lemmas: #31172, #31204, #31205
• Other incenter / excenter lemmas: #31173, #31206, #31493
• Convex combination lemmas: #31451, #31452
• Sphere.secondInter lemmas: #31494, #31495

[Joseph Myers]

The current 13 open PRs in this series:

• The final two PRs setting up the relation of angle bisection to incenter / excenter: #30981, #30982.
• The interaction of Affine.Simplex.reindex to various other simplex definitions: #31054, #31056, #31057 (#31210, #31256 are two more such PRs to complete the set of such lemmas on reindex interaction with other simplex definitions, but aren't on the path to IMO 2024 P4).
• Other affine space lemmas: #31205, #31712.
• Other incenter / excenter lemmas: #31206, #31733.
• Convex combination lemmas in strictly convex sets and spaces: #31452.
• Angle lemmas: #31713.
• Sphere.secondInter lemmas: #31495.
• Tangents / orthRadius lemmas: #31731.

[Joseph Myers]

I'd like to ping the orthRadius lemmas in #31731 early, since I'd like to move orthRadius to a separate file next (in preparation for using it in defining pole and polar) and such a refactoring PR moving existing material is awkward while there are also additions to that existing material under review.

[Joseph Myers]

Thanks for the review! The PR splitting out orthRadius is now #31850; I have the material ready for the next three PRs building on that once it's in.

[Joseph Myers]

This series is now complete (and so formalization of all six IMO 2024 problems is complete). #32295, with 25 open dependencies, has the IMO 2024 P4 formalization itself. Of the 25 open dependencies, the following have no open dependencies themselves and so are ready for review (and merging them will make various of the other dependencies ready for review).

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31205: feat(Analysis/Convex/Side): affine combinations and sides of faces of a simplex
• #31452: feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces
• #31733: feat(Geometry/Euclidean/Incenter): orthRadius lemmas
• #31979: feat(LinearAlgebra/AffineSpace/Independent): injectivity of spans of images
• #32004: feat(Geometry/Euclidean/Angle/Sphere): unoriented law of sines with circumradius
• #32019: feat(Geometry/Euclidean/Projection): map and subtype lemmas
• #32023: feat(Geometry/Euclidean/Sphere/SecondInter): isometry and subtype lemmas
• #32259: feat(Analysis/SpecialFunctions/Trigonometric/Angle): toReal addition lemmas
• #32290: feat(Geometry/Euclidean/Circumcenter): circumcenter_ne_point
• #32296: refactor(LinearAlgebra/FiniteDimensional/Defs): move of_fact_finrank_eq_two

[Joseph Myers]

Thanks for the reviews so far. We're now down to 18 open dependencies, of which the following 8 have no open dependencies themselves and so are ready for review.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31495: feat(Geometry/Euclidean/Sphere/SecondInter): secondInter and sides of faces of a simplex
• #31733: feat(Geometry/Euclidean/Incenter): orthRadius lemmas
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32019: feat(Geometry/Euclidean/Projection): map and subtype lemmas
• #32259: feat(Analysis/SpecialFunctions/Trigonometric/Angle): toReal addition lemmas
• #32273: feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex

Also note that once the full series is in, Mathlib.Geometry.Euclidean.Incenter will be very close to the 1500-line limit, but I propose to wait for all the PRs to that file to be merged before splitting it into three.

[Joseph Myers]

Thanks for the further reviews. We're now at 15 dependencies, with the following 7 immediately available for review as having no further open dependencies themselves.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31495: feat(Geometry/Euclidean/Sphere/SecondInter): secondInter and sides of faces of a simplex
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32021: feat(Geometry/Euclidean/Altitude): map and restrict lemmas
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles
• #32273: feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex

[Joseph Myers]

Thanks for further reviews, now at 13 dependencies, 5 immediately available for review:

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32021: feat(Geometry/Euclidean/Altitude): map and restrict lemmas
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles
• #32273: feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex

[Joseph Myers]

I'd like to ping those five PRs again. #31891 is now showing as the oldest on the queue by its default ordering ("Updated", I think) and #32273 as the 12th oldest. Only #30981 has had any review comments so far.

[Joseph Myers]

Thanks for the further reviews. I believe I've addressed all the further comments on #30981 and #31891; there are no comments yet on #32021, #32260 or #32273.

[Joseph Myers]

Thanks for the further reviews. Now that #32273 is in, #32278 has become available for review.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32021: feat(Geometry/Euclidean/Altitude): map and restrict lemmas
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles
• #32278: feat(Geometry/Euclidean/Incenter): excenters on sides of faces

[Joseph Myers]

Thanks for the further reviews. Now available for review:

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles
• #32278: feat(Geometry/Euclidean/Incenter): excenters on sides of faces

#32260 has no comments so far and is now in 12th place on the queueboard. All the comments on #30981 and #31891 are old and I believe I've addressed them.

[Joseph Myers]

Thanks for the further reviews. The three dependencies in this series currently available for review have all had at least one review, with review comments addressed, and now need reviewing again.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles

[Kevin Buzzard]

Off-topic and please don't let me derail this thread (if this turns into a longer discussion then we can perhaps move it): Is there a way of tracking how many PRs have needed to be merged before one can state this one IMO problem idiomatically? I think it's absolutely commendable that the community are doing this properly (and would expect nothing less from Joseph) but it's also interesting to see how much formalization one IMO problem has motivated.

The statement of the problem can be seen here https://artofproblemsolving.com/wiki/index.php/2024_IMO_Problems/Problem_4 . It is a standard 2d geometry problem about a triangle, involving the incircle, circumcircle and some tangent lines. IIRC this is the problem which DeepMind's bespoke tool (not their Lean tool, their geometry tool) solved in about ten seconds flat. This thread is perhaps an indication of why they didn't try their Lean tool on it!

[Joseph Myers]

We've been able to state this one for a long time, most of the PRs are for proving it. It's a bit fuzzy whether the PRs initially setting up definitions of inspheres and tangency should be considered as part of the PRs towards (stating and proving) this problem, or just as generally setting up definitions to support stating more past IMO geometry problems, but if they are then it's a bit over 100 in total (even without those I think it ends up as about 100 PRs for the solution).

[Joseph Myers]

For stating other IMO geometry problems, some of the most frequently encountered gaps in mathlib include polygons (we have an active PR, though definitions for convex polygons will need building on top of that), arcs of circles (we also have a recent PR), areas (recent Zulip discussion, no PR from that yet) and some kind of bundled definition of an angle bisector as an affine subspace (line) (older Zulip discussion on how to set that up doesn't seem to have resulted in a PR).

[Joseph Myers]

Ping again on these three PRs in this series available for review.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles

These are respectively 1st, 13th and 58th on the queueboard at present.

[Joseph Myers]

The currently available PRs in this series all have some level of review:

• #30982: feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter: non-maintainer approved (no comments)
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars: a series of past reviews and comments that have been addressed, nothing in the past month
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles: review comments have been addressed, non-maintainer approved

[Joseph Myers]

I'd like to ping these PRs again:

• #30982: feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter: non-maintainer approved (no comments)
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars: a series of past reviews and comments that have been addressed, nothing in the past month (beyond fixing merge conflicts)
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles: review comments have been addressed, non-maintainer approved and marked as maintainer merge