Tout est pas mirifique dans le numérique

Je me reproche parfois - boulot oblige - d'avoir tendance à oublier un peu trop le coté obscure des nouvelles technologies. Un buzz sur Internet vient de me rappeler que tout n'est pas angélique dans le numérique.

Ca se passe en Arabie Saoudite. On savait que les femmes devaient pour quitter le pays avoir l'autorisation de leur "tuteur mâle". Yuk ! Maintenant elles peuvent être surveillées électroniquement et leur tuteur reçoit un SMS quand elles sortent du pays...  Beurk ! Yuk !

Lire  http://www.rawstory.com/rs/2012/11/22/saudi-arabia-implements-electronic-tracking-system-for-women/

PS: On se rassure en se disant que si l'informatique est une composante centrale du numérique, elle  n'en est qu'une composante. Au moins on partage la responsabilité avec d'autres.

La littérature peut-elle raconter la science ?

Je ne crois pas qu'on ait résolu le problème, mais en tous cas, on en a causé...

France Culture, Science publique, de Michel Alberganti
Ecouter: http://www.franceculture.fr/player/reecouter?play=4535323

Invités:
Serge Abiteboul, Directeur de Recherche à INRIA, l'institut de recherche en informatique et automatique, membre de l'académie des sciences.
François Bon, écrivain, auteur de théâtre, organisateur d’atelier d’écriture en résidence d’écrivain sur le plateau de Saclay d’avril à décembre 2012
Jean-Michel Frodon, journaliste, longtemps au Monde et aujourd’hui sur Slate.fr, critique de cinéma, professeur associé à Sciences-Po Paris, Coorganisateur des Artssciencefactory Day jusqu'au 29 novembre à Palaiseau.
 Valérie Masson Delmotte, paléoclimatologue au Laboratoire des sciences du climat et de l’environnement du CEA et membre du GIEC.

Feit, Thompson et Gonthier

Le théorème de Feit-Thomson qui traite de la classification des groupes finis simples a été démontré par Walter Feit et John Griggs Thompson in 1963. Il dit (ne me demandez pas de détail) que chaque groupe fini d'ordre impair est résoluble. Georges Gonthier et son équipe du labo INRIA-Microsoft ont achevé en Septembre sa preuve formelle en utilisant le système Coq développé à l'INRIA. Bravo!

Polémique hier au café au LSV:

• C'est un truc techniquement super mais les mathématiciens s'en foutent.
• Ils s'en foutent peut-être mais cela va changer profondément les mathématiques.
• Pas le moins du monde... 

Tout ce que je vais écrire est purement spéculatif et discutable. Je sais que de nombreux collègues mathématiciens hurleraient en le lisant. Mais comme nous sommes entre nous... 

Développer une preuve mathématique est quelque chose de purement artisanal, souvent impliquant seulement un crayon et une feuille de papier. On peut imaginer l'arrivée d'outils qui aideront les mathématiciens en vérifiant leurs hypothèses, en proposant des pistes, en développant des preuves formelles. Le mathématicien serait libéré de la partie fastidieuse des démonstrations. On sort de l'artisanat.

Développer une preuve mathématique est quelque chose de purement individuel (le plus souvent). On peut imaginer des collaborations entre des groupes de mathématiciens autour d'outils informatiques qui leurs permettraient d'additionner leurs talents, leurs efforts.

Bien sûr, tout ce que je dis s'applique aussi aux preuves de programme. C'est finalement un peu la même chose.

Il est énormément plus complexe de découvrir une preuve que de la vérifier. Les ordinateurs font mieux que nous dans la vérification. J'ose le sacrilège. Seront-ils un jour meilleurs que nos meilleurs mathématiciens pour démontrer des théorèmes? Et il nous resterait quoi? Peiner à comprendre leurs preuves? Proposer des théorèmes?