Ingénierie mathématique : définition et exemple

Description :


Conférencier : Jean-Raymond Abrial

Biographie : Né en 1938, Jean-Raymond Abrial est un informaticien internationalement reconnu et considéré comme un pionnier du développement scientifique des méthodes formelles et de leur application à grande échelle dans l’industrie. Ses travaux reposent sur des techniques mathématiques rigoureuses appliquées à la conception de logiciels et figurent parmi les plus cités en informatique. Ses brillantes recherches ont mené à des applications concrètes, bien ancrées dans la société. L’une des méthodes dont il est l’auteur (la méthode B) est notamment à la base de l’automatisation des systèmes de transport de lignes de métro d’une vingtaine de grandes métropoles (dont Paris, Mexico, Hong Kong, Barcelone, San Juan et New York) et permet de transporter en toute sécurité plus de deux millions de personnes par jour. Jean-Raymond Abrial a fait ses études à l’École Polytechnique de France et possède également un diplôme de l’Université Standford aux États-Unis. En 2004, il a accepté un poste de professeur à l’ETH Zurich. Chercheur indépendant, scientifique intègre, il a interagi avec les milieux académique et industriel tout au long de sa carrière. Il travaille maintenant sur la méthode Event-B pour la spécification et l’analyse des systèmes et la construction d’algorithmes, ainsi que sur la construction de preuves mathématiques dans un contexte d’ingénierie du logiciel.

Résumé :Après avoir travaillé pendant des années sur la question de la construction correcte de systèmes sensibles, je me suis tourné depuis quelque temps vers les questions d’éducation. En effet, il ne sert à rien de proposer des méthodes rigoureuses pour la construction de tels systèmes si les acteurs de terrain n’ont pas la formation nécessaire pour comprendre et appliquer ce genre d’approches.

Je me suis aperçu alors (mais je le savais déjà) que les informaticiens de terrain n’avaient pas reçu, bien souvent, la formation suffisante leur permettant d’appliquer des méthodes rigoureuses (mathématiques) dans leur travail de tous les jours. Il y a, en fait, un vrai problème, central, lié à l’élaboration de preuves rigoureuses (mathématiques) : bien souvent les informaticiens de terrain ne savent pas quoi prouver ni comment le faire.

Cherchant à introduire ce genre de questions dans le curriculum des étudiants en informatique, je me suis demandé quelle sorte de matériels on pourrait utiliser. L’idée qui m’est venue à l’esprit serait de proposer l’étude de quelques preuves mathématiques simples pour voir comment les mathématiciens professionnels s’y prennent et ainsi montrer aux étudiants la marche à suivre.

Pour cela, je me suis plongé dans la recherche de telles preuves présentées dans des livres de référence ou dans des articles. Je voulais construire une base de données de telles preuves, base de données que l’on pourrait ensuite consulter pour y puiser de quoi construire des cours. Mais, à ma grande stupéfaction, je me suis aperçu que les mathématiciens professionnels travaillaient un peu en circuit fermé et que leurs preuves étaient souvent difficiles à comprendre (pour moi) et peu aptes à servir d’exemples exportables vers des étudiants qui ne sont pas, a priori, des mathématiciens de formation.

Il ne me restait donc plus qu’à reprendre ces preuves et à leur donner une forme plus lisible pour tous. C’est cela que j’appelle « l’ingénierie mathématique ».

Au cours de ce séminaire, je présenterai trois exemples de constructions de telles preuves : le théorème de point fixe de Knaster-Tarski, le théorème de Cantor-Bernstein (sur l’existence d’une bijection entre deux ensembles reliés par des injections totales) et le théorème de Fürstenberg (sur la preuve topologique de l’infinitude des nombres premiers).

Toutes les personnes intéressées sont cordialement invitées.