A vrai dire, le théorème d'incomplétude de Gödel a prouvé en 1931 l'inexistence d'un système à la fois consistent et complet pour l'arithmétique. Alors si on ne peut pas prouver l'arithmétique, on ne risque pas de prouver des cas plus compliqués (comme les langages de programmation Turing-complets utilisés majoritairement, et même des langages plus simples).
Les réseaux neuronaux ne vont pas aider. Ils pourraient se baser sur des heuristiques (ce que fait l'homme), mais comment distinguer ce qui est formellement prouvé par les règles d'inférence (réécriture) de ce qui est supposé par exploration?
Ce que l'homme est capable de faire, et que l'ordinateur ne peut pas faire, c'est sortir du système de types (aller dans une couche "méta" sur demande). Il existe des classes computationnelles où les algorithmes de preuves sont tractables (voire simplement décidables) mais ce sont des cas restreints et peu pratiques pour l'informatique "réelle".
Donc, effectivement, théoriquement, il y a quelque chose qui les empêche. Si on reste dans le cadre formel. Après, si on s'en fout que l'ordinateur dise n'importe quoi, oui on peut, mais autant faire une sortie aléatoire qui dit vrai ou faux.
[^] # Re: prouveur automatique/assistant de preuve
Posté par smc . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 6.
Les réseaux neuronaux ne vont pas aider. Ils pourraient se baser sur des heuristiques (ce que fait l'homme), mais comment distinguer ce qui est formellement prouvé par les règles d'inférence (réécriture) de ce qui est supposé par exploration?
Ce que l'homme est capable de faire, et que l'ordinateur ne peut pas faire, c'est sortir du système de types (aller dans une couche "méta" sur demande). Il existe des classes computationnelles où les algorithmes de preuves sont tractables (voire simplement décidables) mais ce sont des cas restreints et peu pratiques pour l'informatique "réelle".
Donc, effectivement, théoriquement, il y a quelque chose qui les empêche. Si on reste dans le cadre formel. Après, si on s'en fout que l'ordinateur dise n'importe quoi, oui on peut, mais autant faire une sortie aléatoire qui dit vrai ou faux.