ACTIONS
par Jean-Christophe Filliâtre
Démonstration
L'ordinateur à la rescousse
Une intelligence artificielle comparable à celle de l'être
humain reste encore à ce jour hors de notre portée. Pour
autant, l'ordinateur peut nous aider à mener bien des
raisonnements, parfois même très complexes.
Il n 'est pas possible d 'écrire
un programme qui prend en entrée
un énoncé mathématique
et qui détermine, en un temps fini,
si cet énoncé est vrai ouf aux.
Puzzle Artifact illustrant le théorème
des quatre couleurs
(design : Tara Flannery).
L
' ordinateur est e ncore lo in des
pe r fo rm a nces hum a in es e n
te rmes d ' inte ll igence , mais il
a des ato uts que l' être humain ne possède pas : une capac ité de ca lc ul incomparable , une docilité totale et une fiabilité
sans fa ille dès lors que la mi ss io n q ui lui
a é té confiée l'a é té avec ri g ue ur.
li se mb le a lo rs no rm al que le mathém ati c ie n c he rc he à s ' a ppu yer dess us
po ur l'a ide r da ns ses dé mo nstra ti o ns ,
surto ut ce lles do nt il a du mal à se tire r
to ut seul. Dans ce but , il a do nc im ag iné plu sie urs o uti ls in fo rmatiques.
L'assistant de preuue
L' un des o uti ls les pl us notables de la
dé mo nstrati o n ass istée pa r o rdinate ur
est l'ass istant de pre uve. Un ass ista nt
de pre uve est un log icie l qui vé rifie les
é ta pes d' un ra iso nne me nt log ique. Il
Tangente Hors-série n°52. Mathématiques & informatique