Geometry

Stream: IMO-grand-challenge

[Daniel Selsam]

Joseph Myers said:

It sounds like you have a long list of geometrical definitions and lemmas found to be useful for formal synthetic geometry proofs. It would be good for that list to be available somewhere as a checklist for anyone expanding mathlib's support for Euclidean geometry.

Geometry is notable in that there are several radically different approaches to proving theorems. Here are the rough categories:

1. Human-incomprehensible coordinate bashes, such as Wu's method and Grobner bases. These methods may be able to prove some useful lemmas automatically, but do not seem to scale to IMO-level problems.

2. Human-comprehensible coordinate bashes, such as the Complex bash and the Barycentric bash. These methods are computationally efficient and can be performed by hand, but do not apply to all problems.

3. Human-comprehensible goal-directed rewriting over higher-level Geometry quantities such as the signed area, the Pythagorean difference, the ratio of parallell directed segments, and the full angle. These methods are described here and here. These methods can also be performed by hand, but they are also incomplete.

4. Synthetic reasoning with the "magical" introduction of auxiliary constructions. Our preliminary experiments took this approach, not because it is the most powerful but because categories 1, 2, and to some extent 3 seem unique to Geometry, and solvers based on them are unlikely to usefully inform solvers for the other three IMO categories. We started with the axioms for unordered Geometry used by previous work on forward-chaining for Geometry, and then proceeded through Euclidean Geometry in Mathematical Olympiads (EGMO) adding as additional lemmas any theorems that our solver could not yet easily prove.

My suggestion would be to use EGMO as a guide.

[Joseph Myers]

Since human geometry proofs can combine different approaches, I hope mathlib ends up with enough geometry that human-like proofs combining the approaches can be formalised as well.

[Joseph Myers]

That link on unordered geometry looks like a useful source for very basic lemmas that are too basic to appear in most books. The use of unordered geometry, and the particular concepts defined there, suggest a few questions about what definitions should look like in mathlib.

[Joseph Myers]

