Géométrie et olympiades : AI Google 23++ vs Xcas 40

Bernard.Parisse@univ-grenoble-alpes.fr

4 Février 2024

Résumé: On compare ici deux logiciels permettant de faire des preuves en géométrie, AlphaGeometry à base d’“intelligence artificielle” (géométrie synthétique) et Xcas (assistance calcul formel en géométrie analytique).

1 Introduction

Google a annoncé le 17 janvier dernier une AI (artificial intelligence) dédiée à la résolution de problèmes de géométrie euclidienne dans le plan suffisamment compétitive pour être (presque) classée médaille d’or aux Olympiades internationales de mathématiques (OIM), en annonçant devancer largement l’état de l’art à base de calcul formel (bases de Groebner, méthodes de l’aire, de Wu...). Ceci a attiré mon attention, car Xcas permet de faire des preuves assistées par le calcul formel en géométrie, j’ai donc passé environ deux semaines à résoudre des problèmes d’olympiades avec Xcas, et à essayer de comprendre plus précisément ce que AlphaGeometry est capable de faire. Il se trouve que j’ai résolu tous les problèmes résolus par AlphaGeometry (24), mais aussi des problèmes non résolus, une quinzaine, en fait la plupart des problèmes de géométrie des olympiades 2000-2023 peuvent être résolus en géométrie analytique avec un bon moteur de calcul formel.

Je vais détailler dans les sections qui suivent ce que je pense avoir compris du fonctionnement de AlphaGeometry, puis ce que Xcas est capable de faire, et comment paramétrer le plus efficacement possible les problèmes pour Xcas. Les énoncés des problèmes sont disponibles sur le site des olympiades, j’y ferai référence en donnant l’année (sur 2 chiffres) et le numéro de problème. Attention la numérotation utilisée correspond aux énoncés effectivement donnés aux candidats, et pas aux corrigés en anglais de l’ensemble des problèmes proposés dont seule une petite partie a été réellement donnée aux candidats.

Entre 2000 et 2023, avec normalement 2 problèmes d’olympiades en géométrie par an, on devrait disposer de 48 énoncés de géométrie. J’en ai dénombré 41 qui sont potentiellement résolubles en géométrie analytique assistée par du calcul formel (j’exclus des énoncés dépendant d’un nombre $n$ arbitraire de points) et obtenu 40 solutions complètes par Xcas (l’exception est 03p3). AlphaGeometry (AG) a lui sélectionné un sous-ensemble de 28 énoncés, créant une base de donnée de 30 traductions (2 énoncés disposent de 2 traductions distinctes 02p2 avec 2 solutions, 08p1 avec 1 solution sur les 2 traductions) et fournit 23 solutions complètes et 2 solutions partielles (2 équivalences remplacées par des implications dans un sens: 03p4 et 04p5, pour cette dernière prouver l’implication dans l’autre sens est significativement plus difficile, au moins avec Xcas). Ceci explique le score du titre: 23++ pour AG à 40 pour Xcas.

Avertissement : Il ne s’agit pas du tout ici de défendre l’idée qu’il faudrait remplacer des raisonnements de géométrie pure par des preuves de géométrie analytique assistées par du calcul formel, les deux ont leur place. Je me suis intéressé à la question des preuves en géométrie analytique d’abord parce que je n’ai pas d’intuition pour trouver des preuves en géométrie pure, mais cela ne m’empêche nullement d’apprécier une belle démonstration inventée par quelqu’un d’autre. Mais j’ai aussi envie de pouvoir prouver des résultats en géométrie, en utilisant des outils que je maitrise bien. Les deux approches ont leurs avantages et inconvénients, et peuvent d’ailleurs se compléter.
Une preuve en géométrie analytique est souvent plus facile à concevoir, ce sont les calculs qui peuvent être difficiles. La géométrie analytique permet de traiter des problèmes numériques, qui ne sont pas accessibles à la géométrie pure : tracé de fonctions, courbes paramétrées, optimisation lorsque la solution n’est pas exacte...
La géométrie synthétique permet de simplifier certains calculs en géométrie analytique. Une preuve en géométrie synthétique est souvent plus difficile à concevoir, mais mobilise moins de connaissances (complexes par exemple) et on n’a pas besoin d’outil informatique de vérification.
Les théorèmes de géométrie me fournissent d’excellents moyens de tester le moteur de calcul formel de Xcas, d’ailleurs en cherchant ces 41 énoncés, j’ai été amené à améliorer ou corriger Xcas.

