Vérifier sans faille les démonstrations mathématiques par ordinateur

[Durakwir]

Pour ceux qui aiment les maths
.
Techno-science.com
Par Michel


Lorsque les mathématiciens démontrent des théorèmes de manière traditionnelle, ils présentent leurs arguments sous forme narrative. Ils assument des résultats précédents, ils glissent sur des détails qu'ils pensent que les autres experts comprendront, ils prennent des raccourcis pour rendre la présentation moins pénible, ils font appel à l'intuition, etc. L'exactitude des arguments est déterminée par l'examen minutieux effectué par d'autres mathématiciens, au cours de discussions informelles, lors de conférences, ou dans des articles. Il est important de se rendre compte que les moyens par lesquels les résultats mathématiques sont vérifiés constituent essentiellement un procédé social donc faillible. Quand elle concerne un résultat primordial et bien connu, la démonstration (Cet article ou cette section doit être recyclé. Sa qualité devrait être largement améliorée en le réorganisant et en le...) est particulièrement bien contrôlée et des erreurs sont éventuellement trouvées. Cependant l'histoire des mathématiques a connu des résultats faux qui sont restés longtemps non décelés. En outre, pour quelques cas récents, des théorèmes importants exigeaient des démonstrations tellement longues et complexes que très peu de gens ont le temps (Le temps est un concept développé pour représenter la variation du monde : l'Univers n'est jamais figé, les...), l'énergie (Dans le sens commun l'énergie désigne tout ce qui permet d'effectuer un travail, fabriquer de la chaleur, de la...), et le fond de connaissance nécessaire pour en vérifier l'exactitude par eux-mêmes. Enfin, certaines démonstrations contiennent un code informatique (L'informatique désigne l'automatisation du traitement de l'information par un système, concret (machine) ou abstrait....) considérable pour, par exemple, vérifier de nombreux cas qu'il serait impossible de contrôler à la main. Comment les mathématiciens peuvent-ils alors être sûrs que de telles démonstrations soient fiables ?

Pour venir à bout de ces problèmes, des informaticiens et des mathématiciens ont commencé à développer le domaine de la preuve formelle. Une preuve formelle est une démonstration dans laquelle chaque inférence logique est systématiquement contrôlée vis-à-vis des axiomes fondamentaux des mathématiques. Les mathématiciens n'écrivent habituellement pas ces preuves formelles parce qu'elles sont si longues et "encombrantes" qu'il serait impossible de les faire vérifier par des mathématiciens humains. Mais on peut désormais obliger des "assistants informatiques" à procéder à ce contrôle (Le mot contrôle peut avoir plusieurs sens. Il peut être employé comme synonyme d'examen, de vérification et de maîtrise.). Ces dernières années, ces assistants sont devenus assez puissants pour manipuler des démonstrations complexes

Source techno-science.com
Suite de l'article
Vérifier sans faille les démonstrations mathématiques par ordinateur

.