% 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 - Xcas 40} \author{Bernard.Parisse@univ-grenoble-alpes.fr} \date{Janvier 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 classée médaille d'or aux Olympiades internationales de mathématiques (OIM), en annonçant devancer largement les systèmes de preuve en géométrie analytique et variantes à base de calcul formel (dont bases de Groebner). 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é une bonne semaine à 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 2003p3). 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 2002p2 avec 2 solutions, 2008p1 avec 1 solution sur les 2 traductions) et fournit 25 solutions, dont 2 partielles (2 équivalences remplacées par des implications dans un sens: 2003p4 et 2004p5, 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. 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 ce type de résultats avec d'autres 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. Une preuve en géométrie synthétique est souvent plus difficile à concevoir, mais ne nécessite pas d'outil informatique de vérification. La géométrie analytique permet aussi de traiter des problèmes numériques, qui n'ont pas de solution exacte. La géométrie synthétique peut permettre de simplifier certains calculs en géométrie analytique. Enfin, 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, qui permet de construire la figure en respectant les contraintes. 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 un logiciel, 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 2009p2. Le problème 2008p6 est un exemple nettement plus complexe 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$. Ensuite le système 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: 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 est 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??), 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. J'ignore pourquoi les problèmes de 2023 n'ont pas été traités, pour l'article de Nature, c'est certainement lié à la date de soumission, mais pour le communiqué de presse du 17 janvier, on aimerait 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). \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 tangence. On peut ainsi prendre comme points de tangence $(-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$. On évite ainsi des 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|other(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|other(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]$). \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. \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 (é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 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 (l'article parle de 10 000 processeurs en parallèle, il faudrait pour certains problèmes plus d'une centaine de processeurs pour les 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 pendant 72h, ce qui doit représenter une consommation énergétique de l'ordre de 100MWh, plus qu'une existence humaine entière) 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 avec Xcas sur 1 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 peut-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 des assistants de preuve en géométrie utilisant Lean, Coq et probablement aussi 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} et de la bibliographie vers les méthodes de preuves automatiques en géométrie du plan. \item \ahref{http://www.imo-official.org/problems.aspx}{Le site des olympiades}, \end{enumerate} \end{giacjshere} \end{document}