Prouver tout ce qui est prouvable ?

En fait n'importe quel langage de programmation Turing complet permet de faire ça. Les maths ne sont jamais que l'ensemble des chaînes de caractères que l'on peut obtenir à partir d'autres et de règles fixées à l'avance.

Chat d'eau a écrit:

Un agrégé de math m'a affirmé qu'on savait en principe comment faire pour prouver TOUT ce qui est effectivement vrai en math, j'aimerais bien avoir votre avis, et si c'est vrai quel est le système formel qui permet de tout prouver ?

Attention au mot "vrai", il ne veut rien dire sans autre précision (cf théorème de Tarski).
En général les "agrégés de maths" n'en savent pas plus que l'homme de la rue, sauf s'ils ont reçu une formation spécifique en info théorique/logique et ces matières sont assez confidentielles (elles ne font pas partie du tronc commun obligatoire des matheux à la fac, les gens doivent suivre des modules de leur propre initiative).

Une partie de $\N$ est dite récursivement énumérable (resp décidable) si elle est l'image de $\N$ par une fonction calculable par une machine de Turing et définie partout (resp: si sa fonction caractéristique est calculable par une telle machine). Il est connu qu'une partie est décidable si et seulement si elle est récursivement énumérable ainsi que son complémentaire (pour le sens pas immédiat <=, on exécute les machines qui livrent les valeurs des deux parties en parallèle et on attend de tomber sur le nombre qu'on teste).
On peut convenir qu'un théorème est le numéro d'une machine de Turing qui s'arrête, et un théorème avec preuve un couple $(p,l)$ où $p$ est le numéro d'une machine de Turing qui s'arrête et $l$ est la suite de toutes les étapes de calcul de $p$ mises dans l'ordre (*).

Rappelons qu'il existe des bijections calculables de $\N^2$ dans $\N$, telles que $(x,y)\mapsto x+\frac{(x+y)(x+y+1)}{2}$
de coordonnées réciproques calculables (en fait tout se fait avec des boucles for donc c'est même récursif primitif).
Bref on peut identifier couples de nombres et nombres etc.

Les deux résultats que tout le monde devrait connaître:

1°) l'ensemble des théorèmes avec preuves est (trivialement!!) décidable
2°) l'ensemble des théorèmes est récursivement énumérable (par projection de l'ensemble ci-dessus) mais non décidable (en raison du théorème de l'arrêt).

Après que veut dire "algorithme qui décide si on a un théorème"? Faudra voir si par cette formulation vague on tombe sous le coup de 1° ou de 2°. Il faut bien comprendre qu'en dépit des annonces grandiloquentes diverse et autres propagandes de gens qui se réclament parfois de la philo, la nature des maths est fondamentalement simple (des suites de symboles manipulables par opérations élémentaires).

[small](*) Dans n'importe quel système formalisé exprimant des maths une preuve est une liste finie de listes de symboles respectant des critères explicites fixés à l'avance et arbitrables i.e. dont le respect ou non est décidable. Ca peut être la logique du premier ordre, le bourbakisme, une théorie des types etc [/small].