Intervention de Cédric Villani

Yves Meyer, dans un premier temps, avait parlé des apports extraordinaires de l'informatique aux mathématiques, mais des apports se font également dans l'autre sens. Actuellement, l'informatique théorique est très excitante. Les langages comme Coq incorporent leur propre vérification mathématique. Un autre exemple a fait couler beaucoup d'encre : le fameux théorème des quatre couleurs : la première vérification informatique, assez obscure, jamais acceptée par une partie de la communauté, a été revisitée récemment avec des outils de programmations comme Coq, et il est apparu que la preuve originelle était partiellement défaillante. L'approche constructive est toujours beaucoup plus sûre.

Je crains que nous ne soyons pas compétents pour répondre à la question relative à l'enseignement de l'informatique au lycée. Quand j'étais jeune, comme beaucoup de monde, j'ai appris à programmer en Pascal, mais, depuis, la discipline a beaucoup évolué. Cela dit, quel que soit le langage, la programmation obéit aux mêmes principes.