David Hilbert a écrit :
Joe Cool <zierouhli@free.fr> writes:
Ce qui montre bien que vous n'avez rien compris. Qu'espérez-vous, une
preuve de la cohérence de coc dans coc? Vous atteignez les sommets du
ridicule.
Non j'espérais que l'arrogance naturelle de Joe Cool le ferait se
précipiter dans le (gros-énorme) piège. Et il est tombé dedans comme
un seul homme. Évidemment qu'on ne peut pas prouver la cohérence de
Coq dans Coq. N'importe quel idiot sait cela. Même le noyau Coq écrit
en CaML n'est pas vérifié, pas davantage le compilateur CaML, sans
parler du matériel informatique. Cela fait un gros paquet de choses Ã
croire. Qui parlait de croyance ?
Le mathématicien fait confiance à son intuition, là où le logicien,
dépourvu de toute intuition mathématique, est assez naïf, pour ne pas
dire stupide, pour croire au bon fonctionnement d'un matériel sur
lequel des dizaines de milliers de personnes ont travaillé de façon
totalement non coordonnée.
Et tout cela pour quoi ? Pour redémontrer des théorèmes de
mathématiques totalement évidents, ou financer des projets où la
créativité mathématique est NULLE. Et pourtant, ça se permet de donner
des leçons.
David Hilbert.
Mouais... Bon, on fait quoi du programme de Hales (sur la vérification de sa démonstration de la conjecture de Kepler)? Des économies ? On cherche des mathématiciens plus compétents, de créativité plus grande?
