Source : Communauté de Turing

Auteur : Lin Jun Cen Feng

Wu Wenjun au travail (12 mai 1919-7 mai 2017). Source : Académie des mathématiques et des sciences des systèmes, Académie chinoise des sciences

1979 a été une année importante en Chine. De nombreux événements majeurs ont eu lieu cette année, et elle est également considérée comme un tournant important dans la politique, l'économie, la science et la technologie, la culture et d'autres domaines de la Chine et l'un des points d'arrêt importants de l'histoire chinoise moderne. Comparé à la magnifique nouvelle ère ouverte en 1979, le début de la recherche sur l'intelligence artificielle (IA) en Chine en 1979 ne peut être considéré que comme une vague discrète dans la marée historique, mais dans l'histoire de l'intelligence artificielle en Chine, c'est une révolution événement.

La première école d'intelligence artificielle était l'école du symbolisme. La plupart des premiers scientifiques de l'intelligence artificielle étaient des mathématiciens et des logiciens. Ils ont combiné les ordinateurs avec leurs propres recherches après la naissance des ordinateurs, entrant ainsi dans le domaine de l'intelligence artificielle. En Chine, ce sont aussi des mathématiciens qui ont ouvert la première page de la recherche sur l'intelligence artificielle. En 1979, que ce soit la "Méthode Wu" dans les preuves automatiques qui ait fait le tour du monde, ou la tenue du Computer Science Summer Symposium comparable à la Dartmouth Conference, il y avait des mathématiciens derrière. C'est aussi à partir de cette année que l'intelligence artificielle chinoise a commencé à rattraper le monde.

L'auteur de la "méthode Wu" n'est autre que le mathématicien Wu Wenjun. Avec Wang Xianghao et Zeng Xianchang, il est appelé les "Trois Maîtres de la preuve mécanique". À la fin des années 1970, Wu Wenjun, alors âgé de près de soixante ans, est parti de l'étude des mathématiques chinoises anciennes et a créé un nouveau domaine de la mécanisation mathématique. Il a proposé la « méthode Wu » pour prouver des théorèmes géométriques avec des ordinateurs, qui est considérée comme une travail de pionnier dans le domaine du raisonnement automatique.

1. Wu Wenjun a ouvert la porte à l'intelligence artificielle chinoise pour aller dans le monde

En janvier 1979, à l'invitation de l'Institute for Advanced Study de Princeton, le mathématicien Wu Wenjun embarque pour les États-Unis avec 25 000 dollars en poche.

Il était accompagné du mathématicien Chen Jingrun. Les deux hommes sont le premier groupe de scientifiques invités à étudier et à visiter les Etats-Unis après l'établissement des relations diplomatiques entre la Chine et les Etats-Unis.Ils étudieront et échangeront pendant un certain temps à l'Institute for Advanced Study de Princeton. Le sujet de l'échange de Chen Jingrun est naturellement "1+2", et le contenu principal de l'échange de Wu Wenjun lors de ce voyage, en plus de son ancienne pratique de la topologie, concerne davantage l'histoire des mathématiques chinoises anciennes et de la mécanisation mathématique. pour utiliser les 25 000 yuans qu'il a apportés Dollars acheter un ordinateur pour l'étude de la mécanisation mathématique.

Lorsque Wu Wenjun a remporté le premier prix de sciences naturelles de l'Académie chinoise des sciences (ci-après dénommée "Académie chinoise des sciences") en 1979, la mécanisation mathématique était devenue sa principale direction de recherche. Cette direction de recherche a également attiré l'attention du monde entier. La méthode de recherche de Wu Wenjun est appelée "Méthode Wu" dans le domaine de la preuve du théorème de la machine. La plus haute distinction de la science et de la technologie intelligentes chinoises "Wu Wenjun Artificial Intelligence Science and Technology Award" utilise Le nom de Wu Wenjun pour commémorer Wu Wenjun en tant que réalisations de chercheurs chinois dans des domaines liés à l'IA.