1. An IMO geometry problem often involves ordering of points, even if a version of the result would be true with directed angles without the ordering (or sometimes the ordering is only stated to avoid worries about different configurations and the original result is still true without it). IMO 2019 problem 2 has several requirements that a point is strictly between two other points (or on a segment, etc.), which should be included in any formal version, and equalities of angles in an IMO problem such as that one mean equalities of undirected angles (similarly, where IMO 2019 problem 6 refers to an acute triangle, that's a statement about undirected angles). So if you're going to solve an IMO problem with a solver that uses directed angles, you also need a solver that can create a formal proof that the directed-angles result implies the original result.

[Joseph Myers]

2. That link uses equality of directed angles between lines to avoid configuration-dependence. There are several possibilities for how directed angles (both modulo π, for angles between lines, and modulo 2π, for angle of a rotation) might be represented in mathlib, which are all more or less the same if you're only concerned with equality but become different when you do other calculations with those angles. (a) Define directed angles in a context where you are given an orientation of the 2-dimensional affine (sub)space the points are in, as a quotient of the reals, like the angle type in analysis.special_functions.trigonometric. (b) Define directed angles in such a context, but as a real number between 0 and π or 2π, so it's more convenient to use real number operations with them. (c) Define directed angles without being given an orientation, as an add_comm_group that can only be mapped to or from real numbers when you add the information about the orientation. (All of these except maybe (c) require the concept of an orientation of a finite-dimensional vector space / subspace / affine space / subspace over an ordered field, which I don't think mathlib has yet.)

[Joseph Myers]

3. When is it desirable to have a definition, versus expanding what would be the content of that definition directly in each place that would use it, if in practice you'll want to use the underlying concepts a lot when working with that definition rather than building up an API for the definition that means the underlying concepts aren't generally relevant? Should there be a bundled definition of line as an affine subspace with dimension 1, or should affine_subspace be used with the dimension as an extra hypothesis when needed, given that I've found a lot of the time when working with lines you want to use more general affine_subspace lemmas and duplicating them all for the bundled case would be awkward? (Also, if you're using a bundled line type you can't even construct the line AB without first proving A ≠ B, whereas with the unbundled version you can construct affine_span ℝ {A, B} and only later prove the points are different if you need that.) Should concyclic be defined as cospherical together with coplanar or should lemmas just use cospherical together with any other conditions needed? Should parallel be defined (as equal directions together with one subspace being empty iff the other is), or should equality (in most cases it's clear neither subspace can be empty) just be used directly? (This isn't just an issue for geometry, of course. Should the formal version of any IMO problem referring to an odd integer translate it as ¬ even n, or should there be a definition of odd in mathlib so the mathematical statement can be expressed more directly, even if simp converts it to ¬ even? Certainly there should be conventions for the IMO Grand Challenge that say what the canonical way to express such concepts is.)

[Kevin Buzzard]

Joseph thanks a lot for your thoughts.

[Daniel Selsam]

So if you're going to solve an IMO problem with a solver that uses directed angles, you also need a solver that can create a formal proof that the directed-angles result implies the original result.

I agree it will be necessary to use ordering conditions to convert between the two types of angles. I will add that directed angles can be useful even when the problem does not mention angles at all because many concepts (e.g. parallel, perpendicular, collinear, cyclic) have simple expressions in terms of directed angles.

[Daniel Selsam]

Joseph Myers said:

This isn't just an issue for geometry, of course. Should the formal version of any IMO problem referring to an odd integer translate it as ¬ even n, or should there be a definition of odd in mathlib so the mathematical statement can be expressed more directly, even if simp converts it to ¬ even?

FWIW I prefer having odd.

[Miroslav Olšák]

Daniel Selsam said:

So if you're going to solve an IMO problem with a solver that uses directed angles, you also need a solver that can create a formal proof that the directed-angles result implies the original result.

I agree it will be necessary to use ordering conditions to convert between the two types of angles. I will add that directed angles can be useful even when the problem does not mention angles at all because many concepts (e.g. parallel, perpendicular, collinear, cyclic) have simple expressions in terms of directed angles.

This is not only case of directed angles. Geometrical theorems often work only under certain topological configuration, and the synthetic theorem prover often deal with it just by checking the condition numerically for a given diagram. Such a diagram-based logic is also the core of GeoLogic -- my GUI-ITP for geometry. The question how to convert such a semi-formal proof into actually formal one is another question and people solving the geometry problems have some strategies for it -- typically either proving the topological facts in general, or case analysis on different setups and using very similar reasoning for the cases.

[Daniel Selsam]

Miroslav Olšák said:

The question how to convert such a semi-formal proof into actually formal one is another question and people solving the geometry problems have some strategies for it -- typically either proving the topological facts in general, or case analysis on different setups and using very similar reasoning for the cases.

Do you have an example in mind of an order/ndg condition that you think is necessary to prove an Olympiad problem but that you don't think is actually provable even after a charitable interpretation of the problem (e.g. all points distinct)?

[Daniel Selsam]

^ and that is also relatively recent, in light of https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving/topic/IMO.20Grand.20Challenge/near/210313179

[Miroslav Olšák]

Not anything specific in mind. I didn't mean that the geometry problem would be unprovable -- the problem statements are precise enough. I am just postponing proving such conditions when proving the problem as a human being, and I consider postponing them to be reasonable even for an automated synthetic prover.

I think it is possible to find an example where the order / degeneracy condition cannot be proven, so that it is necessary to discuss multiple cases in the solution. The cases are typically either analogous, or easier than in the original configuration. Would you like me to search for such problems? Because I could possibly contribute more if I didn't look at the official solutions first, and tried to solve the problems myself (but it makes the search for a problem with a specific feature in the solution harder).

[Daniel Selsam]

I think it is possible to find an example where the order / degeneracy condition cannot be proven, so that it is necessary to discuss multiple cases in the solution. The cases are typically either analogous, or easier than in the original configuration. Would you like me to search for such problems?

I do not think it is necessary to seek them out -- I think we will come across them in due time as a consequence of formalizing historical problems.

[Joseph Myers]

Now the IMO 2020 problems are out, we can see we're some way from being able to express problem 1, as that requires the concept of a list of four points forming a convex quadrilateral, and of the interior of such a convex quadrilateral (and of course we should try to define such things in a general form that also covers non-convex polygons, or the interior and exterior of a non-polygonal curve or surface, or a convex polyhedron with n faces). (We also don't have explicit concepts of "internal bisector" of an angle, but that's straightforward to define, or "perpendicular bisector" of a segment, though that can be expressed easily using mk' p d.orthogonal where p is the midpoint and d is the direction of the segment, but we may want specific definitions for both the midpoint (in an affine space context) and the perpendicular bisector.) And once the problem has been expressed, a condition involving ratios of angles seems outside the scope of any system where only equality of angles is used.

Problem 6 would be much more straightforward to express in a natural way, though we ought to add a definition of the distance between a point and a nonempty affine subspace (and of distance between two nonempty affine subspaces) rather than needing to use orthogonal_projection explicitly whenever we wish to refer to such a distance.

[Kevin Buzzard]

(link to problems)

[Scott Morrison]

Problems 4 and 5 are both "determine which" problems...