## Stream: IMO-grand-challenge

### Topic: geometry problems

#### Johan Commelin (Sep 07 2019 at 07:28):

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 (Sep 07 2019 at 07:29):

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

#### Patrick Massot (Sep 07 2019 at 09:10):

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

#### Patrick Massot (Sep 07 2019 at 09:12):

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 (Oct 02 2019 at 14:07):

1. 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 (Oct 02 2019 at 14:07):

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 (Oct 03 2019 at 13:53):

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 (Oct 03 2019 at 14:33):

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 (Oct 03 2019 at 20:16):

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 (Oct 08 2019 at 13:34):

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 (Oct 08 2019 at 13:35):

@Miroslav Olšák Interesting, thanks!

#### Trieu Trinh (Feb 17 2020 at 17:07):

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 (Feb 17 2020 at 21:37):

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 (Feb 18 2020 at 07:31):

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

Last updated: Aug 16 2022 at 18:20 UTC