2 AlphaGeometry (AG)

Voir la section 5 pour des liens sur les ressources. A partir d’un problème donné, il y a une première étape dite de traduction, effectuée par un être humain, qui permet de construire la figure en respectant les contraintes, puis AG détermine une solution ou renvoie un message d’erreur. Par exemple, un énoncé peut dire tracer un point $K$ avec comme contrainte que l’angle $AKB$ est droit, que l’on traduira classiquement par $K$ appartient au cercle de diamètre $AB$ . Il faut bien prendre conscience que cette première étape n’est pas réalisée par AG, et qu’il semble indispensable de pouvoir réaliser cette construction. Ce dernier point peut paraitre évident, mais c’est probablement ce qui empêche toute tentative de résolution par AG d’un certain nombre de problèmes et explique des traductions parfois assez éloignées de l’énoncé originel, par exemple 09p2.

Enoncé 2009p2:
Soit $ABC$ un triangle et $O$ le centre de son cercle circonscrit. Les points $P$ et $Q$ sont des points intérieurs aux côtés $CA$ et $AB$ respectivement. Soit $K$ , $L$ et $M$ les milieux respectifs des segments $BP$ , $CQ$ et $PQ$ , et soit $\Gamma$ le cercle passant par $K$ , $L$ et $M$ . On suppose que la droite $(PQ)$ est tangente au cercle $\Gamma$ . Montrer que $OP$ = $OQ$ .
Ci-dessous la traduction pour Xcas, ici assez fidèle à l’énoncé :

pointc(x):=(1+i*x)/(1-i*x);
assume(b=[0.3,0,2,0.1]);
assume(c=[-0.6,-2,0,0.1]);
A:=point(-1);
B:=point(pointc(b));
C:=point(pointc(c));
triangle(A,B,C);circle(0,1); O:=point(0):;
supposons(p=[0.6,0,1,0.1]);
P:=C+p*(A-C);
supposons(q=[0.3,0,1,0.1]);
Q:=A+q*(B-A);
K:=milieu(B,P);
L:=milieu(C,Q);
M:=milieu(P,Q);
gamma:=circonscrit(K,L,M,display=hidden_name);
PQ:=droite(P,Q,display=hidden_name);
J:=centre(gamma);
I:=projection(P,Q,J);

onload

Traduction AG:
Let $MLK$ be a triangle. Define point $W$ as the circumcenter of triangle $LMK$ . Define point $Q$ such that $MW$ is perpendicular to $MQ$ . Define point $P$ as the mirror of $Q$ through $M$ . Define point $B$ as the mirror of $P$ through $K$ . Define point $C$ as the mirror of $Q$ through $L$ . Define point $A$ as the intersection of lines $QB$ and $PC$ . Define point $O$ as the circumcenter of triangle $CBA$ . Prove that $QO=PO$ .

Le début de preuve de AG:
Proof : Construct point $D$ such that $MK = LD$ and $MD = LK$ .
Construct point $E$ as the mirror of $K$ through $W$ .
Construct point $F$ as the mirror of $Q$ through $D$ .
Step 1. $M, Q, P$ are collinear and $MQ = MP \rightarrow M$ is the midpoint of $QP$ .
... la preuve continue avec en tout 49 étapes. Le point fort d’AG est de construire des points auxiliaires tout seul, comme le ferait un être humain. Par contre la preuve de par sa longueur reste très probablement plus difficile à suivre par un être humain que les solutions proposées sur le site des olympiades.