Par inadvertance, Wu Wenjun a ouvert la porte à la recherche chinoise sur l'intelligence artificielle pour se mondialiser. Les recherches de Wu Wenjun sur l'histoire des mathématiques chinoises anciennes ont commencé vers 1974. À cette époque, Guan Zhaozhi, directeur adjoint de l'Institut de mathématiques de l'Académie chinoise des sciences (ci-après dénommé "l'Institut de mathématiques de l'Académie chinoise des sciences"), a demandé à Wu Wenjun d'étudier les mathématiques chinoises anciennes. Wu Wenjun a rapidement découvert la différence importante entre la tradition mathématique chinoise ancienne et la tradition mathématique occidentale moderne héritée de la Grèce antique. Il a mené une analyse approfondie de l'arithmétique chinoise ancienne et a développé des idées uniques dans de nombreux aspects.

Dans les années 1970, les échanges universitaires étrangers ont commencé à reprendre progressivement. En 1975, Wu Wenjun se rend en France pour un échange et fait un rapport sur la pensée mathématique chinoise ancienne à l'Institut français des sciences avancées. A cette époque, Wu Wenjun avait restauré l'ancienne preuve de la formule de Rigao et avait remarqué les caractéristiques "structurelles" et "mécanistes" des anciennes mathématiques chinoises. Lors du Festival du printemps de 1977, Wu Wenjun a vérifié la faisabilité de la méthode de preuve mécanique du théorème géométrique par calcul manuel, et le processus a duré deux mois.

L'idée originale de prouver le théorème de la machine vient du raisonneur de calcul de Gottfried Wilhelm Leibniz, et a ensuite évolué à partir de la logique symbolique. Plus tard, David Hilbert (David Hilbert) a lancé le "Projet Hilbert" en 1920 sur cette base, espérant axiomatiser strictement l'ensemble du système mathématique. En termes simples, si ce plan est réalisé, cela signifie que pour toute conjecture mathématique, aussi difficile soit-elle, nous pouvons toujours savoir si la conjecture est correcte et la prouver ou la nier. C'est ce que voulait dire Hilbert lorsqu'il disait « Wir müssen wissen, wir werden wissen » (nous devons savoir, nous devons savoir).

Cependant, peu de temps après, en 1931, Kurt Gödel proposa le théorème d'incomplétude de Gödel, qui brisa complètement l'idéal de formalisme de Hilbert. Mais de toute façon, quand Gödel a fermé la porte, il a quand même laissé une fenêtre. La thèse de doctorat du mathématicien de génie français Jacques Herbrand a jeté les bases de la théorie de la preuve et de la théorie de la récursivité de la logique mathématique. Après la proposition du théorème d'incomplétude de Godel, Herbrand a vérifié sa thèse et est parti En un mot - Gödel et mes résultats ne sont pas contradictoires, et je a écrit une lettre à Gödel pour obtenir des conseils. Gödel a répondu à Erblan, mais Erblan n'a pas attendu la lettre. Il est mort dans un accident d'alpinisme deux jours après la réponse de Gödel à l'âge de 23 ans. Plus tard, la plus haute distinction dans le domaine de la démonstration de théorèmes a également été nommée d'après El Brown, et Wu Wenjun a remporté le quatrième prix El Brown pour réalisation exceptionnelle en raisonnement automatique en 1997.

D'autres mathématiciens ont complété le théorème de Gödel. Peu de temps après que Gödel ait prouvé que "les nombres entiers du premier ordre (arithmétiques) sont indécidables", Alfred Tarski a prouvé que "les nombres réels du premier ordre (géométriques et algébriques) sont décidables", cela jette également les bases des preuves de la machine.

En 1936, Turing dans son important article "On Computable Numbers, with an Application to the Entscheidungsproblem" (* On Computable Numbers, with an Application to the Entscheidungsproblem *) de la preuve de Gödel de 1931 et des restrictions de calcul En conséquence, la discussion a été retravaillée, et le langage formel de Gödel basé sur l'arithmétique générale a été remplacé par une forme simple de dispositif abstrait maintenant appelé une machine de Turing, et il a été prouvé que tous les processus calculables peuvent être simulés par une machine de Turing. C'est aussi une base théorique importante pour l'informatique et l'intelligence artificielle. La première école d'intelligence artificielle - l'école des symboles est également étendue sur la base d'opérations logiques formelles.

Pour en revenir à Wu Wenjun, il a travaillé dans l'usine de radio n ° 1 de Pékin qui produisait des ordinateurs dans les années 1970, et à cette époque, il a commencé à entrer en contact avec les ordinateurs et la démonstration de théorèmes machine. "Comment tirer pleinement parti de la puissance de l'ordinateur et l'appliquer à ses propres recherches en mathématiques" est devenu ce qui intéresse Wu Wenjun. Plus tard, Wu Wenjun a commencé à étudier l'histoire des mathématiques chinoises anciennes et a résumé la tendance algébrique géométrique et la pensée algorithmique des mathématiques chinoises anciennes. Après avoir découvert les différentes façons de penser entre les mathématiques chinoises anciennes et les mathématiques occidentales, il a décidé d'utiliser une méthode différente pour faire des preuves automatiques de théorèmes géométriques.

