Une preuve formelle te donne juste un résultat binaire. Oui la démonstration est juste ou bien Non y'a une merde.
Elle ne t'explique pas l'idée clé. Elle ne te fait pas comprendre intuitivement pourquoi la démonstration fonctionne.
Attention, je ne suis pas d'accord. Une preuve formelle est un document qui décrit la preuve en assez de détails pour être vérifiée par un ordinateur. En particulier, elle contient assez de détails pour être relue et comprise par un humain. Elle n'est pas plus "binaire" en cela qu'une preuve en LaTeX.
La question est de savoir si la personne a fait assez d'efforts, en organisant sa preuve mécanisée, pour que l'argument de preuve soit clair et que la preuve puisse être comprise. (Un programme informatique aussi peut être "correct", faire ce qu'on attend, mais illisible par un autre humain. Une preuve LaTeX aussi peut être incompréhensible.)
Aujourd'hui les outils que nous utilisons pour écrire les preuves mécanisées gênent un peu pour écrire des preuves vraiment agréables à relire—d'où l'habitude de maintenir aussi une preuve informelle en LaTeX en parallèle. On travaille à améliorer cela aussi, et aujourd'hui il est déjà possible en faisant des efforts (de la part de l'auteur, surtout, mais aussi du lecteur) de présenter des preuves mécanisées qui sont aussi lisibles/compréhensibles.
(Je pense que tu as en tête une image des preuves vérifiées basées seulement sur la démonstration automatique, où on demande à l'ordinateur de reconstruire l'argument de preuve sans aucune information (le SAT/SMT-solving par exemple). Quand on utilise un assistant de preuve, on peut (et on doit) donner les arguments de preuve à l'assistant, dès qu'on veut démontrer des propriétés plus complexes/intéressantes que ce qui est facile à vérifier par une machine.)
[^] # Re: Math
Posté par gasche . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 6.
Attention, je ne suis pas d'accord. Une preuve formelle est un document qui décrit la preuve en assez de détails pour être vérifiée par un ordinateur. En particulier, elle contient assez de détails pour être relue et comprise par un humain. Elle n'est pas plus "binaire" en cela qu'une preuve en LaTeX.
La question est de savoir si la personne a fait assez d'efforts, en organisant sa preuve mécanisée, pour que l'argument de preuve soit clair et que la preuve puisse être comprise. (Un programme informatique aussi peut être "correct", faire ce qu'on attend, mais illisible par un autre humain. Une preuve LaTeX aussi peut être incompréhensible.)
Aujourd'hui les outils que nous utilisons pour écrire les preuves mécanisées gênent un peu pour écrire des preuves vraiment agréables à relire—d'où l'habitude de maintenir aussi une preuve informelle en LaTeX en parallèle. On travaille à améliorer cela aussi, et aujourd'hui il est déjà possible en faisant des efforts (de la part de l'auteur, surtout, mais aussi du lecteur) de présenter des preuves mécanisées qui sont aussi lisibles/compréhensibles.
(Je pense que tu as en tête une image des preuves vérifiées basées seulement sur la démonstration automatique, où on demande à l'ordinateur de reconstruire l'argument de preuve sans aucune information (le SAT/SMT-solving par exemple). Quand on utilise un assistant de preuve, on peut (et on doit) donner les arguments de preuve à l'assistant, dès qu'on veut démontrer des propriétés plus complexes/intéressantes que ce qui est facile à vérifier par une machine.)