La preuve avec l’assistance du calcul formel,

factor(numer(I-M));

onload

factor(numer(distance2(O,P)-distance2(O,Q)));

onload

Le problème 2008p6 est un autre exemple, plus complexe et non résolu par AG, dont voici l’énoncé :
Soit $ABCD$ un quadrilatère convexe tel que $BA \neq BC$ . Les cercles inscrits dans les triangles $ABC$ et $ADC$ sont notés respectivement $\omega_1$ et $\omega_2$ . On suppose qu’il existe un cercle $\omega$ qui est tangent à la demi-droite $[BA)$ au-delà de $A$ , tangent à la demi-droite $[BC)$ au-delà de $C$ , et qui est aussi tangent aux droites $(AD)$ et $(CD)$ . Montrer que les tangentes communes extérieures à $\omega_1$ et à $\omega_2$ se coupent en un point de $\omega$ .

X:=point(-1);
assume(a=[0.7,-5,5,0.1]);
Y:=point((1+i*a)/(1-i*a));
assume(b=[0.4,-5,5,0.1]);
Z:=point((1+i*b)/(1-i*b));
assume(c=[-4.0,-5,5,0.1]);
W:=point((1+i*c)/(1-i*c));
circle(0,1);
A:=single_inter(rotation(X,pi/2,line(0,X)),
                rotation(Z,pi/2,line(0,Z)));
B:=single_inter(rotation(W,pi/2,line(0,W)),
                rotation(Z,pi/2,line(0,Z)));
D:=single_inter(rotation(X,pi/2,line(0,X)),
                rotation(Y,pi/2,line(0,Y)));
C:=single_inter(rotation(W,pi/2,line(0,W)),
                rotation(Y,pi/2,line(0,Y)));
triangle(A,B,C); triangle(A,D,C);
w1:=incircle(triangle(A,B,C),display=hidden_name);
I1:=center(w1,display=hidden_name);
w2:=incircle(triangle(A,D,C),display=hidden_name);
I2:=center(w2,display=hidden_name);
d:=line(I1,I2,display=hidden_name);

onload

Et la traduction réalisée pour donner le problème à AlphaGeometry :
Let $XYZ$ be a triangle. Define point $O$ as the circumcenter of triangle $YXZ$ . Let $W$ be any point on circle $(O, X)$ . Define point $A$ such that $AX$ is perpendicular to $OX$ and $AZ$ is perpendicular to $OZ$ . Define point $B$ such that $BW$ is perpendicular to $OW$ and $BZ$ is perpendicular to $OZ$ . Define point $C$ such that $CW$ is perpendicular to $OW$ and $CY$ is perpendicular to $OY$ . Define point $D$ such that $DX$ is perpendicular to $OX$ and $DY$ is perpendicular to $OY$ . Define point $I_1$ such that $AI_1$ is the bisector of angle $BAC$ and $CI_1$ is the bisector of angle $ACB$ . Define point $I_2$ such that $AI_2$ is the bisector of angle $CAD$ and $DI_2$ is the bisector of angle $ADC$ . Define point $F_1$ as the foot of $I_1$ on line $AC$ . Define point $F_2$ as the foot of $I_2$ on line $AC$ . Define points $Q, T$ such that $F_1 I_1 =I_1 Q, F_2 I_2 = I_2 T$ , $I_1 Q$ is perpendicular to $QT$ and $I_2 T$ is perpendicular to $QT$ . Define points $P$ , $S$ such that $F_1 I_1 = I_1 P$ , $F_2 I_2 = I_2 S$ , $I_1 P$ is perpendicular to $PS$ and $I_2S$ is perpendicular to $PS$ . Define point $K$ as the intersection of lines $PS$ and $QT$ . Prove that $OK = OX$ .

