o btenir de s ph è res dan s l'es pace est
ce lui utili sé pour fa ire les piles de boulets de canon ou les tas d 'oranges).
Un bon ass istant ne sert pas seule ment
à exéc ute r doc il e me nt des co r vées
si mples qu 'on pourrait faire soi-mê me
à la main si o n éta it près à y consacré
des années ou des s ièc les . li sera d 'autant plu s préc ie ux qu 'o n pourra lui
demander des tâc hes subtil es. Grâce
aux log ic ie ls de calcul formel e t de
démonstration automatique, il n'est pas
ra re qu ' une parti e dé li cate de dé mon stration o u un morceau difficile de ca lcul so it confi é à l'ordin ate ur.
Aujourd ' hui , on voit donc fréquemment
des recherches où l'ordinateur interv ient
en fournissant son aide au moment de la
découverte des nouveaux énoncés, étape
sui vie par une aide à la mise au po int des
démonstrations et éventuellement à leur
contrô le (sans parler de l'a ide qu 'apporte ( 'ordinateur pour éditer les textes
mathématiques, les imprimer et les faire
circuler entre chercheurs).
L'ordinateur pour confirmer
et contrôler
Signalons encore qu'un usage important de l' ordinateur se mbl e e n vue à
cause justement de la complex ité des
preuves que l' interaction e ntre ordinateurs et mathématic iens engendre. La
démonstration que Thomas Hales a mise
au point de la conjecture de Kepler et dont
certaines parties fo nt interve nir des calcul s informatiques a été publiée avec
une mi se en garde du comité d 'experts
chargé d'en fournir la garantie: le comité
a indiqué qu ' il ne pou vait pas assurer
q u'auc une erreur n'éta it restée. Pour
lever cette incertitude, Thomas Ha les a
entrepri s de produire une vers ion formalisée de sa dé monstration , c'est-àdire une version dont chaque pas est
so igneusement ex pli c ité et pe ut être
POUR LES MATHS
contrôl é mécaniquement. Bien sûr le
trava il de mi se au point de la version
formal isée se fait en s'aidant d 'ordinateurs, et une fois que ce travail sera effectué , ce sera encore l'ordinateur qui sera
chargé du contrôle final de la justesse de
chaque pas de la preuve formalisée. Un
tel travail d 'éc riture formelle d ' une
preuve associée à sa vérification a été mené
pour le théorè me des quatre couleurs
par Georges Gonthier.
Cet usage des ordinateurs pour valider
des démonstrations complexes est une
forme nouvelle d 'expérimentation mathématique. Elle s'ajoute aux nombreuses
autres form es d 'ex pé rimentation s e n
train d 'e nvahir l'ense ig ne me nt et la
recherche mathé matique.
J.-P. D.
Bibliographie
• J. Borwein, D . Bai ley, R. Gi rgensohn. Experimetati on in Mathematics:
Computati onal Paths to Discovery. Natick, MA, A. K. Peters, 2004 .
• D. Bailey, J. Borwei n , K . Devi in. The Experimental Mathe matician:
a Computationa l Guide to the Mathematica l Unknown. Natick , MA , A.
K . Peters, 2002 .
• D. Bailey, J . Borwe in , N. Gi rgenshn , Ex perimental Mathematics in
Action, A. K. Peter, 2006.
• K . Cha urasya Experimenta l Mathematics, Campus Books International,
20 12.
• G. Gonthi er, Formai Proof, The Four-Color Theore m . Notices of the
AMS 55 ( 11 ), 1382- 1393, 2008.
• K. Hare. New Techniques for Bou nds on the tota l number of primes factors of an odd Perfects number, Mathematics of Computation, 76:260,
224 1- 2248,2007.
• P. Oc hem, M , Rao,. Odd Perfect Numbers are Greater than 10
1500 ,
Mathemati cs of Computation, 8 1 , 1869- 1877, 20 12.
Hors-série n ° 52. Mathématiques & informatique Tangente
ce lui utili sé pour fa ire les piles de boulets de canon ou les tas d 'oranges).
Un bon ass istant ne sert pas seule ment
à exéc ute r doc il e me nt des co r vées
si mples qu 'on pourrait faire soi-mê me
à la main si o n éta it près à y consacré
des années ou des s ièc les . li sera d 'autant plu s préc ie ux qu 'o n pourra lui
demander des tâc hes subtil es. Grâce
aux log ic ie ls de calcul formel e t de
démonstration automatique, il n'est pas
ra re qu ' une parti e dé li cate de dé mon stration o u un morceau difficile de ca lcul so it confi é à l'ordin ate ur.
Aujourd ' hui , on voit donc fréquemment
des recherches où l'ordinateur interv ient
en fournissant son aide au moment de la
découverte des nouveaux énoncés, étape
sui vie par une aide à la mise au po int des
démonstrations et éventuellement à leur
contrô le (sans parler de l'a ide qu 'apporte ( 'ordinateur pour éditer les textes
mathématiques, les imprimer et les faire
circuler entre chercheurs).
L'ordinateur pour confirmer
et contrôler
Signalons encore qu'un usage important de l' ordinateur se mbl e e n vue à
cause justement de la complex ité des
preuves que l' interaction e ntre ordinateurs et mathématic iens engendre. La
démonstration que Thomas Hales a mise
au point de la conjecture de Kepler et dont
certaines parties fo nt interve nir des calcul s informatiques a été publiée avec
une mi se en garde du comité d 'experts
chargé d'en fournir la garantie: le comité
a indiqué qu ' il ne pou vait pas assurer
q u'auc une erreur n'éta it restée. Pour
lever cette incertitude, Thomas Ha les a
entrepri s de produire une vers ion formalisée de sa dé monstration , c'est-àdire une version dont chaque pas est
so igneusement ex pli c ité et pe ut être
POUR LES MATHS
contrôl é mécaniquement. Bien sûr le
trava il de mi se au point de la version
formal isée se fait en s'aidant d 'ordinateurs, et une fois que ce travail sera effectué , ce sera encore l'ordinateur qui sera
chargé du contrôle final de la justesse de
chaque pas de la preuve formalisée. Un
tel travail d 'éc riture formelle d ' une
preuve associée à sa vérification a été mené
pour le théorè me des quatre couleurs
par Georges Gonthier.
Cet usage des ordinateurs pour valider
des démonstrations complexes est une
forme nouvelle d 'expérimentation mathématique. Elle s'ajoute aux nombreuses
autres form es d 'ex pé rimentation s e n
train d 'e nvahir l'ense ig ne me nt et la
recherche mathé matique.
J.-P. D.
Bibliographie
• J. Borwein, D . Bai ley, R. Gi rgensohn. Experimetati on in Mathematics:
Computati onal Paths to Discovery. Natick, MA, A. K. Peters, 2004 .
• D. Bailey, J. Borwei n , K . Devi in. The Experimental Mathe matician:
a Computationa l Guide to the Mathematica l Unknown. Natick , MA , A.
K . Peters, 2002 .
• D. Bailey, J . Borwe in , N. Gi rgenshn , Ex perimental Mathematics in
Action, A. K. Peter, 2006.
• K . Cha urasya Experimenta l Mathematics, Campus Books International,
20 12.
• G. Gonthi er, Formai Proof, The Four-Color Theore m . Notices of the
AMS 55 ( 11 ), 1382- 1393, 2008.
• K. Hare. New Techniques for Bou nds on the tota l number of primes factors of an odd Perfects number, Mathematics of Computation, 76:260,
224 1- 2248,2007.
• P. Oc hem, M , Rao,. Odd Perfect Numbers are Greater than 10
1500 ,
Mathemati cs of Computation, 8 1 , 1869- 1877, 20 12.
Hors-série n ° 52. Mathématiques & informatique Tangente