À cette époque, Wu Wenjun a lu de nombreux articles étrangers et a parfaitement compris la preuve de la machine. À cette époque, les recherches les plus pointues sur la démonstration de théorèmes des machines provenaient du mathématicien logicien Wang Hao. Au cours de ses études au Département de mathématiques de la Southwestern Associated University, il a étudié auprès du célèbre philosophe et "la première personne de la philosophie chinoise" Jin. Yuelin, puis est allé à l'Université de Harvard aux États-Unis.Le célèbre philosophe et logicien Willard von Quinn (WV Quine) a étudié le système d'axiome formel fondé par Quine et a obtenu un doctorat. Dès 1953, Wang Hao avait déjà commencé à réfléchir à la possibilité de prouver des théorèmes mathématiques avec des machines.

En 1958, Wang Hao a utilisé un programme de logique propositionnelle sur un ordinateur IBM 7041 pour prouver tous les théorèmes de logique du premier ordre dans "Principes de mathématiques", et a terminé la preuve des 200 théorèmes de logique propositionnelle l'année suivante. L'importance du travail de Wang Haozhi réside dans l'annonce de la possibilité d'utiliser des ordinateurs pour prouver des théorèmes. À son retour en Chine en 1977, il a participé à plusieurs symposiums concernant le développement à long terme de la science et de la technologie de mon pays, et a donné 6 conférences spéciales à l'Académie chinoise des sciences, qui ont eu un impact significatif sur la recherche nationale sur la preuve des machines.

Plus près de nous, il y a encore un écart entre les preuves précédentes des théorèmes de logique propositionnelle de Wang Hao dans "Principes de mathématiques" et les preuves automatiques des théorèmes géométriques que Wu Wenjun veut réaliser. Le premier a des composants logiques plus symboliques, tandis que le second a éléments de raisonnement. . À cette époque, il y avait de nombreuses études à l'étranger sur les preuves automatiques de théorèmes géométriques, mais toutes se sont soldées par un échec.

** Deuxièmement, de la mécanisation de la pensée mathématique chinoise ancienne à la "méthode Wu" **

Selon Wu Wenjun, l'expérience de l'échec est également très importante, elle vous dira quelles routes ne fonctionneront pas. Inspiré par la pensée de Descartes, il transforme des problèmes géométriques en problèmes algébriques en introduisant des coordonnées, puis les mécanise selon l'ancienne pensée mathématique chinoise. Wu Wenjun a même combiné la pensée cartésienne avec la pensée mathématique chinoise ancienne et a proposé une voie pour résoudre des problèmes généraux :

Tous les problèmes peuvent être transformés en problèmes mathématiques, tous les problèmes mathématiques peuvent être transformés en problèmes algébriques, tous les problèmes algébriques peuvent être transformés en problèmes de résolution d'équations, et tous les problèmes de résolution d'équations peuvent être transformés en résolution de problèmes d'équations algébriques à variables uniques.

Les mathématiques chinoises anciennes et les mathématiques modernes occidentales sont deux systèmes différents. Wu Wenjun a restauré le "Zhou Bi Suan Jing" selon les connaissances et la pensée et le raisonnement coutumiers des anciens à cette époque sans utiliser les "outils modernes" tels que les fonctions trigonométriques, le calcul, la factorisation et les solutions d'équations d'ordre supérieur en mathématiques modernes. Les méthodes de preuve de "Rigao Tushuo", "Dayanqiuyishu" et "Zengchengkaifangshu" dans "Nine Chapters of Shushu". Il pense que les mathématiques chinoises anciennes ont leurs propres caractéristiques uniques.La méthode de Qin Jiushao a les caractéristiques de la construction et de la mécanisation, et la solution numérique des équations algébriques d'ordre élevé peut être obtenue avec une petite calculatrice. En l'absence d'équipements informatiques performants à cette époque, Wu Wenjun a pu tirer pleinement parti des anciennes idées mathématiques chinoises pour réduire la dimensionnalité pour la recherche, ce qui est également louable.