C’est seulement ensuite qu’AG entre en scène, cherche et affiche une preuve, en construisant si nécessaire des point supplémentaires (cf. par exemple 2000p6).

La traduction représente ici une étape substantielle, on ne peut pas encore considérer que l’intelligence artificielle a résolu toute seule le problème donné aux candidats. Dans certains cas, la construction de la figure (qui est l’étape de traduction) constitue même l’essentiel de la résolution du problème (contraintes géométriques, c’est une question importante en robotique par exemple).

Le nombre d’étapes de résolution est très variable, en moyenne 45, 41, 110, 31 ou 5, 32 (implication), 29, 13, 20, 27, 40, 49, 57, 24, 59, 59, 38, 22, 110, 26, 63, 15, 35, 19, 211, 35, 13. Il me semble peu probable qu’un être humain vérifie des preuves contenant une cinquantaine ou plus d’étapes.

Le nombre de CPU nécessaires à la résolution en moins d’1h30 varie de 246 (08p1a), 76 (09p6?? peut-être est-ce 19p6), 28 (09p2), 17 (15p3), 12 (20p1, 18p1), 5 (04p1), 2 (10p2), 1 (00p6, 14p4, 12p5).

L’absence de solutions pour 01p1, 01p5, 05p1, 06p1, 07p2, 09p4, 13p3, 14p3, 18p6, 21p4 doit inciter à relativiser la performance de AlphaGeometry, d’autant plus qu’on ne semble pas en mesure de savoir quelle est la marge de progression sur 08p6, 11p6 et 21p3. Les problèmes de 2023 n’ont pas été testés par AG, pour l’article de Nature, c’est certainement lié à la date de soumission, mais pour le communiqué de presse du 17 janvier, ce serait intéressant de savoir si AG sait les résoudre (mon pronostic est 23p2 probable, pour 23p6 non).

3 Xcas

Comme pour AlphaGeometry, la première étape de résolution assistée par Xcas consiste à traduire le problème en une suite de commandes permettant de construire la figure. Il est alors essentiel ici de paramétrer le problème pour rendre les calculs efficaces, sinon avec des problèmes d’olympiades, les calculs deviennent rapidement impraticables. C’est là qu’intervient l’intelligence de l’être humain qui guide les calculs avec l’aide de quelques règles citées ci-dessous. On pourrait peut-être remplacer par une intelligence artificielle sur cette étape, avec probablement nettement moins de puissance nécessaire, mais pour le moment les IA ne semblent pas couplées à des moteurs de calcul formel efficaces. L’ensemble de mes solutions peut se tester depuis le forum de Xcas.

La commande assume de Xcas implémente la notion de curseurs symboliques, ce sont des paramètres qui ont une valeur numérique, mais dont la valeur numérique n’est utilisée que pour les évaluations approchées, en particulier cela permet de réaliser une figure, tout en faisant des calculs avec la variable symbolique associée au curseur.

Un exemple de construction pour 10p2, d’énoncé
Soit $I$ le centre du cercle inscrit dans le triangle $ABC$ et soit $\Gamma$ son cercle circonscrit. La droite $(AI)$ recoupe $\Gamma$ en $D$ . Soit $E$ un point de l’arc $BDC$ et $F$ un point du côté $[BC]$ tels que $BAF$ = $CAE < 1/2 BAC$ . Soit enfin $G$ le milieu du segment $[IF]$ . Montrer que les droites $(DG)$ and $(EI)$ se coupent en un point $J$ de $\Gamma$ .

