Le 30 septembre 2017 dernier nous apprenions la mort , à seulement 51 ans, du mathématicien Russe
Vladimir Voevodsky. Médaillé Fields en 2002, pour sa démonstration de la célèbre
conjecture de Milnor, une partie de son travail s'est révélée fausse près de 10 ans plus tard! Prenant conscience de la complexité croissante des preuves mathématiques il avait réorienté ses recherches vers le domaine des assistants de preuve formelle ,comme
COQ , et voulait fournir aux mathématiciens des outils pour écrire et vérifier plus rigoureusement des preuves. Dans la croyance populaire on imagine qu'il suffirait de cliquer sur un bouton pour vérifier ou même démontrer un énoncé, évidement la réalité est bien différente et une preuve assistée par un logiciel se révèle souvent très technique. On peut s'en rendre compte en s'intéressant au calcul formel avec des logiciels populaires comme
Maxima. Démontrer les formules qui expriment la
divergence où le
rotationnel d'une fonction vectorielle dans un système de coordonnées non-cartésien demande beaucoup d'habileté mathématique. C'est un bon exemple pour comprendre et réfléchir à ce que représente un calcul assisté par ordinateur ...
$$ \begin{align*}
{\rm div}({\bf A})
&=\partial_x {\bf A}_x+\partial_y{\bf A}_y+\partial_z{\bf A}_z
\\&={\frac {1}{r}} {\partial_r (rA_{r})}+{\frac {1}{r}}{\partial_\theta A_{\theta }}+{\partial_z A_{z}}\\
\begin{array}{c}{\bf rot}({\bf A})\\~ \\ ~\end{array}&\begin{array}{c}= \\~ \\ ~\end{array}
\begin{pmatrix} {\partial_y \mathrm{A}_z } - {\partial_z \mathrm{A}_y} \\
{\partial_z \mathrm{A}_x } - {\partial_x \mathrm{A}_z }\\
{\partial_x \mathrm{A}_y } - {\partial_y \mathrm{A}_x } \end{pmatrix}
\begin{array}{c}= \\~ \\ ~\end{array}
\begin{array}{r}
\left(\frac{1}{r}{\partial_\theta \mathrm{A}_z} - {\partial_z \mathrm{A}_\theta}\right) \mathbf{e_r} \\
+ \left({\partial_z \mathrm{A}_r} - {\partial_r \mathrm{A}_z}\right)\mathbf{e_\theta} \\
+\frac{1}{r}\left({\partial_r}(r \mathrm{A}_\theta) - {\partial_\theta \mathrm{A}_r}\right) \mathbf{e_z}
\end{array}
\end{align*}$$
