Une puissance de matrice, conjecturée puis démontrée

import numpy as np
import numpy.linalg as al

M = np.array([[1, 2], [0, 1]])

for n in range(1, 11):
    A = al.matrix_power(M, n)
    B = np.array([[1, 2 * n], [0, 1]])    # la formule conjecturee
    # le plus grand ecart, coefficient par coefficient
    print(n, np.max(np.abs(A - B)))

Ce que la machine affiche : un $0$ sur chacune des dix lignes. La conjecture

$$M^n=\left(\begin{array}{cc}1& 2n\\ 0& 1\end{array}\right)$$

est donc confirmée pour $n=1,\dots ,10$.

La démonstration, par récurrence. L'initialisation en $n=1$ est immédiate. Supposons la formule vraie au rang $n$ ; alors

$$M^{n+1}=M^{n}M=\left(\begin{array}{cc}1& 2n\\ 0& 1\end{array}\right)\left(\begin{array}{cc}1& 2\\ 0& 1\end{array}\right)=\left(\begin{array}{cc}1& 2n+2\\ 0& 1\end{array}\right)=\left(\begin{array}{cc}1& 2(n+1)\\ 0& 1\end{array}\right),$$

qui est la formule au rang $n+1$. Elle vaut donc pour tout $n\ge 1$.

Le point délicat. Dix vérifications ne démontrent rien : elles disent seulement qu'aucun contre-exemple n'apparaît parmi les dix premiers cas. La machine suggère la formule, la récurrence l'établit. C'est exactement le partage des rôles que le programme attend de l'informatique.

Un détail de code. On compare par np.max(np.abs(A - B)) et non par A == B : ce test rend un tableau de booléens, pas un booléen. Sur des coefficients flottants, on comparerait d'ailleurs cet écart à un petit seuil plutôt qu'à zéro.