c:=circle(0,1); I:=point(0);
P1:=point(-1);
assume(a=[0.6,-5,5,0.1]);
P2:=point((1+i*a)/(1-i*a));
assume(b=[0.3,-5,5,0.1]);
P3:=point((1-i*b)/(1+i*b));
L1:=perpendicular(P1,line(0,P1)):;
L2:=perpendicular(P2,line(0,P2)):;
L3:=perpendicular(P3,line(0,P3)):;
A:=single_inter(L1,L2);
B:=single_inter(L1,L3);
C:=single_inter(L2,L3);
triangle(A,B,C);
Omega:=circumcircle(A,B,C);
D:=inter(line(A,I),Omega,[A]);
assume(t=[0.2,0,1,0.1]);
F:=B+t*(C-B);
r:=rotation(A,angle(A,F,B),line(A,C));
E:=inter(r,Omega,[A]);
G:=midpoint(I,F);
J:=single_inter(line(D,G),line(E,I));

onload

On peut modifier la figure, il faut alors cliquer sur le bouton exe ci-dessus pour rafraichir. La construction du cercle inscrit et du triangle $ABC$ sont optimisées pour simplifier les calculs, voir ci-dessous. Voici maintenant la commande qui résoud le problème :
normal(distance2(J,center(Omega))-radius(Omega)^2)

On peut se convaincre que les calculs sont bien faits en fonction des paramètres $a,b,t$ , par exemple

factor(coordinates(J))

Voici quelques méthodes qui permettent de simplifier les calculs de Xcas :

utiliser l’invariance par rotation, translation, changement d’échelle. Ainsi au lieu de prendre 6 coordonnées symboliques pour les sommets de 3 triangle, on peut se ramener à 2, en choisissant le premier point à l’origine, et le deuxième au point de coordonnées (1,0). Le menu Edit d’une figure Xcas a un item permettant de créer automatiquement un triangle de cette manière.
on peut paramétrer rationnellement tous les points d’un cercle unité sauf le point (-1,0) en prenant les points d’affixe $e^{i\alpha}=(1+it)/(1-it), t \in \mathbb{R}$ , on a alors $t=\tan(\alpha/2)$ .
lorsqu’on a un problème avec un cercle circonscrit à un triangle, on choisira un point du triangle en $(-1,0)$ et deux paramètres $a=\tan(\alpha/2)$ et $b=\tan(\beta/2)$ réels pour les deux autres points du triangle. Ainsi on évite un calcul de racine carrée (rayon du cercle circonscrit). Xcas propose un modèle pour générer automatiquement un triangle de ce type.
lorsqu’un cercle inscrit à un triangle intervient, on peut construire les points de tangeance sur le cercle inscrit avec la méthode rationnelle décrite précédemment, puis on détermine le triangle en cherchant les intersections des 3 tangentes aux points de tangeance. On peut ainsi prendre comme points de tangeance $(-1,0)$ et 2 paramètres positifs $a=\tan(\alpha/2)$ et $b=-\tan(\beta/2)$ . Comme les arcs de 2 points consécutifs doivent correspondre à un angle inférieur à $\pi$ , il y a 2 conditions à vérifier pour que le cercle soit bien inscrit (et pas exinscrit), les angles $\alpha$ et $\beta$ doivent être de signe contraire (d’où le choix de signe de $a$ et $b$ ), et on doit avoir $ab<1$ . Ce choix de points permet d’éviter les racines carrées pour trouver le centre du cercle inscrit ou les bissectrices du triangle. Xcas propose un modèle pour générer automatiquement un triangle de ce type.
Si on cherche la 2ème intersection du cercle circonscrit à $ABC$ avec une droite $AD$ passant par un des points du cercle, on prendra le symétrique de $A$ par rapport à la projection sur $AD$ du centre du cercle.
otherd(A,D,c):=reflection(projection(A,D,center(c)),A):;
Si on cherche la 2ème intersection de deux cercles, la 1ère intersection étant connue, on prend le symétrique de cette 1ère intersection par rapport à la droite reliant les centres.
otherc(c1,c2,A):=reflection(line(center(c1),center(c2)),A):;
Pour créer un point $C$ sur une droite $(AB)$ ou un segment $[AB]$ , on utilise une équation paramétrique à partir des points définissant la droite ou le segment, par exemple
assume(t=[0.2,0,1,0.01]);
C:=A+t*(B-A); (ici $t\in[0,1]$ équivaut à $C$ appartient au segment $[AB]$ , pour la droite $(AB)$ on prend $t\in \mathbb{R}$ ).
Lors des calculs, on évitera si possible les racines carrées, en utilisant les instructions adéquates de Xcas : distance2, radius2 et en reformulant les contraintes avec des carrés, par exemple deux cercles de rayons $r$ et $R$ sont tangents si la distance $d$ entre les centres vérifie $d=r+R$ ou $d=|r-R|$ se traduira par la forme développée de $(d+r+R)(d-(r+R))(d+r-R)(d+R-r)=R^4-2R^2d^2-2R^2r^2+d^4-2d^2r^2+r^4$ qui ne fait intervenir que des carrés (ce qui explique l’ajout du facteur $d+r+R$ toujours positif qui parait superflu à première vue)
Pour savoir si 3 points $A,B,C$ d’affixe $a,b,c$ sont alignés, on peut tester que $(b-a)/(c-a)$ est réel, ce qui se traduit en Xcas par normal(im((B-A)/(C-A)))==0, on peut même éviter l’introduction d’une fraction avec le test normal(im((B-A)*conj(C-A)))==0
De même, il est souvent utile de traduire les contraintes d’égalité d’angle par des conditions sur les affixes (par exemple partie imaginaire d’un affixe nul).
De même, pour effectuer une rotation d’angle arbitraire, il est avantageux de multiplier par $1+ia$ où $a$ est un paramètre, ou mieux par $(1+ia)/(1-ia)$ si on veut un complexe de module 1 (différent de -1, correspondant à un angle plat).
Les problèmes d’olympiade travaillent avec des angles non orientés, on peut utiliser la fonction tangente pour gérer cette spécificité
Il est parfois nécessaire d’aider le système pour obtenir une simplification à 0. Par exemple, développer une fonction trigonométrique avec texpand, multiplier par le conjugué avec la commande mult_conjugate(), ...