Le premier théorème que Wu Wenjun a prouvé conformément à cette idée était le théorème de Feuerbach, qui a prouvé que "le cercle à neuf points d'un triangle est tangent à son cercle inscrit et à trois cercles circonscrits". C'est l'un des plus beaux théorèmes de la géométrie plane, que l'on retrouve dans l'esthétique de Wu Wenjun. Il n'y avait pas d'ordinateur à cette époque, alors Wu Wenjun a calculé à la main. L'une des caractéristiques de la "méthode de Wu" est qu'un grand nombre de polynômes seront générés. Le plus grand polynôme impliqué dans le processus de preuve a des centaines d'éléments. Ce calcul est très difficile, et toute erreur dans une étape entraînera des calculs ultérieurs à échouer. Au Festival du Printemps de 1977, Wu Wenjun a vérifié avec succès la méthode de preuve mécanique du théorème géométrique pour la première fois par calcul manuel. Plus tard, Wu Wenjun a prouvé le théorème de Simson sur une Grande Muraille 203 produite par l'Usine n°1 de la radio de Pékin.

Wu Wenjun a publié l'article de recherche connexe "Problèmes de détermination de la géométrie élémentaire et preuve mécanisée" dans "Chinese Science" en 1977, et a envoyé l'article à Wang Hao. Wang Hao a fait l'éloge du travail de Wu Wenjun et a répondu pour suggérer que Wu Wenjun utilise le package d'algèbre existant et envisage de mettre en œuvre la méthode de Wu avec un ordinateur. Wang Hao n'a pas réalisé la différence entre les ordinateurs utilisés par les meilleurs universitaires en Chine et aux États-Unis à cette époque : la Grande Muraille 203 peut utiliser le langage machine, mais les systèmes d'instruction des différents ordinateurs ne sont pas universels, et ce n'est pas faisable. pour utiliser le package d'algèbre existant. Ainsi, plus tard, Wu Wenjun a simplement emprunté une petite calculatrice à l'Institut de mathématiques de l'Académie chinoise des sciences comme cadeau d'un étranger qui a visité l'Institut de mathématiques de l'Académie chinoise des sciences, a converti la proposition donnée en une forme algébrique, puis utilisé la méthode de Qin Jiushao pour calculer l'équation d'ordre supérieur.

Les recherches de Wu Wenjun sur la preuve automatique des théorèmes géométriques ont été fortement soutenues par Guan Zhaozhi. Guan Zhaozhi avait étudié en France et était l'un des fondateurs de la branche française de l'Association des scientifiques chinois.Il a réuni un groupe d'intellectuels patriotes exceptionnels, et Wu Wenjun était l'un d'entre eux. À cette époque, l'Institut de mathématiques de l'Académie chinoise des sciences où travaillait Wu Wenjun avait des relations compliquées. Une faction croyait que faire des preuves automatiques était "rebelle" et espérait qu'il continuerait à s'engager dans la recherche en topologie ; Guan Zhaozhi, qui passé de la topologie et de l'analyse fonctionnelle à la théorie du contrôle, l'a particulièrement soutenu et l'a compris, disons que Wu Wenjun peut faire ce qu'il veut. Plus tard, lorsque Guan Zhaozhi a créé l'Institut des sciences des systèmes de l'Académie chinoise des sciences en 1979, Wu Wenjun a suivi Guan Zhao à l'Institut des sciences des systèmes de l'Académie chinoise des sciences (Figure 1-1).

Figure 1-1 L'immeuble de bureaux d'origine de l'Institute of Systems Science, Chinese Academy of Sciences (maintenant Rongke Building) au début des années 1980 (de gauche à droite : Xu Guozhi, Wu Wenjun, universitaire indien, Guan Zhaozhi)

Pour prouver des théorèmes plus compliqués, de meilleures machines sont nécessaires. L'académicien Wang Dezhao, alors directeur de l'Institut d'acoustique de l'Académie chinoise des sciences, a donné des conseils à Wu Wenjun. Il a dit à Wu Wenjun quand et où Li Chang, secrétaire du groupe du parti et vice-président de l'Académie chinoise des sciences, apparaîtrait, mais Wu Wenjun l'a vraiment attrapé. Li Chang était très ouvert d'esprit.Lorsqu'il a été président de l'Institut de technologie de Harbin (ci-après dénommé "HIT") dans les années 1950, il a fait de HIT une université nationale de premier ordre. Parmi les six universités nationales clés identifiées en 1954, l'Institut de technologie de Harbin est la seule à ne pas être située à Pékin. Li Chang a également apporté un grand soutien au travail de Wu Wenjun.L'échange de 25 000 dollars américains de Wu Wenjun pour acheter un ordinateur aux États-Unis a été spécialement approuvé par Li Chang. Avec cet ordinateur, de nombreux théorèmes ont été rapidement prouvés.

