geometry problems

Stream: IMO-grand-challenge

[Johan Commelin]

Every IMO typically features one or two geometry problems. These might be a relatively easy target for AI. One can attack them using Gröbner bases, or decidability for real closed fields. Both algorithms are expensive, but they have been implemented before. I think Maple and Mathematica can solve a whole bunch of these problems, and versions of these have also been implemented in Coq.

[Johan Commelin]

I have no idea if they have ever been systematically "tested" against a database of IMO level geometry problems.

[Patrick Massot]

Reference: https://geocoq.github.io/GeoCoq/

[Patrick Massot]

I'm not sure that brute forcing a computational proof using the area method, or Gröbner bases, really counts as AI. The same issue arise with finite combinatorics IMO problems where a human brute force search would be impossible but a computer can do it. Should it really count as a solution?

[Miroslav Olšák]

2. Geometry
   This is actually a field that I proposed to start with on AITP 2018. As far as I know, the computational methods (Wu's method / Gröbner basis / ...) are stronger than any synthetic approach, and I have heard that they are capable of solving at least some of the IMO problems. On the other hand, the computational methods cannot be generalized for other fields which is why I am not so much interested in them, and I prefer synthetic ones. I believe that the geometrical problems are the easiest ones even using the synthetic approach only.

[Miroslav Olšák]

Because of that, I am now focused mainly on geometry, and I have translated the officialy available shortlists to a semi-formal language (parseable but without detailed semantics and not in any particular therem prover so far). So I could help a bit with this part.

[Miroslav Olšák]

Because of that, I am now focused mainly on geometry, and I have translated the officialy available shortlists to a semi-formal language (parseable but without detailed semantics and not in any particular therem prover so far). So I could help a bit with this part.

Miroslav Olšák Nice! Can you share one example to give us a sense of the semi-formal language?

Sure:

triangle(A,B,C)
M = midpoint(A,C)
circle(w)
B on w
M on w
P = intersection(w, segment(A,B))
Q = intersection(w, segment(B,C))
parallelogram(B,P,T,Q)
T on circumcircle(A,B,C)

DETERMINE: distance(B,T) / distance(B,M)

Note that I also have a parser for that, so I can tell the types of the objects, possibly convert it to other format, etc.

[Miroslav Olšák]

As far as I know, the computational methods (Wu's method / Gröbner basis / ...) are stronger than any synthetic approach, and I have heard that they are capable of solving at least some of the IMO problems
...
Note that I also have a parser for that, so I can tell the types of the objects, possibly convert it to other format, etc.

Miroslav Olšák I am very curious which existing problems can be solved by which existing tools. What do you think are the most relevant off-the-shelf tools to try?

I don't know, perhaps we should ask people from the community around automated deduction in geometry. I don't have many contacts to them yet, For example, I exchanged a few e-mail with Pedro Quaresma (about synthetic approach), so you can try him.

[Miroslav Olšák]

I have heard about the area method too but I don't know how powerful it really is. As far as I know it is a generalization of perhaps the nicest proof of Ceva's theorem (using areas).
An issue of it may lie in the following

The area method is used for proving constructive geometry conjectures: statements about properties of objects constructed by some fixed set of elementary constructions.

(see page 10 of the referred paper: https://hal.archives-ouvertes.fr/hal-00426563/PDF/areaMethodRecapV2.pdf)
If you look at the statements of IMO geometry problems, they are rarely of the form "there is a construction X, proof property Y", more often they are of the form "there is a construction X, prove that if property Y holds, then property Z holds." And even if they are of the first form, would they fit to the constructions and properties that area method uses?
Generally, I don't believe that there is any human-feasible method that would solve by itself a large portion of IMO geometry problems. The IMO jury should be trying to prevent it. If IMO geometry problems are solvable by a computer (I believe it could be the case), it should require large computations.

[Miroslav Olšák]

I asked Peter Novotný about solving IMO geometry problems by computer, he dealt with this topic as a master thesis in 2004. His work was inspired by paper "D. Kapur. Geometry Theorem Proving Using Hilbert’s Nullstellensatz (1986)". He manually encoded 17 IMO geometry problems from years 1984--2003 into problems about Gröbner basis. Without any modifications, he hasn't solved anything. However, after manual addition of degeneracy conditions, he managed to prove 11 of the 17 problems. In particular, he failed to prove problems: 85/1, 96/2, 99/5, 00/6, 02/2, 03/3, and he proved: 84/4 (both directions of equivalence), 85/5, 87/2, 92/4, 93/2 (both cases a, b), 94/2 (both directions of equivalence), 95/1, 97/2, 98/1, 00/1, 03/4 (both directions of equivalence).

[Daniel Selsam]

@Miroslav Olšák Interesting, thanks!

[Trieu Trinh]

Miroslav Olšák said:

I asked Peter Novotný about solving IMO geometry problems by computer, he dealt with this topic as a master thesis in 2004. His work was inspired by paper "D. Kapur. Geometry Theorem Proving Using Hilbert’s Nullstellensatz (1986)". He manually encoded 17 IMO geometry problems from years 1984--2003 into problems about Gröbner basis. Without any modifications, he hasn't solved anything. However, after manual addition of degeneracy conditions, he managed to prove 11 of the 17 problems. In particular, he failed to prove problems: 85/1, 96/2, 99/5, 00/6, 02/2, 03/3, and he proved: 84/4 (both directions of equivalence), 85/5, 87/2, 92/4, 93/2 (both cases a, b), 94/2 (both directions of equivalence), 95/1, 97/2, 98/1, 00/1, 03/4 (both directions of equivalence).

Is there a write up/ report that can be found anywhere? I tried to search for this and nothing came up.

[Peter Jin]

Trieu Trinh said:

Miroslav Olšák said:

I asked Peter Novotný about solving IMO geometry problems by computer, he dealt with this topic as a master thesis in 2004. His work was inspired by paper "D. Kapur. Geometry Theorem Proving Using Hilbert’s Nullstellensatz (1986)". He manually encoded 17 IMO geometry problems from years 1984--2003 into problems about Gröbner basis. Without any modifications, he hasn't solved anything. However, after manual addition of degeneracy conditions, he managed to prove 11 of the 17 problems. In particular, he failed to prove problems: 85/1, 96/2, 99/5, 00/6, 02/2, 03/3, and he proved: 84/4 (both directions of equivalence), 85/5, 87/2, 92/4, 93/2 (both cases a, b), 94/2 (both directions of equivalence), 95/1, 97/2, 98/1, 00/1, 03/4 (both directions of equivalence).

Is there a write up/ report that can be found anywhere? I tried to search for this and nothing came up.

His personal website appears to be at: https://skmo.sk/cvika/ which links to the master thesis (look for diplomová práca). Google translate says the title is, "Use of Gröbner bases for proofs of elementary geometry theorems."

[Miroslav Olšák]

Yes, the thesis is here, however in Slovak: https://skmo.sk/cvika/ukazpdf.php?pdf=diplomka.pdf
He has also sent me the following presentation (also in Slovak): http://www.olsak.net/mirek/peter-novotny-prezentace.pdf