méthode de Wu

Imaginez une figure tracée dans un repère. Chaque point reçoit des coordonnées, et chaque relation géométrique devient une égalité entre polynômes. Être à égale distance de deux points, par exemple, se traduit par l'égalité de deux distances au carré.

La méthode de Wu organise alors les équations des hypothèses en une base caractéristique. Elle élimine successivement des variables et réduit l'équation à démontrer. Si le reste obtenu est nul, sous les conditions de non-dégénérescence requises, le calcul établit le théorème.

La méthode de Wu est une procédure algébrique de démonstration automatique pour des énoncés de géométrie traduisibles par des équations polynomiales. Des coordonnées sont attribuées aux points. Les incidences, parallélismes, perpendicularités ou égalités de distances utiles deviennent un système d'hypothèses polynomiales. La conclusion est elle aussi écrite comme l'annulation d'un polynôme.

À partir des polynômes d'hypothèse, la procédure construit une base caractéristique, c'est-à-dire un système triangulaire ordonné qui facilite l'élimination successive des variables. Elle calcule ensuite le pseudo-reste du polynôme de conclusion par rapport à ce système. Un pseudo-reste nul fournit la vérification algébrique recherchée sur les configurations qui satisfont les hypothèses et les conditions de non-dégénérescence associées au calcul.

Le résultat est une preuve symbolique, et non une vérification sur quelques dessins numériques. Une implémentation dans un assistant de preuve tel que Coq peut en outre certifier les étapes formelles de la démonstration.

La procédure suit quatre opérations. 1. Choisir des coordonnées et traduire les hypothèses en polynômes nuls. 2. Traduire la conclusion en un polynôme à annuler. 3. Construire une base caractéristique des hypothèses selon un ordre de variables. 4. Réduire la conclusion par cette base. Si le pseudo-reste est nul et si les facteurs de non-dégénérescence nécessaires ne s'annulent pas, la conclusion est établie pour les configurations considérées.

La méthode s'applique lorsque les données géométriques et la conclusion peuvent être exprimées par des égalités polynomiales en coordonnées. Il faut fixer un repère, nommer les variables et préciser les hypothèses qui excluent les configurations dégénérées, par exemple deux points censés définir une droite qui coïncideraient. L'ordre choisi pour les variables détermine aussi la forme du système triangulaire obtenu.

Un énoncé qui dépend d'une inégalité, d'un ordre ou d'une propriété non traduite par les seules annulations polynomiales ne peut pas être traité tel quel par cette réduction. Il faut alors compléter la formalisation ou employer une autre procédure adaptée au type de condition manquante.

On considère deux points A et B, de coordonnées respectives (0, 0) et (2, 0). Un point P a pour coordonnées (x, y). L'hypothèse affirme que P appartient à la médiatrice de [AB], donc que son abscisse x vaut 1. La conclusion à établir est PA = PB.

1. L'hypothèse devient le polynôme h = x − 1, avec h = 0. Dans cet exemple, ce polynôme forme déjà un système triangulaire.

2. Pour éviter les racines carrées, on compare les carrés des distances. Le polynôme de conclusion g est introduit par l'égalité suivante : $g=P{A}^2-P{B}^2=x^2+y^2-((x-2{)}^2+y^2)g=PA^2-PB^2=x^2+y^2-((x-2)^2+y^2)$.

3. Le développement donne g = 4x − 4, soit g = 4(x − 1) = 4h. La réduction de g par h a donc un reste nul.

4. Ainsi PA² − PB² = 0. Les distances étant non négatives, PA = PB. Le contrôle se refait avec P = (1, 3) : PA² = 1² + 3² = 10 et PB² = (1 − 2)² + 3² = 10.

Pour démontrer automatiquement un énoncé de géométrie, on commence par choisir des coordonnées qui simplifient la figure. Les relations du dessin sont ensuite remplacées par des polynômes, puis la conclusion est réduite symboliquement.

Le calcul formel est préférable à une vérification numérique lorsque l'objectif porte sur toutes les configurations admises, et non sur quelques valeurs. Le reste algébrique fournit alors un contrôle reproductible.

Lorsqu'une certification formelle est requise, les calculs peuvent être intégrés dans un assistant de preuve tel que Coq. L'assistant contrôle les étapes encodées, tandis que la méthode de Wu fournit la stratégie d'élimination polynomiale.

La méthode de Wu n'est pas le calcul formel en général. Le calcul formel désigne l'ensemble des manipulations symboliques effectuées par logiciel ; la méthode de Wu est une procédure particulière qui organise des hypothèses géométriques en base caractéristique et réduit une conclusion polynomiale.

Elle ne se confond pas non plus avec un assistant de preuve comme Coq. La méthode détermine le calcul géométrique à mener ; l'assistant fournit un cadre où ce calcul et sa justification peuvent être certifiés. Une élimination effectuée sans Coq reste une application de la méthode, tandis que Coq peut formaliser bien d'autres raisonnements.

Configuration dégénérée. Une division ou une pseudo-division peut faire apparaître un facteur supposé non nul. Si ce facteur s'annule, le pseudo-reste nul ne couvre pas automatiquement cette configuration. Il faut isoler ce cas et l'examiner séparément.

Traduction incomplète. Un dessin peut suggérer qu'un point est situé entre deux autres ou qu'une longueur est positive. Des équations seules n'encodent pas nécessairement cet ordre. Si la conclusion en dépend, ces conditions doivent être formalisées autrement.

Reste nul mal interprété. Le verdict concerne le système polynomial réellement fourni. Une hypothèse oubliée ou une conclusion mal traduite produit une preuve du mauvais énoncé. Le contrôle doit donc porter autant sur l'encodage géométrique que sur l'élimination.

Un prolongement naturel consiste à étudier comment une base caractéristique transforme un système de plusieurs polynômes en système triangulaire. On peut alors suivre l'ordre d'élimination des coordonnées et repérer les facteurs non nuls qui écartent les cas dégénérés.

L'autre prolongement relie calcul et certification : l'élimination produit l'identité algébrique utile, puis un assistant de preuve tel que Coq vérifie sa formalisation. Cette séparation aide à distinguer la découverte automatique d'une preuve de sa validation dans un cadre formel.