Les années 1970 ont également été l'âge d'or de la démonstration de théorèmes machine. En 1976, deux mathématiciens américains ont prouvé le théorème des quatre couleurs en utilisant un ordinateur électronique à grande vitesse avec 1200 heures de temps de calcul, et ont résolu le problème difficile que les mathématiciens n'avaient pas résolu depuis plus de 100 ans. La raison pour laquelle le théorème des quatre couleurs peut être prouvé est que les ensembles irréductibles et les ensembles inévitables sont finis. Le problème de "coloration des cartes" du théorème des quatre couleurs semble avoir une infinité de cartes, mais en fait elles peuvent être attribuées à plus de 2000 sortes de formes de base, puis utilisez la puissance de calcul de l'ordinateur pour forcer brutalement et les prouver une par une. D'un point de vue métaphorique, cette approche revient à résoudre un Rubik's cube - en démontant le cube et en le reconstituant - peu élégant mais efficace. On dit maintenant que GPT-3 "fait des miracles avec de grands efforts", mais en fait la preuve du théorème des quatre couleurs est l'ancêtre des "miracles avec de grands efforts".

Cependant, cette pratique consistant à utiliser la puissance de calcul d'un ordinateur pour forcer brutalement les preuves de théorèmes ne peut pas être généralisée. La première étape de la preuve de théorème, la formalisation du théorème, nécessite une formulation complète et rigoureuse. Sur ce point, il y a une petite histoire d'un mathématicien. Un astronome, un physicien et un mathématicien se sont rendus en Écosse en train. Ils ont vu un mouton noir par la fenêtre. L'astronome s'est mis à soupirer : "Pourquoi tous les moutons en Écosse sont-ils noirs ?" Le physicien a corrigé : "Il faut dire que certains les moutons en Ecosse sont noirs." Et l'expression la plus rigoureuse vient des mathématiciens : "En Ecosse il existe au moins un monde, et il y a au moins un mouton, et ce mouton est noir d'au moins un côté." Il y a une autre blague , a déclaré que les problèmes mathématiques sont divisés en deux catégories : l'une est « cela doit également être prouvé ? » et l'autre est « cela peut également être prouvé ? ». De là, nous pouvons voir à quel point il est difficile pour une preuve d'être reconnue par d'autres mathématiciens. De même, pour formaliser un théorème dans un démonstrateur de théorème interactif, il est nécessaire de remplir tous les détails techniques afin de compléter "l'automatisation" du raisonnement, et enfin de remplacer le théorème par une idée de résolution de problème réalisable mais gourmande en calcul. . En d'autres termes, cette méthode repose toujours sur la compréhension des théorèmes par les mathématiciens et ne peut aboutir qu'à "une théorie et une preuve", qui ne peuvent être considérées que comme des preuves de théorèmes assistées par ordinateur.

Par conséquent, après que le théorème des quatre couleurs ait été prouvé par ordinateur, un groupe de logiciens, dont Wang Hao, a émis des opinions différentes : Le théorème des quatre couleurs a-t-il été prouvé ? Ce type de méthode de preuve est considéré comme une preuve traditionnelle, et l'ordinateur ne joue qu'un rôle de calcul auxiliaire. Ce n'est qu'en 2005 que Georges Gonthier a achevé la preuve informatisée complète du théorème des quatre couleurs, et chaque étape de sa dérivation logique a été complétée par un ordinateur. À l'heure actuelle, les gens ont prouvé des centaines de théorèmes mathématiques avec des ordinateurs, mais la plupart de ces théorèmes sont connus et "l'intelligence artificielle" n'a pas encore apporté une réelle contribution aux mathématiques.

