Wu Wen-Tsun

Imaginez une figure tracée sur une feuille : des points sont alignés, des droites se coupent et certains angles ont une propriété précise. Wu Wen-Tsun propose de traduire ces observations en équations polynomiales, c'est-à-dire des égalités faites de nombres et de produits de nombres inconnus. Un ordinateur peut alors examiner le système obtenu. La démonstration automatique ne remplace donc pas la figure : elle transforme ses relations visibles en calculs que l'on peut vérifier et résoudre par une procédure automatisée.

Wu Wen-Tsun désigne ici le mathématicien et la méthode de démonstration automatique associée à ses travaux en géométrie plane. Le principe est de représenter les points par des coordonnées, puis d'exprimer les relations géométriques par des équations polynomiales. Une relation d'incidence, par exemple l'alignement de trois points, devient une égalité entre coordonnées.

L'énoncé géométrique fournit les hypothèses du système et la propriété à établir devient une conséquence algébrique. Les variables représentent les coordonnées ou d'autres grandeurs inconnues ; elles doivent être accompagnées des conditions qui décrivent réellement la figure. La résolution peut alors être automatisée, sous réserve que la traduction conserve les hypothèses de départ et ne crée pas de configurations parasites.

Cette démarche relie la tradition algorithmique des mathématiques chinoises à l'approche axiomatique occidentale. Elle s'inscrit dans les recherches de Wu Wen-Tsun en topologie, notamment sur les espaces fibrés et les variétés fibrées, tout en donnant un cadre particulier à la géométrie plane.

Pour illustrer la traduction algébrique, considérons trois points du plan : A(0, 0), B(2, 1) et C(4, 2). L'énoncé étudié est : ces trois points sont alignés.

Données : x_A=0, y_A=0 ; x_B=2, y_B=1 ; x_C=4, y_C=2.

1. Pour trois points, l'alignement se traduit par l'égalité des produits croisés : $(x_B-x_A)(y_C-y_A)-(y_B-y_A)(x_C-x_A)=0(x\_B-x\_A)(y\_C-y\_A)-(y\_B-y\_A)(x\_C-x\_A)=0$.
2. En remplaçant les coordonnées, on obtient $(2-0)(2-0)-(1-0)(4-0)=4-4=0(2-0)(2-0)-(1-0)(4-0)=4-4=0$.
3. Le critère est satisfait : les points A, B et C sont alignés.

Le contrôle est refaisable en calculant les pentes lorsque les différences d'abscisses ne sont pas nulles : AB donne 1/2 et AC donne 1/2. Le critère polynomial évite toutefois de diviser ; il reste donc directement exploitable dans un système automatisé.

Pour analyser un énoncé de géométrie plane, on commence par recenser les points, les droites et les relations annoncées. On choisit ensuite des coordonnées adaptées et on traduit chaque relation en équations polynomiales. Cette organisation rend les hypothèses visibles avant toute résolution.

Le calcul algébrique devient utile lorsque plusieurs relations doivent être vérifiées ensemble ou lorsque la figure comporte des inconnues. Une construction géométrique reste préférable pour explorer rapidement une configuration et voir sa forme ; la traduction polynomiale devient préférable quand il faut tester une conséquence de manière systématique.

Dans une démonstration automatisée, la résolution du système fournit un moyen de contrôler la conséquence recherchée. Il faut ensuite relire la correspondance entre les solutions et les figures admissibles, car une solution algébrique ne décrit pas nécessairement la configuration géométrique initialement voulue.

La démonstration automatique de Wu Wen-Tsun ne se confond pas avec un simple calcul numérique. Un calcul numérique évalue des données déjà fixées ; ici, les coordonnées et les relations de la figure sont encodées afin qu'un système algébrique puisse établir une conséquence. Le cas des trois points A(0, 0), B(2, 1) et C(4, 2) tranche : l'égalité des produits croisés formalise l'alignement au lieu de seulement mesurer une distance.

Cette méthode ne se confond pas non plus avec une preuve formelle au sens général. Son domaine décrit dans la fiche est la géométrie plane traduite en équations polynomiales ; une preuve formelle peut reposer sur d'autres langages et d'autres objets. Le critère décisif est donc le mode d'encodage de l'énoncé, pas la seule présence d'un ordinateur.

Un système polynomial peut avoir des solutions qui ne correspondent pas à la figure visée. Le symptôme est une configuration qui satisfait les égalités mais viole une condition géométrique, comme l'ordre de points ou la non-coïncidence de deux objets. Il faut conserver ces conditions dans la traduction ou examiner chaque solution dans le domaine géométrique annoncé.

Une division peut masquer un cas particulier. Pour l'alignement, comparer des pentes impose de supposer les différences d'abscisses non nulles ; le cas d'une droite verticale échappe alors au calcul. Le critère polynomial par produits croisés évite cette division, mais il faut encore vérifier que les trois points sont bien distincts si l'énoncé l'exige.

Enfin, automatiser la résolution ne garantit pas à lui seul la fidélité de la modélisation. Une hypothèse oubliée, une convention de coordonnées différente ou une propriété traduite de façon incomplète peut produire une conclusion exacte pour le mauvais système. La vérification porte donc à la fois sur les équations et sur leur interprétation géométrique.

Pour prolonger cette fiche, on peut étudier comment une relation géométrique passe d'une figure à un système d'équations, puis comparer les solutions algébriques avec les configurations réellement admissibles. Ce prolongement permet de comprendre pourquoi l'encodage des hypothèses est aussi important que la résolution automatique.