Bonjour, j'aimerais savoir si on peut formaliser le concept d'algorithme pour les preuves mathématiques : par exemple pour valider l'algorithme du pgcd d'Euclide, ou le procédé d'orthonormalisation de Gram-Schmidt ; dans un cas général. Dans certains cas, on peut trouver une sorte "d'invariant" dans l'algorithme qui permet de faire une preuve par récurrence (en validant le procédé à l'étape n, et on prouve l'étape n+1) mais ça n'est pas toujours possible. A partir de là, est-il légitime de considérer les procédés "à réitérer" comme des preuves mathématiques toutes aussi valables que celles fournies par les règles d'inférence classiques ?
Je vois une difficulté majeure pour "accepter" leur usage : peut-on être certain que le procédé va se terminer et donner le résultat souhaité (aussi obscure que soit la notion de "terminer" -- sûrement indéfinissable...) ?
Merci par avance pour vos réponses :/