Chou Shang-Ching

À l'université du Texas à Austin, Shang-Ching Chou travaille à faire traiter des problèmes de géométrie par des algorithmes. Une figure est décrite à l'aide de nombres et d'équations. L'ordinateur transforme alors la question géométrique en un problème sur des polynômes.

Cette traduction rend automatique une partie du raisonnement : le programme examine les relations algébriques et détermine si la conclusion découle des hypothèses. Chou est surtout connu pour avoir contribué à cette approche des preuves géométriques.

Shang-Ching Chou est un mathématicien américain d'origine chinoise, professeur à l'université du Texas à Austin. Ses domaines de spécialité sont les mathématiques appliquées et l'informatique mathématique. Ses travaux les plus connus portent sur la démonstration automatique de théorèmes de géométrie.

Le principe consiste à coder les hypothèses et la conclusion d'un énoncé géométrique sous forme d'équations polynomiales. Des algorithmes d'algèbre peuvent ensuite déterminer si la conclusion est une conséquence des hypothèses. Les approches associées à Chou s'appuient notamment sur les bases de Gröbner et sur la méthode de Wu-Ritt, issue des travaux de Wu Wenjun.

Cette démarche concerne d'abord des énoncés de géométrie élémentaire qui se traduisent en relations polynomiales. Elle relie ainsi géométrie algorithmique, démonstration automatique et calcul formel. Les contributions de Chou ont aussi participé à l'extension de l'automatisation de la preuve vers d'autres domaines mathématiques.

On veut vérifier que les diagonales d'un parallélogramme ont le même milieu. Les données sont les quatre sommets A de coordonnées (0 ; 0), B (4 ; 0), C (5 ; 2) et D (1 ; 2). Ces valeurs satisfont les relations du parallélogramme : de A à B et de D à C, le déplacement vaut (4 ; 0).

1. Pour la diagonale AC, on calcule la moyenne des abscisses puis celle des ordonnées.

2. Pour la diagonale BD, on effectue le même calcul.

3. Les deux calculs donnent exactement le point de coordonnées (5/2 ; 1). Le contrôle est refaisable en doublant ses coordonnées : on obtient (5 ; 2), soit A + C comme B + D. Dans une preuve automatique, ces égalités sont encodées en relations polynomiales, puis l'algorithme vérifie que les deux milieux coïncident.

Pour un théorème de géométrie élémentaire, on choisit des coordonnées, puis on traduit alignements, parallélismes ou distances en équations. Cette voie est pertinente lorsque toutes les relations utiles sont polynomiales.

Le calcul formel prend ensuite le relais : une base de Gröbner ou la méthode de Wu-Ritt organise l'élimination algébrique. Si l'énoncé ne se laisse pas encoder ainsi, il faut choisir une autre forme de raisonnement ou un autre outil de preuve.

Dans l'exemple du parallélogramme, le geste pratique est de comparer les coordonnées des deux milieux. Leur accord exact fournit le verdict attendu et permet de refaire le contrôle sans se fier au dessin.

Shang-Ching Chou et la méthode de Wu-Ritt. Chou est le mathématicien auquel cette fiche est consacrée ; Wu-Ritt est une méthode algébrique issue des travaux de Wu Wenjun. Dans une phrase, le critère est simple : l'un désigne une personne, l'autre un procédé de calcul.

Preuve automatique et simple vérification d'un dessin. Une figure qui semble correcte ne prouve pas un énoncé. La démonstration automatique traite les relations algébriques issues des hypothèses ; le cas du parallélogramme se tranche donc par les coordonnées des milieux, et non par leur apparence à l'écran.

Une traduction algébrique est indispensable. Si une relation géométrique n'est pas exprimée par les équations polynomiales choisies, l'algorithme ne peut pas l'utiliser. Il faut compléter l'encodage ou changer de cadre de preuve.

Les cas dégénérés doivent être surveillés. Des points confondus ou trois points alignés peuvent satisfaire certaines équations tout en ne représentant pas la figure attendue. Le symptôme est une configuration aplatie ou indéterminée ; il faut alors ajouter les conditions de non-dégénérescence nécessaires.

Un exemple numérique n'est pas une preuve générale. Les quatre sommets choisis confirment le résultat pour un parallélogramme particulier. Pour couvrir tous les parallélogrammes admissibles, l'algorithme doit travailler avec des coordonnées variables et les relations polynomiales qui caractérisent la figure.

Le prolongement naturel consiste à suivre toute la chaîne qui relie une figure à une preuve : choix de coordonnées, mise en équations polynomiales, élimination par une base de Gröbner ou par la méthode de Wu-Ritt, puis interprétation géométrique du résultat. Cette perspective montre pourquoi les travaux de Chou se situent au croisement de la géométrie algorithmique, du calcul formel et de l'automatisation de la preuve.