Moi je dirais qu'il n'en existe pas encore, mais théoriquement, je vois pas ce qui l'empêche.
Théoriquement, il est prouvé depuis longtemps qu'il n'existe pas d'algorithme permettant entre autres, et pour n'importe quel programme en entrée:
- de déterminer si ce programme s'arrête
- de déterminer si ce programme fait la même chose qu'un autre programme
- et par extension de déterminer si ce programme est conforme à sa spécification
Donc tous les prouveurs qu'on pourra écrire seront limités, non autonomes ou non déterministes.
En poussant ton approche plus loin on peut même observer que si la conscience humaine est simulable sur ordinateur, alors un humain ne peut pas non plus prouver toutes ces choses.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Yusei (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 6.
Théoriquement, il est prouvé depuis longtemps qu'il n'existe pas d'algorithme permettant entre autres, et pour n'importe quel programme en entrée:
- de déterminer si ce programme s'arrête
- de déterminer si ce programme fait la même chose qu'un autre programme
- et par extension de déterminer si ce programme est conforme à sa spécification
Donc tous les prouveurs qu'on pourra écrire seront limités, non autonomes ou non déterministes.
En poussant ton approche plus loin on peut même observer que si la conscience humaine est simulable sur ordinateur, alors un humain ne peut pas non plus prouver toutes ces choses.