En appliquant ces règles lors de la construction de la figure, on peut résoudre plus de la moitié des problèmes 2000-2023 de manière quasi-automatique, je dénombre 23 problèmes sur 40 dans ce cas: 00p6, 02p2, 03p4, 05p5, 07p4, 08p1, 09p2, 09p4, 10p4, 11p6, 12p1, 12p5, 13p4, 14p4, 15p3, 15p4, 16p1, 17p4, 18p1, 19p6, 21p3, 21p4, 22p4, et on peut ajouter l’implication dans un sens de 04p5 (AG ne traite que ce sens). Parmi ceux-ci 09p4, 11p6, 21p4 ne sont pas résolus par AG. Parmi les problèmes restants, 00p1, 04p1, 10p2, 19p2, 23p2 se résolvent avec un peu de travail à la construction, 01p1, 07p2, 13p3, 14p3 avec un peu de travail à la résolution. Les problèmes nécessitant une intervention humaine plus conséquente sont 01p5, 04p5 (pour la partie équivalence), 05p1, 06p1 (résolution), 08p6 (construction et résolution), 20p1 (construction), et surtout 18p6 et 23p6 qui sont difficiles.

4 Conclusion

AlphaGeometry (AG) est plus automatisé que Xcas, mais pas encore complètement. Xcas permet de résoudre presque le double de problèmes d’olympiades. Certains problèmes sont probablement hors d’atteinte pour la version actuelle de AG parce qu’ils nécessitent un calcul préalable pour effectuer une construction, AG ne semble pas capable de raisonner sur une figure approximative, contrairement à un être humain en géométrie synthétique ou à Xcas qui peut calculer en géométrie analytique. AG fournit un certificat (le détail des étapes de preuve) qui permet à un être humain de vérifier (si le nombre d’étapes n’est pas trop important), les calculs de Xcas sont par contre souvent trop techniques pour être vérifiés à la main (de ce fait, un logiciel au code source fermé ne devrait pas être utilisé pour fournir une preuve en géométrie analytique).