La preuve du théorème machine repose sur des algorithmes. Au début, les chercheurs ont souvent essayé de trouver un super algorithme pour résoudre tous les problèmes, mais Wu Wenjun a appliqué les anciennes idées mathématiques chinoises au domaine de la preuve automatique des théorèmes géométriques, réalisant "un type, une preuve". Ce point a également été approuvé par Wang Hao. Il pensait que ses premiers travaux avaient quelque chose en commun avec la méthode utilisée par Wu Wenjun, c'est-à-dire trouver d'abord un sous-champ relativement contrôlable, puis trouver l'algorithme le plus efficace en fonction des caractéristiques de ce champ. sous-domaine. Lorsque Wu Wenjun a visité les États-Unis en 1979, il est également allé à l'Université Rockefeller pour visiter Wang Hao.Son travail a été apprécié dans le domaine du théorème de la machine, qui avait une certaine relation avec la forte recommandation de Wang Hao.

La "méthode Wu" s'est vraiment répandue, faisant la première percée dans la démonstration de théorèmes machine dans les années 1980, grâce à Zhou Xianqing, un étudiant étranger aux États-Unis qui avait écouté le cours de démonstration de théorèmes machines de Wu Wenjun. Zhou Xianqing voulait à l'origine passer le diplôme d'études supérieures de Wu Wenjun dans le domaine de la preuve machine, mais il pensait que la géométrie différentielle était sa faiblesse, alors il avait peur de ne pas pouvoir réussir l'examen, alors il a finalement été admis à l'Université. de la science et de la technologie de Chine (ci-après dénommée "Université des sciences et de la technologie de Chine"), puis est allé à l'Institut de technologie informatique de l'Académie chinoise des sciences sous le nom de Dai Pei. À cet égard, j'ai audité la théorie géométrique de Wu Wenjun. cours de preuve.

En 1981, Zhou Xianqing est allé à l'Université du Texas à Austin pour étudier à l'étranger.À cette époque, l'Université du Texas à Austin était connue comme le roi de la démonstration de théorèmes. Zhou Xianqing a mentionné le travail de Wu Wenjun à Robert Boyer. Boyer pensait que c'était très frais, alors il a continué à demander, mais Zhou Xianqing savait seulement qu'il transformait la géométrie en algèbre, et ne pouvait pas expliquer les détails spécifiques.

Après cela, Woody Bledsoe a demandé à Zhou Xianqing et à un autre étudiant Wang Tiecheng de collecter des données.La thèse de doctorat de Zhou Xianqing était la réalisation de la méthode de Wu. Wu Wenjun envoya rapidement deux articles, qu'il signa tous deux à Bledsoe. Au cours des deux années suivantes, ces deux articles ont été copiés par l'Université du Texas à Austin près d'une centaine de fois et envoyés dans le monde entier, et la méthode Wu est devenue largement connue.

En 1983, la National Academic Conference on Proving Theorems by Machines s'est tenue dans le Colorado, aux États-Unis. Zhou Xianqing a présenté un rapport intitulé "Proving Geometry Theorems Using Wu's Method" lors de la conférence. Le programme général développé par Zhou Xianqing peut prouver automatiquement plus de 130 théorèmes géométriques, y compris des preuves de théorèmes plus difficiles tels que le théorème de Moller, le théorème de Simson, le théorème du cercle à neuf points de Feuerbach et le théorème de Desargues. Par la suite, la collection d'articles de cette conférence a été officiellement publiée en 1984 en tant que 29e volume de la série "Contemporary Mathematics" aux États-Unis, et deux articles connexes envoyés par Wu Wenjun y ont également été inclus.

En juin 1986, le lauréat du prix Turing John Hopcroft (John Hopcroft) et d'autres ont organisé un séminaire sur le raisonnement géométrique automatique, et une partie du rapport du séminaire a été incluse dans "Artificiel Dans l'édition spéciale de "Intelligence", l'article d'introduction de l'édition spéciale présente spécialement la nouvelle méthode de géométrie algébrique proposée par Wu Wenjun. Vision, modélisation solide) ont également une valeur d'application importante (Figure 1-2). Depuis lors, Hopcroft a travaillé en étroite collaboration avec de nombreuses universités en Chine. Il a dirigé des instituts de recherche à l'Université Jiao Tong de Shanghai, à l'Université de Pékin et à l'Université chinoise de Hong Kong (Shenzhen). Wu Wenjun et Wu Fafang sont probablement le début de son complexe chinois.

Figure 1-2 Un aperçu de la méthode de Wu dans le premier chapitre de l'édition spéciale de "l'Intelligence Artificielle" en 1988