Bonjour à toutes, à tous et aux autres !
J'ai fait à l'occasion quelques allusion à ce sujet, mais il me semble qu'il n'a pas de fil dédié.
La démonstration automatique reste très peu performante sauf quelques cas particuliers, il faut donc toujours des mathématiciens. (par démonstration automatique, j'entends le fait de fournir un énoncé à un ordinateur et lui demander d'en fournir une démonstration si possible).
Par contre, la vérification automatique de preuve ( fournir une démonstration à un ordinateur et lui demander si elle est correcte) semble avoir de l'avenir et ce dans un futur proche, voire maintenant.
Elle pourrait même changer dans un certaine mesure la façon de faire des mathématiques.
J'ai trouvé l'article ci-dessous:
http://images.math.cnrs.fr/Un-ordina...ifier-les.html
Qu'en pensez vous ?