Toutes les solutions Xcas s’exécutent en au plus une poignée de secondes (hors temps de téléchargement du moteur de calcul) sur un appareil standard (PC, smartphone), avec une quantité de mémoire vive largement en-dessous des possibilités des appareils actuels (256 Mo). La puissance nécessaire pour faire tourner AG est incomparablement plus élevée et hors de portée d’un utilisateur chez lui (l’article parle de 10 000 processeurs en parallèle, il faut pour au moins un problème plus d’une centaine de processeurs pour le résoudre en moins d’1 heure 30, c’est 5 ordres de grandeur au-dessus).

Il a aussi fallu entrainer AG avec plusieurs centaines 100 millions de problèmes (presque tous générés automatiquement, l’article de Nature parle de 500 millions avec 100 000 processeurs en parallèle tournant pendant 72h, ce qui doit représenter une consommation énergétique de l’ordre de la centaine de milliers de kWh) et la résolution de certains problèmes en le temps limite pour un candidat aux olympiades (1h30) peut nécessiter plus de 100 CPU en parallèle (soit plus de 1kWh pour un seul problème contre 12s et 0.0002kWh pour l’ensemble des 40 problèmes sur mon ordinateur portable acheté en 2022 avec Xcas sur 1 seul CPU). C’est certainement incomparable avec l’intelligence humaine, il est assez évident que les candidats aux olympiades n’ont pas eu le temps de s’entrainer sur plus de 100 millions de problèmes! D’ailleurs personne ne semble pouvoir prédire quel serait le taux de réussite d’AG si on multipliait son entrainement par deux, car on ne sait pas vraiment comment l’IA fonctionne. AG pourra-t-il résoudre un énoncé un peu ouvert comme 01p5 ou avec des contraintes de construction fortes comme 05p1 ? Coté Xcas, l’ensemble des 40 solutions tournent en une dizaine de secondes, on sait comment optimiser un problème pour le résoudre en géométrie analytique (diminuer le nombre de paramètres, éviter les racines carrées...), je sais pourquoi Xcas ne peut pas résoudre 03p3 (on a 3 contraintes d’égalité pour rendre égaux 6 paramètres d’angle, ce qui nécessite trop d’astuces pour être résolu mécaniquement) et j’ai pu améliorer l’algorithme de simplification de Xcas dans un cas particulier en observant les caractéristiques de problèmes non ou mal résolus.

Cela laisse penser que l’association intelligence humaine, puissance de calcul informatique, chacun dans son domaine d’excellence (l’intelligence humaine guidant la capacité de calcul informatique) devrait rester plus efficace que l’IA seule, en tout cas telle qu’elle est implémentée aujourd’hui. J’estime que c’est plutôt dans cette direction qu’il faudrait avancer, au lieu de dépenser des sommes et des quantités d’énergie importantes (en kWh par problème) dans des projets tels que AG.

5 Références

AlphaGeometry : l’article de la revue Nature, les 30 traductions, le détail des preuves de AG, le code source.
Les 40 solutions Xcas.
D’autres logiciels de géométrie avec assistance de preuve GCLC, JGEX version Java de GEX, il existe probablement aussi des assistants de preuve en géométrie utilisant Lean, Coq ou z3. Geogebra a également un projet de preuve automatique en géométrie Geogebra Portfolio Prover par la méthode dite de Botana.
L’axiomatique de Tarski, la méthode de l’aire (on y trouve de la bibliographie vers les méthodes de preuves automatiques en géométrie du plan), la méthode de Wu.
Le site des olympiades,

6 Mise à jour juillet 2024

Le 25 juillet 2024, Google annonce “AI achieves silver-medal standard solving International Mathematical Olympiad problems”. Cela correspond à la résolution de 4 des 6 énoncés donnés aux olympiades de juillet 2024, où Google prétend que sa solution mérite le score maximal de 7/7. Deux logiciels sont utilisés AlphaProof (hors géométrie) et AlphaGeometry2 (AG2) pour la partie géométrie. Il reste toujours une intervention humaine, dite étape de formalisation.

