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

Table des matières

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 nn 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 KK avec comme contrainte que l’angle AKBAKB est droit, que l’on traduira classiquement par KK appartient au cercle de diamètre ABAB. 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 ABCABC un triangle et OO le centre de son cercle circonscrit. Les points PP et QQ sont des points intérieurs aux côtés CACA et ABAB respectivement. Soit KK, LL et MM les milieux respectifs des segments BPBP, CQCQ et PQPQ, et soit Γ\Gamma le cercle passant par KK, LL et MM. On suppose que la droite (PQ)(PQ) est tangente au cercle Γ\Gamma. Montrer que OPOP = OQOQ.
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 MLKMLK be a triangle. Define point WW as the circumcenter of triangle LMKLMK. Define point QQ such that MWMW is perpendicular to MQMQ. Define point PP as the mirror of QQ through MM. Define point BB as the mirror of PP through KK. Define point CC as the mirror of QQ through LL. Define point AA as the intersection of lines QBQB and PCPC. Define point OO as the circumcenter of triangle CBACBA. Prove that QO=POQO=PO.

Le début de preuve de AG:
Proof : Construct point DD such that MK=LDMK = LD and MD=LKMD = LK.
Construct point EE as the mirror of KK through WW .
Construct point FF as the mirror of QQ through DD.
Step 1. M,Q,PM, Q, P are collinear and MQ=MPMMQ = MP \rightarrow M is the midpoint of QPQP.
... 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 ABCDABCD un quadrilatère convexe tel que BABCBA \neq BC. Les cercles inscrits dans les triangles ABCABC et ADCADC sont notés respectivement ω 1\omega_1 et ω 2\omega_2. On suppose qu’il existe un cercle ω\omega qui est tangent à la demi-droite [BA)[BA) au-delà de AA, tangent à la demi-droite [BC)[BC) au-delà de CC, et qui est aussi tangent aux droites (AD)(AD) et (CD)(CD). Montrer que les tangentes communes extérieures à ω 1\omega_1 et à ω 2\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 XYZXYZ be a triangle. Define point OO as the circumcenter of triangle YXZYXZ. Let WW be any point on circle (O,X)(O, X). Define point AA such that AXAX is perpendicular to OXOX and AZAZ is perpendicular to OZOZ. Define point BB such that BWBW is perpendicular to OWOW and BZBZ is perpendicular to OZOZ. Define point CC such that CWCW is perpendicular to OWOW and CYCY is perpendicular to OYOY. Define point DD such that DXDX is perpendicular to OXOX and DYDY is perpendicular to OYOY. Define point I 1I_1 such that AI 1AI_1 is the bisector of angle BACBAC and CI 1CI_1 is the bisector of angle ACBACB. Define point I 2I_2 such that AI 2AI_2 is the bisector of angle CADCAD and DI 2DI_2 is the bisector of angle ADCADC. Define point F 1F_1 as the foot of I 1I_1 on line ACAC. Define point F 2F_2 as the foot of I 2I_2 on line ACAC. Define points Q,TQ, T such that F 1I 1=I 1Q,F 2I 2=I 2TF_1 I_1 =I_1 Q, F_2 I_2 = I_2 T, I 1QI_1 Q is perpendicular to QTQT and I 2TI_2 T is perpendicular to QTQT. Define points PP, SS such that F 1I 1=I 1PF_1 I_1 = I_1 P , F 2I 2=I 2SF_2 I_2 = I_2 S, I 1PI_1 P is perpendicular to PSPS and I 2SI_2S is perpendicular to PSPS. Define point KK as the intersection of lines PSPS and QTQT. Prove that OK=OXOK = 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 II le centre du cercle inscrit dans le triangle ABCABC et soit Γ\Gamma son cercle circonscrit. La droite (AI)(AI) recoupe Γ\Gamma en DD. Soit EE un point de l’arc BDCBDC et FF un point du côté [BC][BC] tels que BAFBAF = CAE<1/2BACCAE &lt; 1/2 BAC. Soit enfin GG le milieu du segment [IF][IF]. Montrer que les droites (DG)(DG) and (EI)(EI) se coupent en un point JJ 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 ABCABC sont optimisées pour simplifier les calculs, voir ci-dessous. Voici maintenant la commande qui résoud le problème :


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



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

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

  1. AlphaGeometry : l’article de la revue Nature, les 30 traductions, le détail des preuves de AG, le code source.
  2. Les 40 solutions Xcas.
  3. 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.
  4. 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.
  5. 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 ABCABC un triangle tel que AB<AC<BCAB&lt;AC&lt;BC. Soit ω\omega le cercle inscrit à ABCABC et II son centre. Soit XX le point de (BC)(BC) distinct de CC tel que la droite passant par XX parallèle à (AC)(AC) soit tangente à ω\omega, et de même YY en échangeant le rôle de BB et CC. Soit PP la deuxième intersection de la droite (AI)(AI) avec le cercle circonscrit à ABCABC. Soit KK et LL les milieux de ACAC et BCBC respectivement.
Montrer que la somme des angles IK,ILIK,IL et PY,PXPY,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

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 XX et YY est possible, d’ailleurs Google indique bien que la figure d’illustration est une construction approchée. En effet, XX semble construit comme un point quelconque de la droite (BC)(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 XX et YY est assez simple, il suffit de prendre l’intersection de la droite symétrique par rapport à II de (AC)(AC) ou de (AB)(AB) avec (BC)(BC). On peut se demander si une telle solution mérite vraiment 7/7...

  

Retour à la page principale de Giac/Xcas.
Ce document a été traduit de LATEX par HEVEA