% Merci a Yannick Chevallier pour la version mathjax-enabled
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amsfonts,amssymb}
\usepackage{listings}
\usepackage[francais]{babel}
\usepackage{times}
\usepackage{xspace}
\usepackage{makeidx}
\usepackage{graphicx}
\usepackage{ifpdf}
\ifpdf
 \usepackage[colorlinks,pdftex]{hyperref}
\else
 \usepackage[ps2pdf,breaklinks=true,colorlinks=true,linkcolor=red,citecolor=green]{hyperref}
\fi
\newcommand{\bs}{\symbol{92}}
\newtheorem{thm}{Th\'eor\`eme}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{defn}[thm]{D\'efinition}
\makeindex

% \renewcommand{\cuttingunit}{subsection} (add HEVEA after % for hacha)
\input{giacfr.tex}
\ifhevea
\(
\newcommand{\R}{{\mathbb{R}}}
\newcommand{\C}{{\mathbb{C}}}
\newcommand{\Z}{{\mathbb{Z}}}
\newcommand{\N}{{\mathbb{N}}}
\newcommand{\Q}{{\mathbb{Q}}}
\newcommand{\tr}{\mbox{tr\,}}
\)
\else
\newcommand{\R}{{\mathbb{R}}}
\newcommand{\C}{{\mathbb{C}}}
\newcommand{\Z}{{\mathbb{Z}}}
\newcommand{\N}{{\mathbb{N}}}
\newcommand{\Q}{{\mathbb{Q}}}
\newcommand{\tr}{\mbox{tr\,}}
\fi
%HEVEA\htmlfoot{Retour \`a la page principale de \ahref{http://www-fourier.ujf-grenoble.fr/\home{parisse}/giac_fr.html}{Giac/Xcas}.}
\giacmathjax
%HEVEA\renewcommand{\footertext}{}

\begin{document}
\title{Géométrie et olympiades~: AI Google 23++ vs Xcas 40}
\author{Bernard.Parisse@univ-grenoble-alpes.fr}
\date{4 Février 2024}

\begin{giacjshere}
\maketitle

\begin{abstract}
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). 
\end{abstract}


\tableofcontents

%\printindex

\section{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
\ahref{http://www.imo-official.org/problems.aspx}{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.

\section{AlphaGeometry (AG)}
Voir la section \ref{sec:ref} 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$.
{\bf 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é~:
\begin{giaconload}
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);
\end{giaconload}

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, \\
\begin{giaconload}
factor(numer(I-M));
\end{giaconload}
\begin{giaconload}
factor(numer(distance2(O,P)-distance2(O,Q)));
\end{giaconload}

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$.
\begin{giaconload}
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);
\end{giaconload}

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).

\section{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 
\ahref{https://xcas.univ-grenoble-alpes.fr/forum/viewtopic.php?f=32&t=2891#p12830}{forum de Xcas}.

La commande \verb|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$.
\begin{giaconload}
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));
\end{giaconload}
\\
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~:\\
\giacinput{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\\
\giacinputmath{factor(coordinates(J))}\\

Voici quelques méthodes qui permettent de simplifier les calculs de Xcas~:
\begin{itemize}
\item 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.
\item 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)$.
\item 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.
\item 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.
\item
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.\\
\verb|otherd(A,D,c):=reflection(projection(A,D,center(c)),A):;|
\item 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.\\
\verb|otherc(c1,c2,A):=reflection(line(center(c1),center(c2)),A):;|
\item 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\\
\verb|assume(t=[0.2,0,1,0.01]);|\\
\verb|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}$).
\item Lors des calculs, on évitera si possible les racines carrées,
en utilisant les instructions adéquates de Xcas~: 
\verb|distance2|, 
\verb|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)
\item 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
\verb|normal(im((B-A)/(C-A)))==0|, on peut même
éviter l'introduction d'une fraction avec le test
\verb|normal(im((B-A)*conj(C-A)))==0|
\item 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).  
\item 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).
\item Les problèmes d'olympiade travaillent avec des angles
non orientés, on peut utiliser la fonction tangente
pour gérer cette spécificité
\item Il est parfois nécessaire d'aider le système pour obtenir
une simplification à 0. Par exemple, développer une fonction
trigonométrique avec \verb|texpand|, multiplier par le conjugué
avec la commande \verb|mult_conjugate()|, ...
\end{itemize}
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.

\section{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.

\section{Références} \label{sec:ref}
\begin{enumerate}
\item
AlphaGeometry~:
\ahref{https://www.nature.com/articles/s41586-023-06747-5}{l'article de la revue Nature},
\ahref{https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt}{les 30 traductions},
\ahref{https://static-content.springer.com/esm/art\%3A10.1038\%2Fs41586-023-06747-5/MediaObjects/41586_2023_6747_MOESM1_ESM.pdf}{le détail des
preuves de AG},
\ahref{https://github.com/google-deepmind/alphageometry}{le code source}.

\item
\ahref{https://xcas.univ-grenoble-alpes.fr/forum/viewtopic.php?f=32&t=2891#p12830}{Les 40 solutions Xcas}.

\item D'autres logiciels de géométrie avec assistance de preuve
\ahref{http://www.matf.bg.ac.rs/\home{janicic}/gclc}{GCLC},
\ahref{https://github.com/yezheng1981/Java-Geometry-Expert}{JGEX}
version Java de
\ahref{http://www.mmrc.iss.ac.cn/gex/}{GEX}, 
%MMP Geometer (pas de lien actif trouvé), Geologic.
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 
\ahref{https://arxiv.org/pdf/1603.01228.pdf}{Geogebra Portfolio Prover} 
par la méthode dite de Botana.

\item 
\ahref{https://fr.wikipedia.org/wiki/Axiomes_de_Tarski}{L'axiomatique de Tarski},
\ahref{https://hal.science/hal-00426563/PDF/areaMethodRecapV2.pdf}{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),
\ahref{https://scholarworks.umt.edu/cgi/viewcontent.cgi?article=1034&context=tme}{la méthode de Wu}.

\item
\ahref{http://www.imo-official.org/problems.aspx}{Le site des olympiades},


\end{enumerate}

\end{giacjshere}
\end{document}