Google indique que AG2 est une version améliorée de AG1, capable de résoudre 83% des problèmes de géométrie des 25 dernières années contre 53% pour AG1. On aurait donc 36 problèmes résolus par AG2 sur les 41 de la période 2000-2023 au lieu de 23, mais je n’ai pas trouvé le détail des problèmes non résolus. Le gain en efficacité annoncé est de 2 ordres de grandeur.

L’unique problème de géométrie posé en 2024 (contre 2 habituellement) est annoncé résolu en 19 secondes, mais on ne sait pas quel est le nombre de processeurs utilisés en parallèle. L’énoncé est le suivant :
Soit $ABC$ un triangle tel que $AB<AC<BC$ . Soit $\omega$ le cercle inscrit à $ABC$ et $I$ son centre. Soit $X$ le point de $(BC)$ distinct de $C$ tel que la droite passant par $X$ parallèle à $(AC)$ soit tangente à $\omega$ , et de même $Y$ en échangeant le rôle de $B$ et $C$ . Soit $P$ la deuxième intersection de la droite $(AI)$ avec le cercle circonscrit à $ABC$ . Soit $K$ et $L$ les milieux de $AC$ et $BC$ respectivement.
Montrer que la somme des angles $IK,IL$ et $PY,PX$ vaut 180 degrés.
Voici une construction avec Xcas

pointc(x):=(1+i*x)/(1-i*x);
assume(a=[0.9,0,2,0.1]);
assume(b=[0.3,0,2,0.1]);
P1:=point(-1,display=hidden_name);
P2:=point(pointc(a),display=hidden_name);
P3:=point(pointc(-b),display=hidden_name);
L1:=perpendicular(P1,line(0,P1)):;
L2:=perpendicular(P2,line(0,P2)):;
L3:=perpendicular(P3,line(0,P3)):;
A:=single_inter(L1,L2);
B:=single_inter(L2,L3);
C:=single_inter(L3,L1);
triangle(A,B,C);circle(0,1);
X:=single_inter(line(B,C),reflection(0,line(A,C)));
Y:=single_inter(line(B,C),reflection(0,line(A,B)));
otherd(A,D,c):=reflection(projection(A,D,center(c)),A):;
I:=point(0);
c:=circumcircle(A,B,C);
P:=otherd(A,I,c);
K:=midpoint(A,C);
L:=midpoint(A,B);

onload
et la solution qui s’exécute en une fraction de secondes
t1:=tan(angle(I,K,L)); t2:=tan(angle(P,Y,X)); normal(t1+t2);
Si on regarde la formalisation par AG2 de ce problème,
triangle a b c; a b < a c; a c < b c; incenter i a b c; coll x b c; x != c; foot d i b c; perp x t1 t1 i; cong i t1 i d; para x t1 a c; coll y b c; y != b; perp y t2 t2 i; cong i t2 i d; para y t2 a b; circle o a b c; line_circle_intersection p a i o a; p != a; midpoint k a c; midpoint l a b; ? angeq i l i k p x p y 1 -1 1 -1 180
on s’aperçoit qu’elle est non effective, c’est-à-dire qu’il n’est pas prouvé que la construction de $X$ et $Y$ est possible, d’ailleurs Google indique bien que la figure d’illustration est une construction approchée. En effet, $X$ semble construit comme un point quelconque de la droite $(BC)$ (coll x b c;) et on fait ensuite des hypothèses sur des points de la construction (cong i t1 i d; para x t1 a c;). Pourtant la construction effective de $X$ et $Y$ est assez simple, il suffit de prendre l’intersection de la droite symétrique par rapport à $I$ de $(AC)$ ou de $(AB)$ avec $(BC)$ . On peut se demander si une telle solution mérite vraiment 7/7...