Social Processes and Proofs of Theorems and Programs

Richard A. De Millon
Richard J. Lipton et Alan J. Perlis
CACM, May 79, Vol 22, Number 3, p. 271-280

J'y lis :
"The point is that mathematician's errors are corrected, not by formal symbolic logic, but by other mathematicians"

A discuter

Tout ce que je sais c'est que chaque fois que mon prouveur (logiciel) n'arrivait pas à prouver c'est que ce que je lui demandais de prouver n'était pas un théorème. Je m'étais planté dans ma spécification. Certes ce n'était pas de la grande mathématique et comme j'étais en logique des prédicats, je ne pouvais "bénéficier" que de la semi-décidabilité.
Mais je sais bien que la relecture (c'est crevant que relire sérieusement les textes des autres toute la journée) est essentielle. Ne serait-ce que parce qu'on ne peut prouver mathématiquement que notre modélisation est mauvaise.